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