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