src/HOL/Rings.thy
author huffman
Mon May 17 08:45:46 2010 -0700 (2010-05-17)
changeset 36970 fb3fdb4b585e
parent 36821 9207505d1ee5
child 36977 71c8973a604b
permissions -rw-r--r--
remove simp attribute from square_eq_1_iff
     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 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 class mult_mono = times + zero + ord +
   632   assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
   633   assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"
   634 
   635 text {*
   636   The theory of partially ordered rings is taken from the books:
   637   \begin{itemize}
   638   \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979 
   639   \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963
   640   \end{itemize}
   641   Most of the used notions can also be looked up in 
   642   \begin{itemize}
   643   \item \url{http://www.mathworld.com} by Eric Weisstein et. al.
   644   \item \emph{Algebra I} by van der Waerden, Springer.
   645   \end{itemize}
   646 *}
   647 
   648 class ordered_semiring = mult_mono + semiring_0 + ordered_ab_semigroup_add 
   649 begin
   650 
   651 lemma mult_mono:
   652   "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> c
   653      \<Longrightarrow> a * c \<le> b * d"
   654 apply (erule mult_right_mono [THEN order_trans], assumption)
   655 apply (erule mult_left_mono, assumption)
   656 done
   657 
   658 lemma mult_mono':
   659   "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> c
   660      \<Longrightarrow> a * c \<le> b * d"
   661 apply (rule mult_mono)
   662 apply (fast intro: order_trans)+
   663 done
   664 
   665 end
   666 
   667 class ordered_cancel_semiring = mult_mono + ordered_ab_semigroup_add
   668   + semiring + cancel_comm_monoid_add
   669 begin
   670 
   671 subclass semiring_0_cancel ..
   672 subclass ordered_semiring ..
   673 
   674 lemma mult_nonneg_nonneg: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b"
   675 using mult_left_mono [of 0 b a] by simp
   676 
   677 lemma mult_nonneg_nonpos: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> a * b \<le> 0"
   678 using mult_left_mono [of b 0 a] by simp
   679 
   680 lemma mult_nonpos_nonneg: "a \<le> 0 \<Longrightarrow> 0 \<le> b \<Longrightarrow> a * b \<le> 0"
   681 using mult_right_mono [of a 0 b] by simp
   682 
   683 text {* Legacy - use @{text mult_nonpos_nonneg} *}
   684 lemma mult_nonneg_nonpos2: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> b * a \<le> 0" 
   685 by (drule mult_right_mono [of b 0], auto)
   686 
   687 lemma split_mult_neg_le: "(0 \<le> a & b \<le> 0) | (a \<le> 0 & 0 \<le> b) \<Longrightarrow> a * b \<le> 0" 
   688 by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)
   689 
   690 end
   691 
   692 class linordered_semiring = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add + mult_mono
   693 begin
   694 
   695 subclass ordered_cancel_semiring ..
   696 
   697 subclass ordered_comm_monoid_add ..
   698 
   699 lemma mult_left_less_imp_less:
   700   "c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
   701 by (force simp add: mult_left_mono not_le [symmetric])
   702  
   703 lemma mult_right_less_imp_less:
   704   "a * c < b * c \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
   705 by (force simp add: mult_right_mono not_le [symmetric])
   706 
   707 end
   708 
   709 class linordered_semiring_1 = linordered_semiring + semiring_1
   710 begin
   711 
   712 lemma convex_bound_le:
   713   assumes "x \<le> a" "y \<le> a" "0 \<le> u" "0 \<le> v" "u + v = 1"
   714   shows "u * x + v * y \<le> a"
   715 proof-
   716   from assms have "u * x + v * y \<le> u * a + v * a"
   717     by (simp add: add_mono mult_left_mono)
   718   thus ?thesis using assms unfolding left_distrib[symmetric] by simp
   719 qed
   720 
   721 end
   722 
   723 class linordered_semiring_strict = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add +
   724   assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
   725   assumes mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c"
   726 begin
   727 
   728 subclass semiring_0_cancel ..
   729 
   730 subclass linordered_semiring
   731 proof
   732   fix a b c :: 'a
   733   assume A: "a \<le> b" "0 \<le> c"
   734   from A show "c * a \<le> c * b"
   735     unfolding le_less
   736     using mult_strict_left_mono by (cases "c = 0") auto
   737   from A show "a * c \<le> b * c"
   738     unfolding le_less
   739     using mult_strict_right_mono by (cases "c = 0") auto
   740 qed
   741 
   742 lemma mult_left_le_imp_le:
   743   "c * a \<le> c * b \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
   744 by (force simp add: mult_strict_left_mono _not_less [symmetric])
   745  
   746 lemma mult_right_le_imp_le:
   747   "a * c \<le> b * c \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
   748 by (force simp add: mult_strict_right_mono not_less [symmetric])
   749 
   750 lemma mult_pos_pos: "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a * b"
   751 using mult_strict_left_mono [of 0 b a] by simp
   752 
   753 lemma mult_pos_neg: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> a * b < 0"
   754 using mult_strict_left_mono [of b 0 a] by simp
   755 
   756 lemma mult_neg_pos: "a < 0 \<Longrightarrow> 0 < b \<Longrightarrow> a * b < 0"
   757 using mult_strict_right_mono [of a 0 b] by simp
   758 
   759 text {* Legacy - use @{text mult_neg_pos} *}
   760 lemma mult_pos_neg2: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> b * a < 0" 
   761 by (drule mult_strict_right_mono [of b 0], auto)
   762 
   763 lemma zero_less_mult_pos:
   764   "0 < a * b \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"
   765 apply (cases "b\<le>0")
   766  apply (auto simp add: le_less not_less)
   767 apply (drule_tac mult_pos_neg [of a b])
   768  apply (auto dest: less_not_sym)
   769 done
   770 
   771 lemma zero_less_mult_pos2:
   772   "0 < b * a \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"
   773 apply (cases "b\<le>0")
   774  apply (auto simp add: le_less not_less)
   775 apply (drule_tac mult_pos_neg2 [of a b])
   776  apply (auto dest: less_not_sym)
   777 done
   778 
   779 text{*Strict monotonicity in both arguments*}
   780 lemma mult_strict_mono:
   781   assumes "a < b" and "c < d" and "0 < b" and "0 \<le> c"
   782   shows "a * c < b * d"
   783   using assms apply (cases "c=0")
   784   apply (simp add: mult_pos_pos)
   785   apply (erule mult_strict_right_mono [THEN less_trans])
   786   apply (force simp add: le_less)
   787   apply (erule mult_strict_left_mono, assumption)
   788   done
   789 
   790 text{*This weaker variant has more natural premises*}
   791 lemma mult_strict_mono':
   792   assumes "a < b" and "c < d" and "0 \<le> a" and "0 \<le> c"
   793   shows "a * c < b * d"
   794 by (rule mult_strict_mono) (insert assms, auto)
   795 
   796 lemma mult_less_le_imp_less:
   797   assumes "a < b" and "c \<le> d" and "0 \<le> a" and "0 < c"
   798   shows "a * c < b * d"
   799   using assms apply (subgoal_tac "a * c < b * c")
   800   apply (erule less_le_trans)
   801   apply (erule mult_left_mono)
   802   apply simp
   803   apply (erule mult_strict_right_mono)
   804   apply assumption
   805   done
   806 
   807 lemma mult_le_less_imp_less:
   808   assumes "a \<le> b" and "c < d" and "0 < a" and "0 \<le> c"
   809   shows "a * c < b * d"
   810   using assms apply (subgoal_tac "a * c \<le> b * c")
   811   apply (erule le_less_trans)
   812   apply (erule mult_strict_left_mono)
   813   apply simp
   814   apply (erule mult_right_mono)
   815   apply simp
   816   done
   817 
   818 lemma mult_less_imp_less_left:
   819   assumes less: "c * a < c * b" and nonneg: "0 \<le> c"
   820   shows "a < b"
   821 proof (rule ccontr)
   822   assume "\<not>  a < b"
   823   hence "b \<le> a" by (simp add: linorder_not_less)
   824   hence "c * b \<le> c * a" using nonneg by (rule mult_left_mono)
   825   with this and less show False by (simp add: not_less [symmetric])
   826 qed
   827 
   828 lemma mult_less_imp_less_right:
   829   assumes less: "a * c < b * c" and nonneg: "0 \<le> c"
   830   shows "a < b"
   831 proof (rule ccontr)
   832   assume "\<not> a < b"
   833   hence "b \<le> a" by (simp add: linorder_not_less)
   834   hence "b * c \<le> a * c" using nonneg by (rule mult_right_mono)
   835   with this and less show False by (simp add: not_less [symmetric])
   836 qed  
   837 
   838 end
   839 
   840 class linordered_semiring_1_strict = linordered_semiring_strict + semiring_1
   841 begin
   842 
   843 subclass linordered_semiring_1 ..
   844 
   845 lemma convex_bound_lt:
   846   assumes "x < a" "y < a" "0 \<le> u" "0 \<le> v" "u + v = 1"
   847   shows "u * x + v * y < a"
   848 proof -
   849   from assms have "u * x + v * y < u * a + v * a"
   850     by (cases "u = 0")
   851        (auto intro!: add_less_le_mono mult_strict_left_mono mult_left_mono)
   852   thus ?thesis using assms unfolding left_distrib[symmetric] by simp
   853 qed
   854 
   855 end
   856 
   857 class mult_mono1 = times + zero + ord +
   858   assumes mult_mono1: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
   859 
   860 class ordered_comm_semiring = comm_semiring_0
   861   + ordered_ab_semigroup_add + mult_mono1
   862 begin
   863 
   864 subclass ordered_semiring
   865 proof
   866   fix a b c :: 'a
   867   assume "a \<le> b" "0 \<le> c"
   868   thus "c * a \<le> c * b" by (rule mult_mono1)
   869   thus "a * c \<le> b * c" by (simp only: mult_commute)
   870 qed
   871 
   872 end
   873 
   874 class ordered_cancel_comm_semiring = comm_semiring_0_cancel
   875   + ordered_ab_semigroup_add + mult_mono1
   876 begin
   877 
   878 subclass ordered_comm_semiring ..
   879 subclass ordered_cancel_semiring ..
   880 
   881 end
   882 
   883 class linordered_comm_semiring_strict = comm_semiring_0 + linordered_cancel_ab_semigroup_add +
   884   assumes mult_strict_left_mono_comm: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
   885 begin
   886 
   887 subclass linordered_semiring_strict
   888 proof
   889   fix a b c :: 'a
   890   assume "a < b" "0 < c"
   891   thus "c * a < c * b" by (rule mult_strict_left_mono_comm)
   892   thus "a * c < b * c" by (simp only: mult_commute)
   893 qed
   894 
   895 subclass ordered_cancel_comm_semiring
   896 proof
   897   fix a b c :: 'a
   898   assume "a \<le> b" "0 \<le> c"
   899   thus "c * a \<le> c * b"
   900     unfolding le_less
   901     using mult_strict_left_mono by (cases "c = 0") auto
   902 qed
   903 
   904 end
   905 
   906 class ordered_ring = ring + ordered_cancel_semiring 
   907 begin
   908 
   909 subclass ordered_ab_group_add ..
   910 
   911 lemma less_add_iff1:
   912   "a * e + c < b * e + d \<longleftrightarrow> (a - b) * e + c < d"
   913 by (simp add: algebra_simps)
   914 
   915 lemma less_add_iff2:
   916   "a * e + c < b * e + d \<longleftrightarrow> c < (b - a) * e + d"
   917 by (simp add: algebra_simps)
   918 
   919 lemma le_add_iff1:
   920   "a * e + c \<le> b * e + d \<longleftrightarrow> (a - b) * e + c \<le> d"
   921 by (simp add: algebra_simps)
   922 
   923 lemma le_add_iff2:
   924   "a * e + c \<le> b * e + d \<longleftrightarrow> c \<le> (b - a) * e + d"
   925 by (simp add: algebra_simps)
   926 
   927 lemma mult_left_mono_neg:
   928   "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> c * a \<le> c * b"
   929   apply (drule mult_left_mono [of _ _ "- c"])
   930   apply simp_all
   931   done
   932 
   933 lemma mult_right_mono_neg:
   934   "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> a * c \<le> b * c"
   935   apply (drule mult_right_mono [of _ _ "- c"])
   936   apply simp_all
   937   done
   938 
   939 lemma mult_nonpos_nonpos: "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> 0 \<le> a * b"
   940 using mult_right_mono_neg [of a 0 b] by simp
   941 
   942 lemma split_mult_pos_le:
   943   "(0 \<le> a \<and> 0 \<le> b) \<or> (a \<le> 0 \<and> b \<le> 0) \<Longrightarrow> 0 \<le> a * b"
   944 by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)
   945 
   946 end
   947 
   948 class linordered_ring = ring + linordered_semiring + linordered_ab_group_add + abs_if
   949 begin
   950 
   951 subclass ordered_ring ..
   952 
   953 subclass ordered_ab_group_add_abs
   954 proof
   955   fix a b
   956   show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
   957     by (auto simp add: abs_if not_less)
   958     (auto simp del: minus_add_distrib simp add: minus_add_distrib [symmetric],
   959      auto intro: add_nonneg_nonneg, auto intro!: less_imp_le add_neg_neg)
   960 qed (auto simp add: abs_if)
   961 
   962 lemma zero_le_square [simp]: "0 \<le> a * a"
   963   using linear [of 0 a]
   964   by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)
   965 
   966 lemma not_square_less_zero [simp]: "\<not> (a * a < 0)"
   967   by (simp add: not_less)
   968 
   969 end
   970 
   971 (* The "strict" suffix can be seen as describing the combination of linordered_ring and no_zero_divisors.
   972    Basically, linordered_ring + no_zero_divisors = linordered_ring_strict.
   973  *)
   974 class linordered_ring_strict = ring + linordered_semiring_strict
   975   + ordered_ab_group_add + abs_if
   976 begin
   977 
   978 subclass linordered_ring ..
   979 
   980 lemma mult_strict_left_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> c * a < c * b"
   981 using mult_strict_left_mono [of b a "- c"] by simp
   982 
   983 lemma mult_strict_right_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> a * c < b * c"
   984 using mult_strict_right_mono [of b a "- c"] by simp
   985 
   986 lemma mult_neg_neg: "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> 0 < a * b"
   987 using mult_strict_right_mono_neg [of a 0 b] by simp
   988 
   989 subclass ring_no_zero_divisors
   990 proof
   991   fix a b
   992   assume "a \<noteq> 0" then have A: "a < 0 \<or> 0 < a" by (simp add: neq_iff)
   993   assume "b \<noteq> 0" then have B: "b < 0 \<or> 0 < b" by (simp add: neq_iff)
   994   have "a * b < 0 \<or> 0 < a * b"
   995   proof (cases "a < 0")
   996     case True note A' = this
   997     show ?thesis proof (cases "b < 0")
   998       case True with A'
   999       show ?thesis by (auto dest: mult_neg_neg)
  1000     next
  1001       case False with B have "0 < b" by auto
  1002       with A' show ?thesis by (auto dest: mult_strict_right_mono)
  1003     qed
  1004   next
  1005     case False with A have A': "0 < a" by auto
  1006     show ?thesis proof (cases "b < 0")
  1007       case True with A'
  1008       show ?thesis by (auto dest: mult_strict_right_mono_neg)
  1009     next
  1010       case False with B have "0 < b" by auto
  1011       with A' show ?thesis by (auto dest: mult_pos_pos)
  1012     qed
  1013   qed
  1014   then show "a * b \<noteq> 0" by (simp add: neq_iff)
  1015 qed
  1016 
  1017 lemma zero_less_mult_iff:
  1018   "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0"
  1019   apply (auto simp add: mult_pos_pos mult_neg_neg)
  1020   apply (simp_all add: not_less le_less)
  1021   apply (erule disjE) apply assumption defer
  1022   apply (erule disjE) defer apply (drule sym) apply simp
  1023   apply (erule disjE) defer apply (drule sym) apply simp
  1024   apply (erule disjE) apply assumption apply (drule sym) apply simp
  1025   apply (drule sym) apply simp
  1026   apply (blast dest: zero_less_mult_pos)
  1027   apply (blast dest: zero_less_mult_pos2)
  1028   done
  1029 
  1030 lemma zero_le_mult_iff:
  1031   "0 \<le> a * b \<longleftrightarrow> 0 \<le> a \<and> 0 \<le> b \<or> a \<le> 0 \<and> b \<le> 0"
  1032 by (auto simp add: eq_commute [of 0] le_less not_less zero_less_mult_iff)
  1033 
  1034 lemma mult_less_0_iff:
  1035   "a * b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b"
  1036   apply (insert zero_less_mult_iff [of "-a" b])
  1037   apply force
  1038   done
  1039 
  1040 lemma mult_le_0_iff:
  1041   "a * b \<le> 0 \<longleftrightarrow> 0 \<le> a \<and> b \<le> 0 \<or> a \<le> 0 \<and> 0 \<le> b"
  1042   apply (insert zero_le_mult_iff [of "-a" b]) 
  1043   apply force
  1044   done
  1045 
  1046 text{*Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"},
  1047    also with the relations @{text "\<le>"} and equality.*}
  1048 
  1049 text{*These ``disjunction'' versions produce two cases when the comparison is
  1050  an assumption, but effectively four when the comparison is a goal.*}
  1051 
  1052 lemma mult_less_cancel_right_disj:
  1053   "a * c < b * c \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"
  1054   apply (cases "c = 0")
  1055   apply (auto simp add: neq_iff mult_strict_right_mono 
  1056                       mult_strict_right_mono_neg)
  1057   apply (auto simp add: not_less 
  1058                       not_le [symmetric, of "a*c"]
  1059                       not_le [symmetric, of a])
  1060   apply (erule_tac [!] notE)
  1061   apply (auto simp add: less_imp_le mult_right_mono 
  1062                       mult_right_mono_neg)
  1063   done
  1064 
  1065 lemma mult_less_cancel_left_disj:
  1066   "c * a < c * b \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"
  1067   apply (cases "c = 0")
  1068   apply (auto simp add: neq_iff mult_strict_left_mono 
  1069                       mult_strict_left_mono_neg)
  1070   apply (auto simp add: not_less 
  1071                       not_le [symmetric, of "c*a"]
  1072                       not_le [symmetric, of a])
  1073   apply (erule_tac [!] notE)
  1074   apply (auto simp add: less_imp_le mult_left_mono 
  1075                       mult_left_mono_neg)
  1076   done
  1077 
  1078 text{*The ``conjunction of implication'' lemmas produce two cases when the
  1079 comparison is a goal, but give four when the comparison is an assumption.*}
  1080 
  1081 lemma mult_less_cancel_right:
  1082   "a * c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)"
  1083   using mult_less_cancel_right_disj [of a c b] by auto
  1084 
  1085 lemma mult_less_cancel_left:
  1086   "c * a < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)"
  1087   using mult_less_cancel_left_disj [of c a b] by auto
  1088 
  1089 lemma mult_le_cancel_right:
  1090    "a * c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
  1091 by (simp add: not_less [symmetric] mult_less_cancel_right_disj)
  1092 
  1093 lemma mult_le_cancel_left:
  1094   "c * a \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
  1095 by (simp add: not_less [symmetric] mult_less_cancel_left_disj)
  1096 
  1097 lemma mult_le_cancel_left_pos:
  1098   "0 < c \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> a \<le> b"
  1099 by (auto simp: mult_le_cancel_left)
  1100 
  1101 lemma mult_le_cancel_left_neg:
  1102   "c < 0 \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> b \<le> a"
  1103 by (auto simp: mult_le_cancel_left)
  1104 
  1105 lemma mult_less_cancel_left_pos:
  1106   "0 < c \<Longrightarrow> c * a < c * b \<longleftrightarrow> a < b"
  1107 by (auto simp: mult_less_cancel_left)
  1108 
  1109 lemma mult_less_cancel_left_neg:
  1110   "c < 0 \<Longrightarrow> c * a < c * b \<longleftrightarrow> b < a"
  1111 by (auto simp: mult_less_cancel_left)
  1112 
  1113 end
  1114 
  1115 lemmas mult_sign_intros =
  1116   mult_nonneg_nonneg mult_nonneg_nonpos
  1117   mult_nonpos_nonneg mult_nonpos_nonpos
  1118   mult_pos_pos mult_pos_neg
  1119   mult_neg_pos mult_neg_neg
  1120 
  1121 class ordered_comm_ring = comm_ring + ordered_comm_semiring
  1122 begin
  1123 
  1124 subclass ordered_ring ..
  1125 subclass ordered_cancel_comm_semiring ..
  1126 
  1127 end
  1128 
  1129 class linordered_semidom = comm_semiring_1_cancel + linordered_comm_semiring_strict +
  1130   (*previously linordered_semiring*)
  1131   assumes zero_less_one [simp]: "0 < 1"
  1132 begin
  1133 
  1134 lemma pos_add_strict:
  1135   shows "0 < a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
  1136   using add_strict_mono [of 0 a b c] by simp
  1137 
  1138 lemma zero_le_one [simp]: "0 \<le> 1"
  1139 by (rule zero_less_one [THEN less_imp_le]) 
  1140 
  1141 lemma not_one_le_zero [simp]: "\<not> 1 \<le> 0"
  1142 by (simp add: not_le) 
  1143 
  1144 lemma not_one_less_zero [simp]: "\<not> 1 < 0"
  1145 by (simp add: not_less) 
  1146 
  1147 lemma less_1_mult:
  1148   assumes "1 < m" and "1 < n"
  1149   shows "1 < m * n"
  1150   using assms mult_strict_mono [of 1 m 1 n]
  1151     by (simp add:  less_trans [OF zero_less_one]) 
  1152 
  1153 end
  1154 
  1155 class linordered_idom = comm_ring_1 +
  1156   linordered_comm_semiring_strict + ordered_ab_group_add +
  1157   abs_if + sgn_if
  1158   (*previously linordered_ring*)
  1159 begin
  1160 
  1161 subclass linordered_semiring_1_strict ..
  1162 subclass linordered_ring_strict ..
  1163 subclass ordered_comm_ring ..
  1164 subclass idom ..
  1165 
  1166 subclass linordered_semidom
  1167 proof
  1168   have "0 \<le> 1 * 1" by (rule zero_le_square)
  1169   thus "0 < 1" by (simp add: le_less)
  1170 qed 
  1171 
  1172 lemma linorder_neqE_linordered_idom:
  1173   assumes "x \<noteq> y" obtains "x < y" | "y < x"
  1174   using assms by (rule neqE)
  1175 
  1176 text {* These cancellation simprules also produce two cases when the comparison is a goal. *}
  1177 
  1178 lemma mult_le_cancel_right1:
  1179   "c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)"
  1180 by (insert mult_le_cancel_right [of 1 c b], simp)
  1181 
  1182 lemma mult_le_cancel_right2:
  1183   "a * c \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)"
  1184 by (insert mult_le_cancel_right [of a c 1], simp)
  1185 
  1186 lemma mult_le_cancel_left1:
  1187   "c \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)"
  1188 by (insert mult_le_cancel_left [of c 1 b], simp)
  1189 
  1190 lemma mult_le_cancel_left2:
  1191   "c * a \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)"
  1192 by (insert mult_le_cancel_left [of c a 1], simp)
  1193 
  1194 lemma mult_less_cancel_right1:
  1195   "c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)"
  1196 by (insert mult_less_cancel_right [of 1 c b], simp)
  1197 
  1198 lemma mult_less_cancel_right2:
  1199   "a * c < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"
  1200 by (insert mult_less_cancel_right [of a c 1], simp)
  1201 
  1202 lemma mult_less_cancel_left1:
  1203   "c < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)"
  1204 by (insert mult_less_cancel_left [of c 1 b], simp)
  1205 
  1206 lemma mult_less_cancel_left2:
  1207   "c * a < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"
  1208 by (insert mult_less_cancel_left [of c a 1], simp)
  1209 
  1210 lemma sgn_sgn [simp]:
  1211   "sgn (sgn a) = sgn a"
  1212 unfolding sgn_if by simp
  1213 
  1214 lemma sgn_0_0:
  1215   "sgn a = 0 \<longleftrightarrow> a = 0"
  1216 unfolding sgn_if by simp
  1217 
  1218 lemma sgn_1_pos:
  1219   "sgn a = 1 \<longleftrightarrow> a > 0"
  1220 unfolding sgn_if by simp
  1221 
  1222 lemma sgn_1_neg:
  1223   "sgn a = - 1 \<longleftrightarrow> a < 0"
  1224 unfolding sgn_if by auto
  1225 
  1226 lemma sgn_pos [simp]:
  1227   "0 < a \<Longrightarrow> sgn a = 1"
  1228 unfolding sgn_1_pos .
  1229 
  1230 lemma sgn_neg [simp]:
  1231   "a < 0 \<Longrightarrow> sgn a = - 1"
  1232 unfolding sgn_1_neg .
  1233 
  1234 lemma sgn_times:
  1235   "sgn (a * b) = sgn a * sgn b"
  1236 by (auto simp add: sgn_if zero_less_mult_iff)
  1237 
  1238 lemma abs_sgn: "\<bar>k\<bar> = k * sgn k"
  1239 unfolding sgn_if abs_if by auto
  1240 
  1241 lemma sgn_greater [simp]:
  1242   "0 < sgn a \<longleftrightarrow> 0 < a"
  1243   unfolding sgn_if by auto
  1244 
  1245 lemma sgn_less [simp]:
  1246   "sgn a < 0 \<longleftrightarrow> a < 0"
  1247   unfolding sgn_if by auto
  1248 
  1249 lemma abs_dvd_iff [simp]: "\<bar>m\<bar> dvd k \<longleftrightarrow> m dvd k"
  1250   by (simp add: abs_if)
  1251 
  1252 lemma dvd_abs_iff [simp]: "m dvd \<bar>k\<bar> \<longleftrightarrow> m dvd k"
  1253   by (simp add: abs_if)
  1254 
  1255 lemma dvd_if_abs_eq:
  1256   "\<bar>l\<bar> = \<bar>k\<bar> \<Longrightarrow> l dvd k"
  1257 by(subst abs_dvd_iff[symmetric]) simp
  1258 
  1259 end
  1260 
  1261 text {* Simprules for comparisons where common factors can be cancelled. *}
  1262 
  1263 lemmas mult_compare_simps[no_atp] =
  1264     mult_le_cancel_right mult_le_cancel_left
  1265     mult_le_cancel_right1 mult_le_cancel_right2
  1266     mult_le_cancel_left1 mult_le_cancel_left2
  1267     mult_less_cancel_right mult_less_cancel_left
  1268     mult_less_cancel_right1 mult_less_cancel_right2
  1269     mult_less_cancel_left1 mult_less_cancel_left2
  1270     mult_cancel_right mult_cancel_left
  1271     mult_cancel_right1 mult_cancel_right2
  1272     mult_cancel_left1 mult_cancel_left2
  1273 
  1274 text {* Reasoning about inequalities with division *}
  1275 
  1276 context linordered_semidom
  1277 begin
  1278 
  1279 lemma less_add_one: "a < a + 1"
  1280 proof -
  1281   have "a + 0 < a + 1"
  1282     by (blast intro: zero_less_one add_strict_left_mono)
  1283   thus ?thesis by simp
  1284 qed
  1285 
  1286 lemma zero_less_two: "0 < 1 + 1"
  1287 by (blast intro: less_trans zero_less_one less_add_one)
  1288 
  1289 end
  1290 
  1291 context linordered_idom
  1292 begin
  1293 
  1294 lemma mult_right_le_one_le:
  1295   "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> x * y \<le> x"
  1296   by (auto simp add: mult_le_cancel_left2)
  1297 
  1298 lemma mult_left_le_one_le:
  1299   "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> y * x \<le> x"
  1300   by (auto simp add: mult_le_cancel_right2)
  1301 
  1302 end
  1303 
  1304 text {* Absolute Value *}
  1305 
  1306 context linordered_idom
  1307 begin
  1308 
  1309 lemma mult_sgn_abs:
  1310   "sgn x * \<bar>x\<bar> = x"
  1311   unfolding abs_if sgn_if by auto
  1312 
  1313 lemma abs_one [simp]:
  1314   "\<bar>1\<bar> = 1"
  1315   by (simp add: abs_if zero_less_one [THEN less_not_sym])
  1316 
  1317 end
  1318 
  1319 class ordered_ring_abs = ordered_ring + ordered_ab_group_add_abs +
  1320   assumes abs_eq_mult:
  1321     "(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>"
  1322 
  1323 context linordered_idom
  1324 begin
  1325 
  1326 subclass ordered_ring_abs proof
  1327 qed (auto simp add: abs_if not_less mult_less_0_iff)
  1328 
  1329 lemma abs_mult:
  1330   "\<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>" 
  1331   by (rule abs_eq_mult) auto
  1332 
  1333 lemma abs_mult_self:
  1334   "\<bar>a\<bar> * \<bar>a\<bar> = a * a"
  1335   by (simp add: abs_if) 
  1336 
  1337 lemma abs_mult_less:
  1338   "\<bar>a\<bar> < c \<Longrightarrow> \<bar>b\<bar> < d \<Longrightarrow> \<bar>a\<bar> * \<bar>b\<bar> < c * d"
  1339 proof -
  1340   assume ac: "\<bar>a\<bar> < c"
  1341   hence cpos: "0<c" by (blast intro: le_less_trans abs_ge_zero)
  1342   assume "\<bar>b\<bar> < d"
  1343   thus ?thesis by (simp add: ac cpos mult_strict_mono) 
  1344 qed
  1345 
  1346 lemma less_minus_self_iff:
  1347   "a < - a \<longleftrightarrow> a < 0"
  1348   by (simp only: less_le less_eq_neg_nonpos equal_neg_zero)
  1349 
  1350 lemma abs_less_iff:
  1351   "\<bar>a\<bar> < b \<longleftrightarrow> a < b \<and> - a < b" 
  1352   by (simp add: less_le abs_le_iff) (auto simp add: abs_if)
  1353 
  1354 lemma abs_mult_pos:
  1355   "0 \<le> x \<Longrightarrow> \<bar>y\<bar> * x = \<bar>y * x\<bar>"
  1356   by (simp add: abs_mult)
  1357 
  1358 end
  1359 
  1360 code_modulename SML
  1361   Rings Arith
  1362 
  1363 code_modulename OCaml
  1364   Rings Arith
  1365 
  1366 code_modulename Haskell
  1367   Rings Arith
  1368 
  1369 end