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