src/HOL/Rings.thy
author haftmann
Mon Nov 29 13:44:54 2010 +0100 (2010-11-29)
changeset 40815 6e2d17cc0d1d
parent 38642 8fa437809c67
child 44064 5bce8ff0d9ae
permissions -rw-r--r--
equivI has replaced equiv.intro
     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   "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 class no_zero_divisors = zero + times +
   187   assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
   188 begin
   189 
   190 lemma divisors_zero:
   191   assumes "a * b = 0"
   192   shows "a = 0 \<or> b = 0"
   193 proof (rule classical)
   194   assume "\<not> (a = 0 \<or> b = 0)"
   195   then have "a \<noteq> 0" and "b \<noteq> 0" by auto
   196   with no_zero_divisors have "a * b \<noteq> 0" by blast
   197   with assms show ?thesis by simp
   198 qed
   199 
   200 end
   201 
   202 class semiring_1_cancel = semiring + cancel_comm_monoid_add
   203   + zero_neq_one + monoid_mult
   204 begin
   205 
   206 subclass semiring_0_cancel ..
   207 
   208 subclass semiring_1 ..
   209 
   210 end
   211 
   212 class comm_semiring_1_cancel = comm_semiring + cancel_comm_monoid_add
   213   + zero_neq_one + comm_monoid_mult
   214 begin
   215 
   216 subclass semiring_1_cancel ..
   217 subclass comm_semiring_0_cancel ..
   218 subclass comm_semiring_1 ..
   219 
   220 end
   221 
   222 class ring = semiring + ab_group_add
   223 begin
   224 
   225 subclass semiring_0_cancel ..
   226 
   227 text {* Distribution rules *}
   228 
   229 lemma minus_mult_left: "- (a * b) = - a * b"
   230 by (rule minus_unique) (simp add: left_distrib [symmetric]) 
   231 
   232 lemma minus_mult_right: "- (a * b) = a * - b"
   233 by (rule minus_unique) (simp add: right_distrib [symmetric]) 
   234 
   235 text{*Extract signs from products*}
   236 lemmas mult_minus_left [simp, no_atp] = minus_mult_left [symmetric]
   237 lemmas mult_minus_right [simp,no_atp] = minus_mult_right [symmetric]
   238 
   239 lemma minus_mult_minus [simp]: "- a * - b = a * b"
   240 by simp
   241 
   242 lemma minus_mult_commute: "- a * b = a * - b"
   243 by simp
   244 
   245 lemma right_diff_distrib[algebra_simps, field_simps]: "a * (b - c) = a * b - a * c"
   246 by (simp add: right_distrib diff_minus)
   247 
   248 lemma left_diff_distrib[algebra_simps, field_simps]: "(a - b) * c = a * c - b * c"
   249 by (simp add: left_distrib diff_minus)
   250 
   251 lemmas ring_distribs[no_atp] =
   252   right_distrib left_distrib left_diff_distrib right_diff_distrib
   253 
   254 lemma eq_add_iff1:
   255   "a * e + c = b * e + d \<longleftrightarrow> (a - b) * e + c = d"
   256 by (simp add: algebra_simps)
   257 
   258 lemma eq_add_iff2:
   259   "a * e + c = b * e + d \<longleftrightarrow> c = (b - a) * e + d"
   260 by (simp add: algebra_simps)
   261 
   262 end
   263 
   264 lemmas ring_distribs[no_atp] =
   265   right_distrib left_distrib left_diff_distrib right_diff_distrib
   266 
   267 class comm_ring = comm_semiring + ab_group_add
   268 begin
   269 
   270 subclass ring ..
   271 subclass comm_semiring_0_cancel ..
   272 
   273 end
   274 
   275 class ring_1 = ring + zero_neq_one + monoid_mult
   276 begin
   277 
   278 subclass semiring_1_cancel ..
   279 
   280 end
   281 
   282 class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult
   283   (*previously ring*)
   284 begin
   285 
   286 subclass ring_1 ..
   287 subclass comm_semiring_1_cancel ..
   288 
   289 lemma dvd_minus_iff [simp]: "x dvd - y \<longleftrightarrow> x dvd y"
   290 proof
   291   assume "x dvd - y"
   292   then have "x dvd - 1 * - y" by (rule dvd_mult)
   293   then show "x dvd y" by simp
   294 next
   295   assume "x dvd y"
   296   then have "x dvd - 1 * y" by (rule dvd_mult)
   297   then show "x dvd - y" by simp
   298 qed
   299 
   300 lemma minus_dvd_iff [simp]: "- x dvd y \<longleftrightarrow> x dvd y"
   301 proof
   302   assume "- x dvd y"
   303   then obtain k where "y = - x * k" ..
   304   then have "y = x * - k" by simp
   305   then show "x dvd y" ..
   306 next
   307   assume "x dvd y"
   308   then obtain k where "y = x * k" ..
   309   then have "y = - x * - k" by simp
   310   then show "- x dvd y" ..
   311 qed
   312 
   313 lemma dvd_diff[simp]: "x dvd y \<Longrightarrow> x dvd z \<Longrightarrow> x dvd (y - z)"
   314 by (simp only: diff_minus dvd_add dvd_minus_iff)
   315 
   316 end
   317 
   318 class ring_no_zero_divisors = ring + no_zero_divisors
   319 begin
   320 
   321 lemma mult_eq_0_iff [simp]:
   322   shows "a * b = 0 \<longleftrightarrow> (a = 0 \<or> b = 0)"
   323 proof (cases "a = 0 \<or> b = 0")
   324   case False then have "a \<noteq> 0" and "b \<noteq> 0" by auto
   325     then show ?thesis using no_zero_divisors by simp
   326 next
   327   case True then show ?thesis by auto
   328 qed
   329 
   330 text{*Cancellation of equalities with a common factor*}
   331 lemma mult_cancel_right [simp, no_atp]:
   332   "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b"
   333 proof -
   334   have "(a * c = b * c) = ((a - b) * c = 0)"
   335     by (simp add: algebra_simps)
   336   thus ?thesis by (simp add: disj_commute)
   337 qed
   338 
   339 lemma mult_cancel_left [simp, no_atp]:
   340   "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b"
   341 proof -
   342   have "(c * a = c * b) = (c * (a - b) = 0)"
   343     by (simp add: algebra_simps)
   344   thus ?thesis by simp
   345 qed
   346 
   347 end
   348 
   349 class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors
   350 begin
   351 
   352 lemma square_eq_1_iff:
   353   "x * x = 1 \<longleftrightarrow> x = 1 \<or> x = - 1"
   354 proof -
   355   have "(x - 1) * (x + 1) = x * x - 1"
   356     by (simp add: algebra_simps)
   357   hence "x * x = 1 \<longleftrightarrow> (x - 1) * (x + 1) = 0"
   358     by simp
   359   thus ?thesis
   360     by (simp add: eq_neg_iff_add_eq_0)
   361 qed
   362 
   363 lemma mult_cancel_right1 [simp]:
   364   "c = b * c \<longleftrightarrow> c = 0 \<or> b = 1"
   365 by (insert mult_cancel_right [of 1 c b], force)
   366 
   367 lemma mult_cancel_right2 [simp]:
   368   "a * c = c \<longleftrightarrow> c = 0 \<or> a = 1"
   369 by (insert mult_cancel_right [of a c 1], simp)
   370  
   371 lemma mult_cancel_left1 [simp]:
   372   "c = c * b \<longleftrightarrow> c = 0 \<or> b = 1"
   373 by (insert mult_cancel_left [of c 1 b], force)
   374 
   375 lemma mult_cancel_left2 [simp]:
   376   "c * a = c \<longleftrightarrow> c = 0 \<or> a = 1"
   377 by (insert mult_cancel_left [of c a 1], simp)
   378 
   379 end
   380 
   381 class idom = comm_ring_1 + no_zero_divisors
   382 begin
   383 
   384 subclass ring_1_no_zero_divisors ..
   385 
   386 lemma square_eq_iff: "a * a = b * b \<longleftrightarrow> (a = b \<or> a = - b)"
   387 proof
   388   assume "a * a = b * b"
   389   then have "(a - b) * (a + b) = 0"
   390     by (simp add: algebra_simps)
   391   then show "a = b \<or> a = - b"
   392     by (simp add: eq_neg_iff_add_eq_0)
   393 next
   394   assume "a = b \<or> a = - b"
   395   then show "a * a = b * b" by auto
   396 qed
   397 
   398 lemma dvd_mult_cancel_right [simp]:
   399   "a * c dvd b * c \<longleftrightarrow> c = 0 \<or> a dvd b"
   400 proof -
   401   have "a * c dvd b * c \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)"
   402     unfolding dvd_def by (simp add: mult_ac)
   403   also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b"
   404     unfolding dvd_def by simp
   405   finally show ?thesis .
   406 qed
   407 
   408 lemma dvd_mult_cancel_left [simp]:
   409   "c * a dvd c * b \<longleftrightarrow> c = 0 \<or> a dvd b"
   410 proof -
   411   have "c * a dvd c * b \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)"
   412     unfolding dvd_def by (simp add: mult_ac)
   413   also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b"
   414     unfolding dvd_def by simp
   415   finally show ?thesis .
   416 qed
   417 
   418 end
   419 
   420 class inverse =
   421   fixes inverse :: "'a \<Rightarrow> 'a"
   422     and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "'/" 70)
   423 
   424 class division_ring = ring_1 + inverse +
   425   assumes left_inverse [simp]:  "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
   426   assumes right_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> a * inverse a = 1"
   427   assumes divide_inverse: "a / b = a * inverse b"
   428 begin
   429 
   430 subclass ring_1_no_zero_divisors
   431 proof
   432   fix a b :: 'a
   433   assume a: "a \<noteq> 0" and b: "b \<noteq> 0"
   434   show "a * b \<noteq> 0"
   435   proof
   436     assume ab: "a * b = 0"
   437     hence "0 = inverse a * (a * b) * inverse b" by simp
   438     also have "\<dots> = (inverse a * a) * (b * inverse b)"
   439       by (simp only: mult_assoc)
   440     also have "\<dots> = 1" using a b by simp
   441     finally show False by simp
   442   qed
   443 qed
   444 
   445 lemma nonzero_imp_inverse_nonzero:
   446   "a \<noteq> 0 \<Longrightarrow> inverse a \<noteq> 0"
   447 proof
   448   assume ianz: "inverse a = 0"
   449   assume "a \<noteq> 0"
   450   hence "1 = a * inverse a" by simp
   451   also have "... = 0" by (simp add: ianz)
   452   finally have "1 = 0" .
   453   thus False by (simp add: eq_commute)
   454 qed
   455 
   456 lemma inverse_zero_imp_zero:
   457   "inverse a = 0 \<Longrightarrow> a = 0"
   458 apply (rule classical)
   459 apply (drule nonzero_imp_inverse_nonzero)
   460 apply auto
   461 done
   462 
   463 lemma inverse_unique: 
   464   assumes ab: "a * b = 1"
   465   shows "inverse a = b"
   466 proof -
   467   have "a \<noteq> 0" using ab by (cases "a = 0") simp_all
   468   moreover have "inverse a * (a * b) = inverse a" by (simp add: ab)
   469   ultimately show ?thesis by (simp add: mult_assoc [symmetric])
   470 qed
   471 
   472 lemma nonzero_inverse_minus_eq:
   473   "a \<noteq> 0 \<Longrightarrow> inverse (- a) = - inverse a"
   474 by (rule inverse_unique) simp
   475 
   476 lemma nonzero_inverse_inverse_eq:
   477   "a \<noteq> 0 \<Longrightarrow> inverse (inverse a) = a"
   478 by (rule inverse_unique) simp
   479 
   480 lemma nonzero_inverse_eq_imp_eq:
   481   assumes "inverse a = inverse b" and "a \<noteq> 0" and "b \<noteq> 0"
   482   shows "a = b"
   483 proof -
   484   from `inverse a = inverse b`
   485   have "inverse (inverse a) = inverse (inverse b)" by (rule arg_cong)
   486   with `a \<noteq> 0` and `b \<noteq> 0` show "a = b"
   487     by (simp add: nonzero_inverse_inverse_eq)
   488 qed
   489 
   490 lemma inverse_1 [simp]: "inverse 1 = 1"
   491 by (rule inverse_unique) simp
   492 
   493 lemma nonzero_inverse_mult_distrib: 
   494   assumes "a \<noteq> 0" and "b \<noteq> 0"
   495   shows "inverse (a * b) = inverse b * inverse a"
   496 proof -
   497   have "a * (b * inverse b) * inverse a = 1" using assms by simp
   498   hence "a * b * (inverse b * inverse a) = 1" by (simp only: mult_assoc)
   499   thus ?thesis by (rule inverse_unique)
   500 qed
   501 
   502 lemma division_ring_inverse_add:
   503   "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a + inverse b = inverse a * (a + b) * inverse b"
   504 by (simp add: algebra_simps)
   505 
   506 lemma division_ring_inverse_diff:
   507   "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a - inverse b = inverse a * (b - a) * inverse b"
   508 by (simp add: algebra_simps)
   509 
   510 lemma right_inverse_eq: "b \<noteq> 0 \<Longrightarrow> a / b = 1 \<longleftrightarrow> a = b"
   511 proof
   512   assume neq: "b \<noteq> 0"
   513   {
   514     hence "a = (a / b) * b" by (simp add: divide_inverse mult_assoc)
   515     also assume "a / b = 1"
   516     finally show "a = b" by simp
   517   next
   518     assume "a = b"
   519     with neq show "a / b = 1" by (simp add: divide_inverse)
   520   }
   521 qed
   522 
   523 lemma nonzero_inverse_eq_divide: "a \<noteq> 0 \<Longrightarrow> inverse a = 1 / a"
   524 by (simp add: divide_inverse)
   525 
   526 lemma divide_self [simp]: "a \<noteq> 0 \<Longrightarrow> a / a = 1"
   527 by (simp add: divide_inverse)
   528 
   529 lemma divide_zero_left [simp]: "0 / a = 0"
   530 by (simp add: divide_inverse)
   531 
   532 lemma inverse_eq_divide: "inverse a = 1 / a"
   533 by (simp add: divide_inverse)
   534 
   535 lemma add_divide_distrib: "(a+b) / c = a/c + b/c"
   536 by (simp add: divide_inverse algebra_simps)
   537 
   538 lemma divide_1 [simp]: "a / 1 = a"
   539   by (simp add: divide_inverse)
   540 
   541 lemma times_divide_eq_right [simp]: "a * (b / c) = (a * b) / c"
   542   by (simp add: divide_inverse mult_assoc)
   543 
   544 lemma minus_divide_left: "- (a / b) = (-a) / b"
   545   by (simp add: divide_inverse)
   546 
   547 lemma nonzero_minus_divide_right: "b \<noteq> 0 ==> - (a / b) = a / (- b)"
   548   by (simp add: divide_inverse nonzero_inverse_minus_eq)
   549 
   550 lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (-a) / (-b) = a / b"
   551   by (simp add: divide_inverse nonzero_inverse_minus_eq)
   552 
   553 lemma divide_minus_left [simp, no_atp]: "(-a) / b = - (a / b)"
   554   by (simp add: divide_inverse)
   555 
   556 lemma diff_divide_distrib: "(a - b) / c = a / c - b / c"
   557   by (simp add: diff_minus add_divide_distrib)
   558 
   559 lemma nonzero_eq_divide_eq [field_simps]: "c \<noteq> 0 \<Longrightarrow> a = b / c \<longleftrightarrow> a * c = b"
   560 proof -
   561   assume [simp]: "c \<noteq> 0"
   562   have "a = b / c \<longleftrightarrow> a * c = (b / c) * c" by simp
   563   also have "... \<longleftrightarrow> a * c = b" by (simp add: divide_inverse mult_assoc)
   564   finally show ?thesis .
   565 qed
   566 
   567 lemma nonzero_divide_eq_eq [field_simps]: "c \<noteq> 0 \<Longrightarrow> b / c = a \<longleftrightarrow> b = a * c"
   568 proof -
   569   assume [simp]: "c \<noteq> 0"
   570   have "b / c = a \<longleftrightarrow> (b / c) * c = a * c" by simp
   571   also have "... \<longleftrightarrow> b = a * c" by (simp add: divide_inverse mult_assoc) 
   572   finally show ?thesis .
   573 qed
   574 
   575 lemma divide_eq_imp: "c \<noteq> 0 \<Longrightarrow> b = a * c \<Longrightarrow> b / c = a"
   576   by (simp add: divide_inverse mult_assoc)
   577 
   578 lemma eq_divide_imp: "c \<noteq> 0 \<Longrightarrow> a * c = b \<Longrightarrow> a = b / c"
   579   by (drule sym) (simp add: divide_inverse mult_assoc)
   580 
   581 end
   582 
   583 class division_ring_inverse_zero = division_ring +
   584   assumes inverse_zero [simp]: "inverse 0 = 0"
   585 begin
   586 
   587 lemma divide_zero [simp]:
   588   "a / 0 = 0"
   589   by (simp add: divide_inverse)
   590 
   591 lemma divide_self_if [simp]:
   592   "a / a = (if a = 0 then 0 else 1)"
   593   by simp
   594 
   595 lemma inverse_nonzero_iff_nonzero [simp]:
   596   "inverse a = 0 \<longleftrightarrow> a = 0"
   597   by rule (fact inverse_zero_imp_zero, simp)
   598 
   599 lemma inverse_minus_eq [simp]:
   600   "inverse (- a) = - inverse a"
   601 proof cases
   602   assume "a=0" thus ?thesis by simp
   603 next
   604   assume "a\<noteq>0" 
   605   thus ?thesis by (simp add: nonzero_inverse_minus_eq)
   606 qed
   607 
   608 lemma inverse_eq_imp_eq:
   609   "inverse a = inverse b \<Longrightarrow> a = b"
   610 apply (cases "a=0 | b=0") 
   611  apply (force dest!: inverse_zero_imp_zero
   612               simp add: eq_commute [of "0::'a"])
   613 apply (force dest!: nonzero_inverse_eq_imp_eq) 
   614 done
   615 
   616 lemma inverse_eq_iff_eq [simp]:
   617   "inverse a = inverse b \<longleftrightarrow> a = b"
   618   by (force dest!: inverse_eq_imp_eq)
   619 
   620 lemma inverse_inverse_eq [simp]:
   621   "inverse (inverse a) = a"
   622 proof cases
   623   assume "a=0" thus ?thesis by simp
   624 next
   625   assume "a\<noteq>0" 
   626   thus ?thesis by (simp add: nonzero_inverse_inverse_eq)
   627 qed
   628 
   629 end
   630 
   631 text {*
   632   The theory of partially ordered rings is taken from the books:
   633   \begin{itemize}
   634   \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979 
   635   \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963
   636   \end{itemize}
   637   Most of the used notions can also be looked up in 
   638   \begin{itemize}
   639   \item \url{http://www.mathworld.com} by Eric Weisstein et. al.
   640   \item \emph{Algebra I} by van der Waerden, Springer.
   641   \end{itemize}
   642 *}
   643 
   644 class ordered_semiring = semiring + comm_monoid_add + ordered_ab_semigroup_add +
   645   assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
   646   assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"
   647 begin
   648 
   649 lemma mult_mono:
   650   "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * d"
   651 apply (erule mult_right_mono [THEN order_trans], assumption)
   652 apply (erule mult_left_mono, assumption)
   653 done
   654 
   655 lemma mult_mono':
   656   "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * d"
   657 apply (rule mult_mono)
   658 apply (fast intro: order_trans)+
   659 done
   660 
   661 end
   662 
   663 class ordered_cancel_semiring = ordered_semiring + cancel_comm_monoid_add
   664 begin
   665 
   666 subclass semiring_0_cancel ..
   667 
   668 lemma mult_nonneg_nonneg: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b"
   669 using mult_left_mono [of 0 b a] by simp
   670 
   671 lemma mult_nonneg_nonpos: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> a * b \<le> 0"
   672 using mult_left_mono [of b 0 a] by simp
   673 
   674 lemma mult_nonpos_nonneg: "a \<le> 0 \<Longrightarrow> 0 \<le> b \<Longrightarrow> a * b \<le> 0"
   675 using mult_right_mono [of a 0 b] by simp
   676 
   677 text {* Legacy - use @{text mult_nonpos_nonneg} *}
   678 lemma mult_nonneg_nonpos2: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> b * a \<le> 0" 
   679 by (drule mult_right_mono [of b 0], auto)
   680 
   681 lemma split_mult_neg_le: "(0 \<le> a & b \<le> 0) | (a \<le> 0 & 0 \<le> b) \<Longrightarrow> a * b \<le> 0" 
   682 by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)
   683 
   684 end
   685 
   686 class linordered_semiring = ordered_semiring + linordered_cancel_ab_semigroup_add
   687 begin
   688 
   689 subclass ordered_cancel_semiring ..
   690 
   691 subclass ordered_comm_monoid_add ..
   692 
   693 lemma mult_left_less_imp_less:
   694   "c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
   695 by (force simp add: mult_left_mono not_le [symmetric])
   696  
   697 lemma mult_right_less_imp_less:
   698   "a * c < b * c \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
   699 by (force simp add: mult_right_mono not_le [symmetric])
   700 
   701 end
   702 
   703 class linordered_semiring_1 = linordered_semiring + semiring_1
   704 begin
   705 
   706 lemma convex_bound_le:
   707   assumes "x \<le> a" "y \<le> a" "0 \<le> u" "0 \<le> v" "u + v = 1"
   708   shows "u * x + v * y \<le> a"
   709 proof-
   710   from assms have "u * x + v * y \<le> u * a + v * a"
   711     by (simp add: add_mono mult_left_mono)
   712   thus ?thesis using assms unfolding left_distrib[symmetric] by simp
   713 qed
   714 
   715 end
   716 
   717 class linordered_semiring_strict = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add +
   718   assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
   719   assumes mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c"
   720 begin
   721 
   722 subclass semiring_0_cancel ..
   723 
   724 subclass linordered_semiring
   725 proof
   726   fix a b c :: 'a
   727   assume A: "a \<le> b" "0 \<le> c"
   728   from A show "c * a \<le> c * b"
   729     unfolding le_less
   730     using mult_strict_left_mono by (cases "c = 0") auto
   731   from A show "a * c \<le> b * c"
   732     unfolding le_less
   733     using mult_strict_right_mono by (cases "c = 0") auto
   734 qed
   735 
   736 lemma mult_left_le_imp_le:
   737   "c * a \<le> c * b \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
   738 by (force simp add: mult_strict_left_mono _not_less [symmetric])
   739  
   740 lemma mult_right_le_imp_le:
   741   "a * c \<le> b * c \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
   742 by (force simp add: mult_strict_right_mono not_less [symmetric])
   743 
   744 lemma mult_pos_pos: "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a * b"
   745 using mult_strict_left_mono [of 0 b a] by simp
   746 
   747 lemma mult_pos_neg: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> a * b < 0"
   748 using mult_strict_left_mono [of b 0 a] by simp
   749 
   750 lemma mult_neg_pos: "a < 0 \<Longrightarrow> 0 < b \<Longrightarrow> a * b < 0"
   751 using mult_strict_right_mono [of a 0 b] by simp
   752 
   753 text {* Legacy - use @{text mult_neg_pos} *}
   754 lemma mult_pos_neg2: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> b * a < 0" 
   755 by (drule mult_strict_right_mono [of b 0], auto)
   756 
   757 lemma zero_less_mult_pos:
   758   "0 < a * b \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"
   759 apply (cases "b\<le>0")
   760  apply (auto simp add: le_less not_less)
   761 apply (drule_tac mult_pos_neg [of a b])
   762  apply (auto dest: less_not_sym)
   763 done
   764 
   765 lemma zero_less_mult_pos2:
   766   "0 < b * a \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"
   767 apply (cases "b\<le>0")
   768  apply (auto simp add: le_less not_less)
   769 apply (drule_tac mult_pos_neg2 [of a b])
   770  apply (auto dest: less_not_sym)
   771 done
   772 
   773 text{*Strict monotonicity in both arguments*}
   774 lemma mult_strict_mono:
   775   assumes "a < b" and "c < d" and "0 < b" and "0 \<le> c"
   776   shows "a * c < b * d"
   777   using assms apply (cases "c=0")
   778   apply (simp add: mult_pos_pos)
   779   apply (erule mult_strict_right_mono [THEN less_trans])
   780   apply (force simp add: le_less)
   781   apply (erule mult_strict_left_mono, assumption)
   782   done
   783 
   784 text{*This weaker variant has more natural premises*}
   785 lemma mult_strict_mono':
   786   assumes "a < b" and "c < d" and "0 \<le> a" and "0 \<le> c"
   787   shows "a * c < b * d"
   788 by (rule mult_strict_mono) (insert assms, auto)
   789 
   790 lemma mult_less_le_imp_less:
   791   assumes "a < b" and "c \<le> d" and "0 \<le> a" and "0 < c"
   792   shows "a * c < b * d"
   793   using assms apply (subgoal_tac "a * c < b * c")
   794   apply (erule less_le_trans)
   795   apply (erule mult_left_mono)
   796   apply simp
   797   apply (erule mult_strict_right_mono)
   798   apply assumption
   799   done
   800 
   801 lemma mult_le_less_imp_less:
   802   assumes "a \<le> b" and "c < d" and "0 < a" and "0 \<le> c"
   803   shows "a * c < b * d"
   804   using assms apply (subgoal_tac "a * c \<le> b * c")
   805   apply (erule le_less_trans)
   806   apply (erule mult_strict_left_mono)
   807   apply simp
   808   apply (erule mult_right_mono)
   809   apply simp
   810   done
   811 
   812 lemma mult_less_imp_less_left:
   813   assumes less: "c * a < c * b" and nonneg: "0 \<le> c"
   814   shows "a < b"
   815 proof (rule ccontr)
   816   assume "\<not>  a < b"
   817   hence "b \<le> a" by (simp add: linorder_not_less)
   818   hence "c * b \<le> c * a" using nonneg by (rule mult_left_mono)
   819   with this and less show False by (simp add: not_less [symmetric])
   820 qed
   821 
   822 lemma mult_less_imp_less_right:
   823   assumes less: "a * c < b * c" and nonneg: "0 \<le> c"
   824   shows "a < b"
   825 proof (rule ccontr)
   826   assume "\<not> a < b"
   827   hence "b \<le> a" by (simp add: linorder_not_less)
   828   hence "b * c \<le> a * c" using nonneg by (rule mult_right_mono)
   829   with this and less show False by (simp add: not_less [symmetric])
   830 qed  
   831 
   832 end
   833 
   834 class linordered_semiring_1_strict = linordered_semiring_strict + semiring_1
   835 begin
   836 
   837 subclass linordered_semiring_1 ..
   838 
   839 lemma convex_bound_lt:
   840   assumes "x < a" "y < a" "0 \<le> u" "0 \<le> v" "u + v = 1"
   841   shows "u * x + v * y < a"
   842 proof -
   843   from assms have "u * x + v * y < u * a + v * a"
   844     by (cases "u = 0")
   845        (auto intro!: add_less_le_mono mult_strict_left_mono mult_left_mono)
   846   thus ?thesis using assms unfolding left_distrib[symmetric] by simp
   847 qed
   848 
   849 end
   850 
   851 class ordered_comm_semiring = comm_semiring_0 + ordered_ab_semigroup_add + 
   852   assumes comm_mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
   853 begin
   854 
   855 subclass ordered_semiring
   856 proof
   857   fix a b c :: 'a
   858   assume "a \<le> b" "0 \<le> c"
   859   thus "c * a \<le> c * b" by (rule comm_mult_left_mono)
   860   thus "a * c \<le> b * c" by (simp only: mult_commute)
   861 qed
   862 
   863 end
   864 
   865 class ordered_cancel_comm_semiring = ordered_comm_semiring + cancel_comm_monoid_add
   866 begin
   867 
   868 subclass comm_semiring_0_cancel ..
   869 subclass ordered_comm_semiring ..
   870 subclass ordered_cancel_semiring ..
   871 
   872 end
   873 
   874 class linordered_comm_semiring_strict = comm_semiring_0 + linordered_cancel_ab_semigroup_add +
   875   assumes comm_mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
   876 begin
   877 
   878 subclass linordered_semiring_strict
   879 proof
   880   fix a b c :: 'a
   881   assume "a < b" "0 < c"
   882   thus "c * a < c * b" by (rule comm_mult_strict_left_mono)
   883   thus "a * c < b * c" by (simp only: mult_commute)
   884 qed
   885 
   886 subclass ordered_cancel_comm_semiring
   887 proof
   888   fix a b c :: 'a
   889   assume "a \<le> b" "0 \<le> c"
   890   thus "c * a \<le> c * b"
   891     unfolding le_less
   892     using mult_strict_left_mono by (cases "c = 0") auto
   893 qed
   894 
   895 end
   896 
   897 class ordered_ring = ring + ordered_cancel_semiring 
   898 begin
   899 
   900 subclass ordered_ab_group_add ..
   901 
   902 lemma less_add_iff1:
   903   "a * e + c < b * e + d \<longleftrightarrow> (a - b) * e + c < d"
   904 by (simp add: algebra_simps)
   905 
   906 lemma less_add_iff2:
   907   "a * e + c < b * e + d \<longleftrightarrow> c < (b - a) * e + d"
   908 by (simp add: algebra_simps)
   909 
   910 lemma le_add_iff1:
   911   "a * e + c \<le> b * e + d \<longleftrightarrow> (a - b) * e + c \<le> d"
   912 by (simp add: algebra_simps)
   913 
   914 lemma le_add_iff2:
   915   "a * e + c \<le> b * e + d \<longleftrightarrow> c \<le> (b - a) * e + d"
   916 by (simp add: algebra_simps)
   917 
   918 lemma mult_left_mono_neg:
   919   "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> c * a \<le> c * b"
   920   apply (drule mult_left_mono [of _ _ "- c"])
   921   apply simp_all
   922   done
   923 
   924 lemma mult_right_mono_neg:
   925   "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> a * c \<le> b * c"
   926   apply (drule mult_right_mono [of _ _ "- c"])
   927   apply simp_all
   928   done
   929 
   930 lemma mult_nonpos_nonpos: "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> 0 \<le> a * b"
   931 using mult_right_mono_neg [of a 0 b] by simp
   932 
   933 lemma split_mult_pos_le:
   934   "(0 \<le> a \<and> 0 \<le> b) \<or> (a \<le> 0 \<and> b \<le> 0) \<Longrightarrow> 0 \<le> a * b"
   935 by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)
   936 
   937 end
   938 
   939 class linordered_ring = ring + linordered_semiring + linordered_ab_group_add + abs_if
   940 begin
   941 
   942 subclass ordered_ring ..
   943 
   944 subclass ordered_ab_group_add_abs
   945 proof
   946   fix a b
   947   show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
   948     by (auto simp add: abs_if not_less)
   949     (auto simp del: minus_add_distrib simp add: minus_add_distrib [symmetric],
   950      auto intro!: less_imp_le add_neg_neg)
   951 qed (auto simp add: abs_if)
   952 
   953 lemma zero_le_square [simp]: "0 \<le> a * a"
   954   using linear [of 0 a]
   955   by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)
   956 
   957 lemma not_square_less_zero [simp]: "\<not> (a * a < 0)"
   958   by (simp add: not_less)
   959 
   960 end
   961 
   962 (* The "strict" suffix can be seen as describing the combination of linordered_ring and no_zero_divisors.
   963    Basically, linordered_ring + no_zero_divisors = linordered_ring_strict.
   964  *)
   965 class linordered_ring_strict = ring + linordered_semiring_strict
   966   + ordered_ab_group_add + abs_if
   967 begin
   968 
   969 subclass linordered_ring ..
   970 
   971 lemma mult_strict_left_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> c * a < c * b"
   972 using mult_strict_left_mono [of b a "- c"] by simp
   973 
   974 lemma mult_strict_right_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> a * c < b * c"
   975 using mult_strict_right_mono [of b a "- c"] by simp
   976 
   977 lemma mult_neg_neg: "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> 0 < a * b"
   978 using mult_strict_right_mono_neg [of a 0 b] by simp
   979 
   980 subclass ring_no_zero_divisors
   981 proof
   982   fix a b
   983   assume "a \<noteq> 0" then have A: "a < 0 \<or> 0 < a" by (simp add: neq_iff)
   984   assume "b \<noteq> 0" then have B: "b < 0 \<or> 0 < b" by (simp add: neq_iff)
   985   have "a * b < 0 \<or> 0 < a * b"
   986   proof (cases "a < 0")
   987     case True note A' = this
   988     show ?thesis proof (cases "b < 0")
   989       case True with A'
   990       show ?thesis by (auto dest: mult_neg_neg)
   991     next
   992       case False with B have "0 < b" by auto
   993       with A' show ?thesis by (auto dest: mult_strict_right_mono)
   994     qed
   995   next
   996     case False with A have A': "0 < a" by auto
   997     show ?thesis proof (cases "b < 0")
   998       case True with A'
   999       show ?thesis by (auto dest: mult_strict_right_mono_neg)
  1000     next
  1001       case False with B have "0 < b" by auto
  1002       with A' show ?thesis by (auto dest: mult_pos_pos)
  1003     qed
  1004   qed
  1005   then show "a * b \<noteq> 0" by (simp add: neq_iff)
  1006 qed
  1007 
  1008 lemma zero_less_mult_iff:
  1009   "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0"
  1010   apply (auto simp add: mult_pos_pos mult_neg_neg)
  1011   apply (simp_all add: not_less le_less)
  1012   apply (erule disjE) apply assumption defer
  1013   apply (erule disjE) defer apply (drule sym) apply simp
  1014   apply (erule disjE) defer apply (drule sym) apply simp
  1015   apply (erule disjE) apply assumption apply (drule sym) apply simp
  1016   apply (drule sym) apply simp
  1017   apply (blast dest: zero_less_mult_pos)
  1018   apply (blast dest: zero_less_mult_pos2)
  1019   done
  1020 
  1021 lemma zero_le_mult_iff:
  1022   "0 \<le> a * b \<longleftrightarrow> 0 \<le> a \<and> 0 \<le> b \<or> a \<le> 0 \<and> b \<le> 0"
  1023 by (auto simp add: eq_commute [of 0] le_less not_less zero_less_mult_iff)
  1024 
  1025 lemma mult_less_0_iff:
  1026   "a * b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b"
  1027   apply (insert zero_less_mult_iff [of "-a" b])
  1028   apply force
  1029   done
  1030 
  1031 lemma mult_le_0_iff:
  1032   "a * b \<le> 0 \<longleftrightarrow> 0 \<le> a \<and> b \<le> 0 \<or> a \<le> 0 \<and> 0 \<le> b"
  1033   apply (insert zero_le_mult_iff [of "-a" b]) 
  1034   apply force
  1035   done
  1036 
  1037 text{*Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"},
  1038    also with the relations @{text "\<le>"} and equality.*}
  1039 
  1040 text{*These ``disjunction'' versions produce two cases when the comparison is
  1041  an assumption, but effectively four when the comparison is a goal.*}
  1042 
  1043 lemma mult_less_cancel_right_disj:
  1044   "a * c < b * c \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"
  1045   apply (cases "c = 0")
  1046   apply (auto simp add: neq_iff mult_strict_right_mono 
  1047                       mult_strict_right_mono_neg)
  1048   apply (auto simp add: not_less 
  1049                       not_le [symmetric, of "a*c"]
  1050                       not_le [symmetric, of a])
  1051   apply (erule_tac [!] notE)
  1052   apply (auto simp add: less_imp_le mult_right_mono 
  1053                       mult_right_mono_neg)
  1054   done
  1055 
  1056 lemma mult_less_cancel_left_disj:
  1057   "c * a < c * b \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"
  1058   apply (cases "c = 0")
  1059   apply (auto simp add: neq_iff mult_strict_left_mono 
  1060                       mult_strict_left_mono_neg)
  1061   apply (auto simp add: not_less 
  1062                       not_le [symmetric, of "c*a"]
  1063                       not_le [symmetric, of a])
  1064   apply (erule_tac [!] notE)
  1065   apply (auto simp add: less_imp_le mult_left_mono 
  1066                       mult_left_mono_neg)
  1067   done
  1068 
  1069 text{*The ``conjunction of implication'' lemmas produce two cases when the
  1070 comparison is a goal, but give four when the comparison is an assumption.*}
  1071 
  1072 lemma mult_less_cancel_right:
  1073   "a * c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)"
  1074   using mult_less_cancel_right_disj [of a c b] by auto
  1075 
  1076 lemma mult_less_cancel_left:
  1077   "c * a < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)"
  1078   using mult_less_cancel_left_disj [of c a b] by auto
  1079 
  1080 lemma mult_le_cancel_right:
  1081    "a * c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
  1082 by (simp add: not_less [symmetric] mult_less_cancel_right_disj)
  1083 
  1084 lemma mult_le_cancel_left:
  1085   "c * a \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
  1086 by (simp add: not_less [symmetric] mult_less_cancel_left_disj)
  1087 
  1088 lemma mult_le_cancel_left_pos:
  1089   "0 < c \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> a \<le> b"
  1090 by (auto simp: mult_le_cancel_left)
  1091 
  1092 lemma mult_le_cancel_left_neg:
  1093   "c < 0 \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> b \<le> a"
  1094 by (auto simp: mult_le_cancel_left)
  1095 
  1096 lemma mult_less_cancel_left_pos:
  1097   "0 < c \<Longrightarrow> c * a < c * b \<longleftrightarrow> a < b"
  1098 by (auto simp: mult_less_cancel_left)
  1099 
  1100 lemma mult_less_cancel_left_neg:
  1101   "c < 0 \<Longrightarrow> c * a < c * b \<longleftrightarrow> b < a"
  1102 by (auto simp: mult_less_cancel_left)
  1103 
  1104 end
  1105 
  1106 lemmas mult_sign_intros =
  1107   mult_nonneg_nonneg mult_nonneg_nonpos
  1108   mult_nonpos_nonneg mult_nonpos_nonpos
  1109   mult_pos_pos mult_pos_neg
  1110   mult_neg_pos mult_neg_neg
  1111 
  1112 class ordered_comm_ring = comm_ring + ordered_comm_semiring
  1113 begin
  1114 
  1115 subclass ordered_ring ..
  1116 subclass ordered_cancel_comm_semiring ..
  1117 
  1118 end
  1119 
  1120 class linordered_semidom = comm_semiring_1_cancel + linordered_comm_semiring_strict +
  1121   (*previously linordered_semiring*)
  1122   assumes zero_less_one [simp]: "0 < 1"
  1123 begin
  1124 
  1125 lemma pos_add_strict:
  1126   shows "0 < a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
  1127   using add_strict_mono [of 0 a b c] by simp
  1128 
  1129 lemma zero_le_one [simp]: "0 \<le> 1"
  1130 by (rule zero_less_one [THEN less_imp_le]) 
  1131 
  1132 lemma not_one_le_zero [simp]: "\<not> 1 \<le> 0"
  1133 by (simp add: not_le) 
  1134 
  1135 lemma not_one_less_zero [simp]: "\<not> 1 < 0"
  1136 by (simp add: not_less) 
  1137 
  1138 lemma less_1_mult:
  1139   assumes "1 < m" and "1 < n"
  1140   shows "1 < m * n"
  1141   using assms mult_strict_mono [of 1 m 1 n]
  1142     by (simp add:  less_trans [OF zero_less_one]) 
  1143 
  1144 end
  1145 
  1146 class linordered_idom = comm_ring_1 +
  1147   linordered_comm_semiring_strict + ordered_ab_group_add +
  1148   abs_if + sgn_if
  1149   (*previously linordered_ring*)
  1150 begin
  1151 
  1152 subclass linordered_semiring_1_strict ..
  1153 subclass linordered_ring_strict ..
  1154 subclass ordered_comm_ring ..
  1155 subclass idom ..
  1156 
  1157 subclass linordered_semidom
  1158 proof
  1159   have "0 \<le> 1 * 1" by (rule zero_le_square)
  1160   thus "0 < 1" by (simp add: le_less)
  1161 qed 
  1162 
  1163 lemma linorder_neqE_linordered_idom:
  1164   assumes "x \<noteq> y" obtains "x < y" | "y < x"
  1165   using assms by (rule neqE)
  1166 
  1167 text {* These cancellation simprules also produce two cases when the comparison is a goal. *}
  1168 
  1169 lemma mult_le_cancel_right1:
  1170   "c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)"
  1171 by (insert mult_le_cancel_right [of 1 c b], simp)
  1172 
  1173 lemma mult_le_cancel_right2:
  1174   "a * c \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)"
  1175 by (insert mult_le_cancel_right [of a c 1], simp)
  1176 
  1177 lemma mult_le_cancel_left1:
  1178   "c \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)"
  1179 by (insert mult_le_cancel_left [of c 1 b], simp)
  1180 
  1181 lemma mult_le_cancel_left2:
  1182   "c * a \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)"
  1183 by (insert mult_le_cancel_left [of c a 1], simp)
  1184 
  1185 lemma mult_less_cancel_right1:
  1186   "c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)"
  1187 by (insert mult_less_cancel_right [of 1 c b], simp)
  1188 
  1189 lemma mult_less_cancel_right2:
  1190   "a * c < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"
  1191 by (insert mult_less_cancel_right [of a c 1], simp)
  1192 
  1193 lemma mult_less_cancel_left1:
  1194   "c < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)"
  1195 by (insert mult_less_cancel_left [of c 1 b], simp)
  1196 
  1197 lemma mult_less_cancel_left2:
  1198   "c * a < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"
  1199 by (insert mult_less_cancel_left [of c a 1], simp)
  1200 
  1201 lemma sgn_sgn [simp]:
  1202   "sgn (sgn a) = sgn a"
  1203 unfolding sgn_if by simp
  1204 
  1205 lemma sgn_0_0:
  1206   "sgn a = 0 \<longleftrightarrow> a = 0"
  1207 unfolding sgn_if by simp
  1208 
  1209 lemma sgn_1_pos:
  1210   "sgn a = 1 \<longleftrightarrow> a > 0"
  1211 unfolding sgn_if by simp
  1212 
  1213 lemma sgn_1_neg:
  1214   "sgn a = - 1 \<longleftrightarrow> a < 0"
  1215 unfolding sgn_if by auto
  1216 
  1217 lemma sgn_pos [simp]:
  1218   "0 < a \<Longrightarrow> sgn a = 1"
  1219 unfolding sgn_1_pos .
  1220 
  1221 lemma sgn_neg [simp]:
  1222   "a < 0 \<Longrightarrow> sgn a = - 1"
  1223 unfolding sgn_1_neg .
  1224 
  1225 lemma sgn_times:
  1226   "sgn (a * b) = sgn a * sgn b"
  1227 by (auto simp add: sgn_if zero_less_mult_iff)
  1228 
  1229 lemma abs_sgn: "\<bar>k\<bar> = k * sgn k"
  1230 unfolding sgn_if abs_if by auto
  1231 
  1232 lemma sgn_greater [simp]:
  1233   "0 < sgn a \<longleftrightarrow> 0 < a"
  1234   unfolding sgn_if by auto
  1235 
  1236 lemma sgn_less [simp]:
  1237   "sgn a < 0 \<longleftrightarrow> a < 0"
  1238   unfolding sgn_if by auto
  1239 
  1240 lemma abs_dvd_iff [simp]: "\<bar>m\<bar> dvd k \<longleftrightarrow> m dvd k"
  1241   by (simp add: abs_if)
  1242 
  1243 lemma dvd_abs_iff [simp]: "m dvd \<bar>k\<bar> \<longleftrightarrow> m dvd k"
  1244   by (simp add: abs_if)
  1245 
  1246 lemma dvd_if_abs_eq:
  1247   "\<bar>l\<bar> = \<bar>k\<bar> \<Longrightarrow> l dvd k"
  1248 by(subst abs_dvd_iff[symmetric]) simp
  1249 
  1250 end
  1251 
  1252 text {* Simprules for comparisons where common factors can be cancelled. *}
  1253 
  1254 lemmas mult_compare_simps[no_atp] =
  1255     mult_le_cancel_right mult_le_cancel_left
  1256     mult_le_cancel_right1 mult_le_cancel_right2
  1257     mult_le_cancel_left1 mult_le_cancel_left2
  1258     mult_less_cancel_right mult_less_cancel_left
  1259     mult_less_cancel_right1 mult_less_cancel_right2
  1260     mult_less_cancel_left1 mult_less_cancel_left2
  1261     mult_cancel_right mult_cancel_left
  1262     mult_cancel_right1 mult_cancel_right2
  1263     mult_cancel_left1 mult_cancel_left2
  1264 
  1265 text {* Reasoning about inequalities with division *}
  1266 
  1267 context linordered_semidom
  1268 begin
  1269 
  1270 lemma less_add_one: "a < a + 1"
  1271 proof -
  1272   have "a + 0 < a + 1"
  1273     by (blast intro: zero_less_one add_strict_left_mono)
  1274   thus ?thesis by simp
  1275 qed
  1276 
  1277 lemma zero_less_two: "0 < 1 + 1"
  1278 by (blast intro: less_trans zero_less_one less_add_one)
  1279 
  1280 end
  1281 
  1282 context linordered_idom
  1283 begin
  1284 
  1285 lemma mult_right_le_one_le:
  1286   "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> x * y \<le> x"
  1287   by (auto simp add: mult_le_cancel_left2)
  1288 
  1289 lemma mult_left_le_one_le:
  1290   "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> y * x \<le> x"
  1291   by (auto simp add: mult_le_cancel_right2)
  1292 
  1293 end
  1294 
  1295 text {* Absolute Value *}
  1296 
  1297 context linordered_idom
  1298 begin
  1299 
  1300 lemma mult_sgn_abs:
  1301   "sgn x * \<bar>x\<bar> = x"
  1302   unfolding abs_if sgn_if by auto
  1303 
  1304 lemma abs_one [simp]:
  1305   "\<bar>1\<bar> = 1"
  1306   by (simp add: abs_if zero_less_one [THEN less_not_sym])
  1307 
  1308 end
  1309 
  1310 class ordered_ring_abs = ordered_ring + ordered_ab_group_add_abs +
  1311   assumes abs_eq_mult:
  1312     "(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>"
  1313 
  1314 context linordered_idom
  1315 begin
  1316 
  1317 subclass ordered_ring_abs proof
  1318 qed (auto simp add: abs_if not_less mult_less_0_iff)
  1319 
  1320 lemma abs_mult:
  1321   "\<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>" 
  1322   by (rule abs_eq_mult) auto
  1323 
  1324 lemma abs_mult_self:
  1325   "\<bar>a\<bar> * \<bar>a\<bar> = a * a"
  1326   by (simp add: abs_if) 
  1327 
  1328 lemma abs_mult_less:
  1329   "\<bar>a\<bar> < c \<Longrightarrow> \<bar>b\<bar> < d \<Longrightarrow> \<bar>a\<bar> * \<bar>b\<bar> < c * d"
  1330 proof -
  1331   assume ac: "\<bar>a\<bar> < c"
  1332   hence cpos: "0<c" by (blast intro: le_less_trans abs_ge_zero)
  1333   assume "\<bar>b\<bar> < d"
  1334   thus ?thesis by (simp add: ac cpos mult_strict_mono) 
  1335 qed
  1336 
  1337 lemma less_minus_self_iff:
  1338   "a < - a \<longleftrightarrow> a < 0"
  1339   by (simp only: less_le less_eq_neg_nonpos equal_neg_zero)
  1340 
  1341 lemma abs_less_iff:
  1342   "\<bar>a\<bar> < b \<longleftrightarrow> a < b \<and> - a < b" 
  1343   by (simp add: less_le abs_le_iff) (auto simp add: abs_if)
  1344 
  1345 lemma abs_mult_pos:
  1346   "0 \<le> x \<Longrightarrow> \<bar>y\<bar> * x = \<bar>y * x\<bar>"
  1347   by (simp add: abs_mult)
  1348 
  1349 end
  1350 
  1351 code_modulename SML
  1352   Rings Arith
  1353 
  1354 code_modulename OCaml
  1355   Rings Arith
  1356 
  1357 code_modulename Haskell
  1358   Rings Arith
  1359 
  1360 end