src/HOL/Ring_and_Field.thy
author nipkow
Thu Dec 11 08:52:50 2008 +0100 (2008-12-11)
changeset 29106 25e28a4070f3
parent 28823 dcbef866c9e2
child 29406 54bac26089bd
permissions -rw-r--r--
Testfile for Stefan's code generator
     1 (*  Title:   HOL/Ring_and_Field.thy
     2     ID:      $Id$
     3     Author:  Gertrud Bauer, Steven Obua, Tobias Nipkow, Lawrence C Paulson, and Markus Wenzel,
     4              with contributions by Jeremy Avigad
     5 *)
     6 
     7 header {* (Ordered) Rings and Fields *}
     8 
     9 theory Ring_and_Field
    10 imports OrderedGroup
    11 begin
    12 
    13 text {*
    14   The theory of partially ordered rings is taken from the books:
    15   \begin{itemize}
    16   \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979 
    17   \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963
    18   \end{itemize}
    19   Most of the used notions can also be looked up in 
    20   \begin{itemize}
    21   \item \url{http://www.mathworld.com} by Eric Weisstein et. al.
    22   \item \emph{Algebra I} by van der Waerden, Springer.
    23   \end{itemize}
    24 *}
    25 
    26 class semiring = ab_semigroup_add + semigroup_mult +
    27   assumes left_distrib: "(a + b) * c = a * c + b * c"
    28   assumes right_distrib: "a * (b + c) = a * b + a * c"
    29 begin
    30 
    31 text{*For the @{text combine_numerals} simproc*}
    32 lemma combine_common_factor:
    33   "a * e + (b * e + c) = (a + b) * e + c"
    34   by (simp add: left_distrib add_ac)
    35 
    36 end
    37 
    38 class mult_zero = times + zero +
    39   assumes mult_zero_left [simp]: "0 * a = 0"
    40   assumes mult_zero_right [simp]: "a * 0 = 0"
    41 
    42 class semiring_0 = semiring + comm_monoid_add + mult_zero
    43 
    44 class semiring_0_cancel = semiring + comm_monoid_add + cancel_ab_semigroup_add
    45 begin
    46 
    47 subclass semiring_0
    48 proof
    49   fix a :: 'a
    50   have "0 * a + 0 * a = 0 * a + 0"
    51     by (simp add: left_distrib [symmetric])
    52   thus "0 * a = 0"
    53     by (simp only: add_left_cancel)
    54 next
    55   fix a :: 'a
    56   have "a * 0 + a * 0 = a * 0 + 0"
    57     by (simp add: right_distrib [symmetric])
    58   thus "a * 0 = 0"
    59     by (simp only: add_left_cancel)
    60 qed
    61 
    62 end
    63 
    64 class comm_semiring = ab_semigroup_add + ab_semigroup_mult +
    65   assumes distrib: "(a + b) * c = a * c + b * c"
    66 begin
    67 
    68 subclass semiring
    69 proof
    70   fix a b c :: 'a
    71   show "(a + b) * c = a * c + b * c" by (simp add: distrib)
    72   have "a * (b + c) = (b + c) * a" by (simp add: mult_ac)
    73   also have "... = b * a + c * a" by (simp only: distrib)
    74   also have "... = a * b + a * c" by (simp add: mult_ac)
    75   finally show "a * (b + c) = a * b + a * c" by blast
    76 qed
    77 
    78 end
    79 
    80 class comm_semiring_0 = comm_semiring + comm_monoid_add + mult_zero
    81 begin
    82 
    83 subclass semiring_0 ..
    84 
    85 end
    86 
    87 class comm_semiring_0_cancel = comm_semiring + comm_monoid_add + cancel_ab_semigroup_add
    88 begin
    89 
    90 subclass semiring_0_cancel ..
    91 
    92 subclass comm_semiring_0 ..
    93 
    94 end
    95 
    96 class zero_neq_one = zero + one +
    97   assumes zero_neq_one [simp]: "0 \<noteq> 1"
    98 begin
    99 
   100 lemma one_neq_zero [simp]: "1 \<noteq> 0"
   101   by (rule not_sym) (rule zero_neq_one)
   102 
   103 end
   104 
   105 class semiring_1 = zero_neq_one + semiring_0 + monoid_mult
   106 
   107 text {* Abstract divisibility *}
   108 
   109 class dvd = times
   110 begin
   111 
   112 definition dvd :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "dvd" 50) where
   113   [code del]: "b dvd a \<longleftrightarrow> (\<exists>k. a = b * k)"
   114 
   115 lemma dvdI [intro?]: "a = b * k \<Longrightarrow> b dvd a"
   116   unfolding dvd_def ..
   117 
   118 lemma dvdE [elim?]: "b dvd a \<Longrightarrow> (\<And>k. a = b * k \<Longrightarrow> P) \<Longrightarrow> P"
   119   unfolding dvd_def by blast 
   120 
   121 end
   122 
   123 class comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult + dvd
   124   (*previously almost_semiring*)
   125 begin
   126 
   127 subclass semiring_1 ..
   128 
   129 lemma dvd_refl: "a dvd a"
   130 proof
   131   show "a = a * 1" by simp
   132 qed
   133 
   134 lemma dvd_trans:
   135   assumes "a dvd b" and "b dvd c"
   136   shows "a dvd c"
   137 proof -
   138   from assms obtain v where "b = a * v" by (auto elim!: dvdE)
   139   moreover from assms obtain w where "c = b * w" by (auto elim!: dvdE)
   140   ultimately have "c = a * (v * w)" by (simp add: mult_assoc)
   141   then show ?thesis ..
   142 qed
   143 
   144 lemma dvd_0_left_iff [noatp, simp]: "0 dvd a \<longleftrightarrow> a = 0"
   145   by (auto intro: dvd_refl elim!: dvdE)
   146 
   147 lemma dvd_0_right [iff]: "a dvd 0"
   148 proof
   149   show "0 = a * 0" by simp
   150 qed
   151 
   152 lemma one_dvd [simp]: "1 dvd a"
   153   by (auto intro!: dvdI)
   154 
   155 lemma dvd_mult: "a dvd c \<Longrightarrow> a dvd (b * c)"
   156   by (auto intro!: mult_left_commute dvdI elim!: dvdE)
   157 
   158 lemma dvd_mult2: "a dvd b \<Longrightarrow> a dvd (b * c)"
   159   apply (subst mult_commute)
   160   apply (erule dvd_mult)
   161   done
   162 
   163 lemma dvd_triv_right [simp]: "a dvd b * a"
   164   by (rule dvd_mult) (rule dvd_refl)
   165 
   166 lemma dvd_triv_left [simp]: "a dvd a * b"
   167   by (rule dvd_mult2) (rule dvd_refl)
   168 
   169 lemma mult_dvd_mono:
   170   assumes ab: "a dvd b"
   171     and "cd": "c dvd d"
   172   shows "a * c dvd b * d"
   173 proof -
   174   from ab obtain b' where "b = a * b'" ..
   175   moreover from "cd" obtain d' where "d = c * d'" ..
   176   ultimately have "b * d = (a * c) * (b' * d')" by (simp add: mult_ac)
   177   then show ?thesis ..
   178 qed
   179 
   180 lemma dvd_mult_left: "a * b dvd c \<Longrightarrow> a dvd c"
   181   by (simp add: dvd_def mult_assoc, blast)
   182 
   183 lemma dvd_mult_right: "a * b dvd c \<Longrightarrow> b dvd c"
   184   unfolding mult_ac [of a] by (rule dvd_mult_left)
   185 
   186 lemma dvd_0_left: "0 dvd a \<Longrightarrow> a = 0"
   187   by simp
   188 
   189 lemma dvd_add:
   190   assumes ab: "a dvd b"
   191     and ac: "a dvd c"
   192     shows "a dvd (b + c)"
   193 proof -
   194   from ab obtain b' where "b = a * b'" ..
   195   moreover from ac obtain c' where "c = a * c'" ..
   196   ultimately have "b + c = a * (b' + c')" by (simp add: right_distrib)
   197   then show ?thesis ..
   198 qed
   199 
   200 end
   201 
   202 class no_zero_divisors = zero + times +
   203   assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
   204 
   205 class semiring_1_cancel = semiring + comm_monoid_add + zero_neq_one
   206   + cancel_ab_semigroup_add + monoid_mult
   207 begin
   208 
   209 subclass semiring_0_cancel ..
   210 
   211 subclass semiring_1 ..
   212 
   213 end
   214 
   215 class comm_semiring_1_cancel = comm_semiring + comm_monoid_add + comm_monoid_mult
   216   + zero_neq_one + cancel_ab_semigroup_add
   217 begin
   218 
   219 subclass semiring_1_cancel ..
   220 subclass comm_semiring_0_cancel ..
   221 subclass comm_semiring_1 ..
   222 
   223 end
   224 
   225 class ring = semiring + ab_group_add
   226 begin
   227 
   228 subclass semiring_0_cancel ..
   229 
   230 text {* Distribution rules *}
   231 
   232 lemma minus_mult_left: "- (a * b) = - a * b"
   233   by (rule equals_zero_I) (simp add: left_distrib [symmetric]) 
   234 
   235 lemma minus_mult_right: "- (a * b) = a * - b"
   236   by (rule equals_zero_I) (simp add: right_distrib [symmetric]) 
   237 
   238 lemma minus_mult_minus [simp]: "- a * - b = a * b"
   239   by (simp add: minus_mult_left [symmetric] minus_mult_right [symmetric])
   240 
   241 lemma minus_mult_commute: "- a * b = a * - b"
   242   by (simp add: minus_mult_left [symmetric] minus_mult_right [symmetric])
   243 
   244 lemma right_diff_distrib: "a * (b - c) = a * b - a * c"
   245   by (simp add: right_distrib diff_minus 
   246     minus_mult_left [symmetric] minus_mult_right [symmetric]) 
   247 
   248 lemma left_diff_distrib: "(a - b) * c = a * c - b * c"
   249   by (simp add: left_distrib diff_minus 
   250     minus_mult_left [symmetric] minus_mult_right [symmetric]) 
   251 
   252 lemmas ring_distribs =
   253   right_distrib left_distrib left_diff_distrib right_diff_distrib
   254 
   255 lemmas ring_simps =
   256   add_ac
   257   add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2
   258   diff_eq_eq eq_diff_eq diff_minus [symmetric] uminus_add_conv_diff
   259   ring_distribs
   260 
   261 lemma eq_add_iff1:
   262   "a * e + c = b * e + d \<longleftrightarrow> (a - b) * e + c = d"
   263   by (simp add: ring_simps)
   264 
   265 lemma eq_add_iff2:
   266   "a * e + c = b * e + d \<longleftrightarrow> c = (b - a) * e + d"
   267   by (simp add: ring_simps)
   268 
   269 end
   270 
   271 lemmas ring_distribs =
   272   right_distrib left_distrib left_diff_distrib right_diff_distrib
   273 
   274 class comm_ring = comm_semiring + ab_group_add
   275 begin
   276 
   277 subclass ring ..
   278 subclass comm_semiring_0_cancel ..
   279 
   280 end
   281 
   282 class ring_1 = ring + zero_neq_one + monoid_mult
   283 begin
   284 
   285 subclass semiring_1_cancel ..
   286 
   287 end
   288 
   289 class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult
   290   (*previously ring*)
   291 begin
   292 
   293 subclass ring_1 ..
   294 subclass comm_semiring_1_cancel ..
   295 
   296 end
   297 
   298 class ring_no_zero_divisors = ring + no_zero_divisors
   299 begin
   300 
   301 lemma mult_eq_0_iff [simp]:
   302   shows "a * b = 0 \<longleftrightarrow> (a = 0 \<or> b = 0)"
   303 proof (cases "a = 0 \<or> b = 0")
   304   case False then have "a \<noteq> 0" and "b \<noteq> 0" by auto
   305     then show ?thesis using no_zero_divisors by simp
   306 next
   307   case True then show ?thesis by auto
   308 qed
   309 
   310 text{*Cancellation of equalities with a common factor*}
   311 lemma mult_cancel_right [simp, noatp]:
   312   "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b"
   313 proof -
   314   have "(a * c = b * c) = ((a - b) * c = 0)"
   315     by (simp add: ring_distribs right_minus_eq)
   316   thus ?thesis
   317     by (simp add: disj_commute right_minus_eq)
   318 qed
   319 
   320 lemma mult_cancel_left [simp, noatp]:
   321   "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b"
   322 proof -
   323   have "(c * a = c * b) = (c * (a - b) = 0)"
   324     by (simp add: ring_distribs right_minus_eq)
   325   thus ?thesis
   326     by (simp add: right_minus_eq)
   327 qed
   328 
   329 end
   330 
   331 class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors
   332 begin
   333 
   334 lemma mult_cancel_right1 [simp]:
   335   "c = b * c \<longleftrightarrow> c = 0 \<or> b = 1"
   336   by (insert mult_cancel_right [of 1 c b], force)
   337 
   338 lemma mult_cancel_right2 [simp]:
   339   "a * c = c \<longleftrightarrow> c = 0 \<or> a = 1"
   340   by (insert mult_cancel_right [of a c 1], simp)
   341  
   342 lemma mult_cancel_left1 [simp]:
   343   "c = c * b \<longleftrightarrow> c = 0 \<or> b = 1"
   344   by (insert mult_cancel_left [of c 1 b], force)
   345 
   346 lemma mult_cancel_left2 [simp]:
   347   "c * a = c \<longleftrightarrow> c = 0 \<or> a = 1"
   348   by (insert mult_cancel_left [of c a 1], simp)
   349 
   350 end
   351 
   352 class idom = comm_ring_1 + no_zero_divisors
   353 begin
   354 
   355 subclass ring_1_no_zero_divisors ..
   356 
   357 end
   358 
   359 class division_ring = ring_1 + inverse +
   360   assumes left_inverse [simp]:  "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
   361   assumes right_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> a * inverse a = 1"
   362 begin
   363 
   364 subclass ring_1_no_zero_divisors
   365 proof
   366   fix a b :: 'a
   367   assume a: "a \<noteq> 0" and b: "b \<noteq> 0"
   368   show "a * b \<noteq> 0"
   369   proof
   370     assume ab: "a * b = 0"
   371     hence "0 = inverse a * (a * b) * inverse b"
   372       by simp
   373     also have "\<dots> = (inverse a * a) * (b * inverse b)"
   374       by (simp only: mult_assoc)
   375     also have "\<dots> = 1"
   376       using a b by simp
   377     finally show False
   378       by simp
   379   qed
   380 qed
   381 
   382 lemma nonzero_imp_inverse_nonzero:
   383   "a \<noteq> 0 \<Longrightarrow> inverse a \<noteq> 0"
   384 proof
   385   assume ianz: "inverse a = 0"
   386   assume "a \<noteq> 0"
   387   hence "1 = a * inverse a" by simp
   388   also have "... = 0" by (simp add: ianz)
   389   finally have "1 = 0" .
   390   thus False by (simp add: eq_commute)
   391 qed
   392 
   393 lemma inverse_zero_imp_zero:
   394   "inverse a = 0 \<Longrightarrow> a = 0"
   395 apply (rule classical)
   396 apply (drule nonzero_imp_inverse_nonzero)
   397 apply auto
   398 done
   399 
   400 lemma nonzero_inverse_minus_eq:
   401   assumes "a \<noteq> 0"
   402   shows "inverse (- a) = - inverse a"
   403 proof -
   404   have "- a * inverse (- a) = - a * - inverse a"
   405     using assms by simp
   406   then show ?thesis unfolding mult_cancel_left using assms by simp 
   407 qed
   408 
   409 lemma nonzero_inverse_inverse_eq:
   410   assumes "a \<noteq> 0"
   411   shows "inverse (inverse a) = a"
   412 proof -
   413   have "(inverse (inverse a) * inverse a) * a = a" 
   414     using assms by (simp add: nonzero_imp_inverse_nonzero)
   415   then show ?thesis using assms by (simp add: mult_assoc)
   416 qed
   417 
   418 lemma nonzero_inverse_eq_imp_eq:
   419   assumes inveq: "inverse a = inverse b"
   420     and anz:  "a \<noteq> 0"
   421     and bnz:  "b \<noteq> 0"
   422   shows "a = b"
   423 proof -
   424   have "a * inverse b = a * inverse a"
   425     by (simp add: inveq)
   426   hence "(a * inverse b) * b = (a * inverse a) * b"
   427     by simp
   428   then show "a = b"
   429     by (simp add: mult_assoc anz bnz)
   430 qed
   431 
   432 lemma inverse_1 [simp]: "inverse 1 = 1"
   433 proof -
   434   have "inverse 1 * 1 = 1" 
   435     by (rule left_inverse) (rule one_neq_zero)
   436   then show ?thesis by simp
   437 qed
   438 
   439 lemma inverse_unique: 
   440   assumes ab: "a * b = 1"
   441   shows "inverse a = b"
   442 proof -
   443   have "a \<noteq> 0" using ab by (cases "a = 0") simp_all
   444   moreover have "inverse a * (a * b) = inverse a" by (simp add: ab) 
   445   ultimately show ?thesis by (simp add: mult_assoc [symmetric]) 
   446 qed
   447 
   448 lemma nonzero_inverse_mult_distrib: 
   449   assumes anz: "a \<noteq> 0"
   450     and bnz: "b \<noteq> 0"
   451   shows "inverse (a * b) = inverse b * inverse a"
   452 proof -
   453   have "inverse (a * b) * (a * b) * inverse b = inverse b" 
   454     by (simp add: anz bnz)
   455   hence "inverse (a * b) * a = inverse b" 
   456     by (simp add: mult_assoc bnz)
   457   hence "inverse (a * b) * a * inverse a = inverse b * inverse a" 
   458     by simp
   459   thus ?thesis
   460     by (simp add: mult_assoc anz)
   461 qed
   462 
   463 lemma division_ring_inverse_add:
   464   "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a + inverse b = inverse a * (a + b) * inverse b"
   465   by (simp add: ring_simps mult_assoc)
   466 
   467 lemma division_ring_inverse_diff:
   468   "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a - inverse b = inverse a * (b - a) * inverse b"
   469   by (simp add: ring_simps mult_assoc)
   470 
   471 end
   472 
   473 class field = comm_ring_1 + inverse +
   474   assumes field_inverse:  "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
   475   assumes divide_inverse: "a / b = a * inverse b"
   476 begin
   477 
   478 subclass division_ring
   479 proof
   480   fix a :: 'a
   481   assume "a \<noteq> 0"
   482   thus "inverse a * a = 1" by (rule field_inverse)
   483   thus "a * inverse a = 1" by (simp only: mult_commute)
   484 qed
   485 
   486 subclass idom ..
   487 
   488 lemma right_inverse_eq: "b \<noteq> 0 \<Longrightarrow> a / b = 1 \<longleftrightarrow> a = b"
   489 proof
   490   assume neq: "b \<noteq> 0"
   491   {
   492     hence "a = (a / b) * b" by (simp add: divide_inverse mult_ac)
   493     also assume "a / b = 1"
   494     finally show "a = b" by simp
   495   next
   496     assume "a = b"
   497     with neq show "a / b = 1" by (simp add: divide_inverse)
   498   }
   499 qed
   500 
   501 lemma nonzero_inverse_eq_divide: "a \<noteq> 0 \<Longrightarrow> inverse a = 1 / a"
   502   by (simp add: divide_inverse)
   503 
   504 lemma divide_self [simp]: "a \<noteq> 0 \<Longrightarrow> a / a = 1"
   505   by (simp add: divide_inverse)
   506 
   507 lemma divide_zero_left [simp]: "0 / a = 0"
   508   by (simp add: divide_inverse)
   509 
   510 lemma inverse_eq_divide: "inverse a = 1 / a"
   511   by (simp add: divide_inverse)
   512 
   513 lemma add_divide_distrib: "(a+b) / c = a/c + b/c"
   514   by (simp add: divide_inverse ring_distribs) 
   515 
   516 end
   517 
   518 class division_by_zero = zero + inverse +
   519   assumes inverse_zero [simp]: "inverse 0 = 0"
   520 
   521 lemma divide_zero [simp]:
   522   "a / 0 = (0::'a::{field,division_by_zero})"
   523   by (simp add: divide_inverse)
   524 
   525 lemma divide_self_if [simp]:
   526   "a / (a::'a::{field,division_by_zero}) = (if a=0 then 0 else 1)"
   527   by simp
   528 
   529 class mult_mono = times + zero + ord +
   530   assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
   531   assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"
   532 
   533 class pordered_semiring = mult_mono + semiring_0 + pordered_ab_semigroup_add 
   534 begin
   535 
   536 lemma mult_mono:
   537   "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> c
   538      \<Longrightarrow> a * c \<le> b * d"
   539 apply (erule mult_right_mono [THEN order_trans], assumption)
   540 apply (erule mult_left_mono, assumption)
   541 done
   542 
   543 lemma mult_mono':
   544   "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> c
   545      \<Longrightarrow> a * c \<le> b * d"
   546 apply (rule mult_mono)
   547 apply (fast intro: order_trans)+
   548 done
   549 
   550 end
   551 
   552 class pordered_cancel_semiring = mult_mono + pordered_ab_semigroup_add
   553   + semiring + comm_monoid_add + cancel_ab_semigroup_add
   554 begin
   555 
   556 subclass semiring_0_cancel ..
   557 subclass pordered_semiring ..
   558 
   559 lemma mult_nonneg_nonneg: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b"
   560   by (drule mult_left_mono [of zero b], auto)
   561 
   562 lemma mult_nonneg_nonpos: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> a * b \<le> 0"
   563   by (drule mult_left_mono [of b zero], auto)
   564 
   565 lemma mult_nonneg_nonpos2: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> b * a \<le> 0" 
   566   by (drule mult_right_mono [of b zero], auto)
   567 
   568 lemma split_mult_neg_le: "(0 \<le> a & b \<le> 0) | (a \<le> 0 & 0 \<le> b) \<Longrightarrow> a * b \<le> 0" 
   569   by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)
   570 
   571 end
   572 
   573 class ordered_semiring = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add + mult_mono
   574 begin
   575 
   576 subclass pordered_cancel_semiring ..
   577 
   578 subclass pordered_comm_monoid_add ..
   579 
   580 lemma mult_left_less_imp_less:
   581   "c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
   582   by (force simp add: mult_left_mono not_le [symmetric])
   583  
   584 lemma mult_right_less_imp_less:
   585   "a * c < b * c \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
   586   by (force simp add: mult_right_mono not_le [symmetric])
   587 
   588 end
   589 
   590 class ordered_semiring_strict = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add +
   591   assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
   592   assumes mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c"
   593 begin
   594 
   595 subclass semiring_0_cancel ..
   596 
   597 subclass ordered_semiring
   598 proof
   599   fix a b c :: 'a
   600   assume A: "a \<le> b" "0 \<le> c"
   601   from A show "c * a \<le> c * b"
   602     unfolding le_less
   603     using mult_strict_left_mono by (cases "c = 0") auto
   604   from A show "a * c \<le> b * c"
   605     unfolding le_less
   606     using mult_strict_right_mono by (cases "c = 0") auto
   607 qed
   608 
   609 lemma mult_left_le_imp_le:
   610   "c * a \<le> c * b \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
   611   by (force simp add: mult_strict_left_mono _not_less [symmetric])
   612  
   613 lemma mult_right_le_imp_le:
   614   "a * c \<le> b * c \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
   615   by (force simp add: mult_strict_right_mono not_less [symmetric])
   616 
   617 lemma mult_pos_pos:
   618   "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a * b"
   619   by (drule mult_strict_left_mono [of zero b], auto)
   620 
   621 lemma mult_pos_neg:
   622   "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> a * b < 0"
   623   by (drule mult_strict_left_mono [of b zero], auto)
   624 
   625 lemma mult_pos_neg2:
   626   "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> b * a < 0" 
   627   by (drule mult_strict_right_mono [of b zero], auto)
   628 
   629 lemma zero_less_mult_pos:
   630   "0 < a * b \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"
   631 apply (cases "b\<le>0") 
   632  apply (auto simp add: le_less not_less)
   633 apply (drule_tac mult_pos_neg [of a b]) 
   634  apply (auto dest: less_not_sym)
   635 done
   636 
   637 lemma zero_less_mult_pos2:
   638   "0 < b * a \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"
   639 apply (cases "b\<le>0") 
   640  apply (auto simp add: le_less not_less)
   641 apply (drule_tac mult_pos_neg2 [of a b]) 
   642  apply (auto dest: less_not_sym)
   643 done
   644 
   645 text{*Strict monotonicity in both arguments*}
   646 lemma mult_strict_mono:
   647   assumes "a < b" and "c < d" and "0 < b" and "0 \<le> c"
   648   shows "a * c < b * d"
   649   using assms apply (cases "c=0")
   650   apply (simp add: mult_pos_pos) 
   651   apply (erule mult_strict_right_mono [THEN less_trans])
   652   apply (force simp add: le_less) 
   653   apply (erule mult_strict_left_mono, assumption)
   654   done
   655 
   656 text{*This weaker variant has more natural premises*}
   657 lemma mult_strict_mono':
   658   assumes "a < b" and "c < d" and "0 \<le> a" and "0 \<le> c"
   659   shows "a * c < b * d"
   660   by (rule mult_strict_mono) (insert assms, auto)
   661 
   662 lemma mult_less_le_imp_less:
   663   assumes "a < b" and "c \<le> d" and "0 \<le> a" and "0 < c"
   664   shows "a * c < b * d"
   665   using assms apply (subgoal_tac "a * c < b * c")
   666   apply (erule less_le_trans)
   667   apply (erule mult_left_mono)
   668   apply simp
   669   apply (erule mult_strict_right_mono)
   670   apply assumption
   671   done
   672 
   673 lemma mult_le_less_imp_less:
   674   assumes "a \<le> b" and "c < d" and "0 < a" and "0 \<le> c"
   675   shows "a * c < b * d"
   676   using assms apply (subgoal_tac "a * c \<le> b * c")
   677   apply (erule le_less_trans)
   678   apply (erule mult_strict_left_mono)
   679   apply simp
   680   apply (erule mult_right_mono)
   681   apply simp
   682   done
   683 
   684 lemma mult_less_imp_less_left:
   685   assumes less: "c * a < c * b" and nonneg: "0 \<le> c"
   686   shows "a < b"
   687 proof (rule ccontr)
   688   assume "\<not>  a < b"
   689   hence "b \<le> a" by (simp add: linorder_not_less)
   690   hence "c * b \<le> c * a" using nonneg by (rule mult_left_mono)
   691   with this and less show False 
   692     by (simp add: not_less [symmetric])
   693 qed
   694 
   695 lemma mult_less_imp_less_right:
   696   assumes less: "a * c < b * c" and nonneg: "0 \<le> c"
   697   shows "a < b"
   698 proof (rule ccontr)
   699   assume "\<not> a < b"
   700   hence "b \<le> a" by (simp add: linorder_not_less)
   701   hence "b * c \<le> a * c" using nonneg by (rule mult_right_mono)
   702   with this and less show False 
   703     by (simp add: not_less [symmetric])
   704 qed  
   705 
   706 end
   707 
   708 class mult_mono1 = times + zero + ord +
   709   assumes mult_mono1: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
   710 
   711 class pordered_comm_semiring = comm_semiring_0
   712   + pordered_ab_semigroup_add + mult_mono1
   713 begin
   714 
   715 subclass pordered_semiring
   716 proof
   717   fix a b c :: 'a
   718   assume "a \<le> b" "0 \<le> c"
   719   thus "c * a \<le> c * b" by (rule mult_mono1)
   720   thus "a * c \<le> b * c" by (simp only: mult_commute)
   721 qed
   722 
   723 end
   724 
   725 class pordered_cancel_comm_semiring = comm_semiring_0_cancel
   726   + pordered_ab_semigroup_add + mult_mono1
   727 begin
   728 
   729 subclass pordered_comm_semiring ..
   730 subclass pordered_cancel_semiring ..
   731 
   732 end
   733 
   734 class ordered_comm_semiring_strict = comm_semiring_0 + ordered_cancel_ab_semigroup_add +
   735   assumes mult_strict_left_mono_comm: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
   736 begin
   737 
   738 subclass ordered_semiring_strict
   739 proof
   740   fix a b c :: 'a
   741   assume "a < b" "0 < c"
   742   thus "c * a < c * b" by (rule mult_strict_left_mono_comm)
   743   thus "a * c < b * c" by (simp only: mult_commute)
   744 qed
   745 
   746 subclass pordered_cancel_comm_semiring
   747 proof
   748   fix a b c :: 'a
   749   assume "a \<le> b" "0 \<le> c"
   750   thus "c * a \<le> c * b"
   751     unfolding le_less
   752     using mult_strict_left_mono by (cases "c = 0") auto
   753 qed
   754 
   755 end
   756 
   757 class pordered_ring = ring + pordered_cancel_semiring 
   758 begin
   759 
   760 subclass pordered_ab_group_add ..
   761 
   762 lemmas ring_simps = ring_simps group_simps
   763 
   764 lemma less_add_iff1:
   765   "a * e + c < b * e + d \<longleftrightarrow> (a - b) * e + c < d"
   766   by (simp add: ring_simps)
   767 
   768 lemma less_add_iff2:
   769   "a * e + c < b * e + d \<longleftrightarrow> c < (b - a) * e + d"
   770   by (simp add: ring_simps)
   771 
   772 lemma le_add_iff1:
   773   "a * e + c \<le> b * e + d \<longleftrightarrow> (a - b) * e + c \<le> d"
   774   by (simp add: ring_simps)
   775 
   776 lemma le_add_iff2:
   777   "a * e + c \<le> b * e + d \<longleftrightarrow> c \<le> (b - a) * e + d"
   778   by (simp add: ring_simps)
   779 
   780 lemma mult_left_mono_neg:
   781   "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> c * a \<le> c * b"
   782   apply (drule mult_left_mono [of _ _ "uminus c"])
   783   apply (simp_all add: minus_mult_left [symmetric]) 
   784   done
   785 
   786 lemma mult_right_mono_neg:
   787   "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> a * c \<le> b * c"
   788   apply (drule mult_right_mono [of _ _ "uminus c"])
   789   apply (simp_all add: minus_mult_right [symmetric]) 
   790   done
   791 
   792 lemma mult_nonpos_nonpos:
   793   "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> 0 \<le> a * b"
   794   by (drule mult_right_mono_neg [of a zero b]) auto
   795 
   796 lemma split_mult_pos_le:
   797   "(0 \<le> a \<and> 0 \<le> b) \<or> (a \<le> 0 \<and> b \<le> 0) \<Longrightarrow> 0 \<le> a * b"
   798   by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)
   799 
   800 end
   801 
   802 class abs_if = minus + uminus + ord + zero + abs +
   803   assumes abs_if: "\<bar>a\<bar> = (if a < 0 then - a else a)"
   804 
   805 class sgn_if = minus + uminus + zero + one + ord + sgn +
   806   assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
   807 
   808 lemma (in sgn_if) sgn0[simp]: "sgn 0 = 0"
   809 by(simp add:sgn_if)
   810 
   811 class ordered_ring = ring + ordered_semiring
   812   + ordered_ab_group_add + abs_if
   813 begin
   814 
   815 subclass pordered_ring ..
   816 
   817 subclass pordered_ab_group_add_abs
   818 proof
   819   fix a b
   820   show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
   821   by (auto simp add: abs_if not_less neg_less_eq_nonneg less_eq_neg_nonpos)
   822    (auto simp del: minus_add_distrib simp add: minus_add_distrib [symmetric]
   823      neg_less_eq_nonneg less_eq_neg_nonpos, auto intro: add_nonneg_nonneg,
   824       auto intro!: less_imp_le add_neg_neg)
   825 qed (auto simp add: abs_if less_eq_neg_nonpos neg_equal_zero)
   826 
   827 end
   828 
   829 (* The "strict" suffix can be seen as describing the combination of ordered_ring and no_zero_divisors.
   830    Basically, ordered_ring + no_zero_divisors = ordered_ring_strict.
   831  *)
   832 class ordered_ring_strict = ring + ordered_semiring_strict
   833   + ordered_ab_group_add + abs_if
   834 begin
   835 
   836 subclass ordered_ring ..
   837 
   838 lemma mult_strict_left_mono_neg:
   839   "b < a \<Longrightarrow> c < 0 \<Longrightarrow> c * a < c * b"
   840   apply (drule mult_strict_left_mono [of _ _ "uminus c"])
   841   apply (simp_all add: minus_mult_left [symmetric]) 
   842   done
   843 
   844 lemma mult_strict_right_mono_neg:
   845   "b < a \<Longrightarrow> c < 0 \<Longrightarrow> a * c < b * c"
   846   apply (drule mult_strict_right_mono [of _ _ "uminus c"])
   847   apply (simp_all add: minus_mult_right [symmetric]) 
   848   done
   849 
   850 lemma mult_neg_neg:
   851   "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> 0 < a * b"
   852   by (drule mult_strict_right_mono_neg, auto)
   853 
   854 subclass ring_no_zero_divisors
   855 proof
   856   fix a b
   857   assume "a \<noteq> 0" then have A: "a < 0 \<or> 0 < a" by (simp add: neq_iff)
   858   assume "b \<noteq> 0" then have B: "b < 0 \<or> 0 < b" by (simp add: neq_iff)
   859   have "a * b < 0 \<or> 0 < a * b"
   860   proof (cases "a < 0")
   861     case True note A' = this
   862     show ?thesis proof (cases "b < 0")
   863       case True with A'
   864       show ?thesis by (auto dest: mult_neg_neg)
   865     next
   866       case False with B have "0 < b" by auto
   867       with A' show ?thesis by (auto dest: mult_strict_right_mono)
   868     qed
   869   next
   870     case False with A have A': "0 < a" by auto
   871     show ?thesis proof (cases "b < 0")
   872       case True with A'
   873       show ?thesis by (auto dest: mult_strict_right_mono_neg)
   874     next
   875       case False with B have "0 < b" by auto
   876       with A' show ?thesis by (auto dest: mult_pos_pos)
   877     qed
   878   qed
   879   then show "a * b \<noteq> 0" by (simp add: neq_iff)
   880 qed
   881 
   882 lemma zero_less_mult_iff:
   883   "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0"
   884   apply (auto simp add: mult_pos_pos mult_neg_neg)
   885   apply (simp_all add: not_less le_less)
   886   apply (erule disjE) apply assumption defer
   887   apply (erule disjE) defer apply (drule sym) apply simp
   888   apply (erule disjE) defer apply (drule sym) apply simp
   889   apply (erule disjE) apply assumption apply (drule sym) apply simp
   890   apply (drule sym) apply simp
   891   apply (blast dest: zero_less_mult_pos)
   892   apply (blast dest: zero_less_mult_pos2)
   893   done
   894 
   895 lemma zero_le_mult_iff:
   896   "0 \<le> a * b \<longleftrightarrow> 0 \<le> a \<and> 0 \<le> b \<or> a \<le> 0 \<and> b \<le> 0"
   897   by (auto simp add: eq_commute [of 0] le_less not_less zero_less_mult_iff)
   898 
   899 lemma mult_less_0_iff:
   900   "a * b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b"
   901   apply (insert zero_less_mult_iff [of "-a" b]) 
   902   apply (force simp add: minus_mult_left[symmetric]) 
   903   done
   904 
   905 lemma mult_le_0_iff:
   906   "a * b \<le> 0 \<longleftrightarrow> 0 \<le> a \<and> b \<le> 0 \<or> a \<le> 0 \<and> 0 \<le> b"
   907   apply (insert zero_le_mult_iff [of "-a" b]) 
   908   apply (force simp add: minus_mult_left[symmetric]) 
   909   done
   910 
   911 lemma zero_le_square [simp]: "0 \<le> a * a"
   912   by (simp add: zero_le_mult_iff linear)
   913 
   914 lemma not_square_less_zero [simp]: "\<not> (a * a < 0)"
   915   by (simp add: not_less)
   916 
   917 text{*Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"},
   918    also with the relations @{text "\<le>"} and equality.*}
   919 
   920 text{*These ``disjunction'' versions produce two cases when the comparison is
   921  an assumption, but effectively four when the comparison is a goal.*}
   922 
   923 lemma mult_less_cancel_right_disj:
   924   "a * c < b * c \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"
   925   apply (cases "c = 0")
   926   apply (auto simp add: neq_iff mult_strict_right_mono 
   927                       mult_strict_right_mono_neg)
   928   apply (auto simp add: not_less 
   929                       not_le [symmetric, of "a*c"]
   930                       not_le [symmetric, of a])
   931   apply (erule_tac [!] notE)
   932   apply (auto simp add: less_imp_le mult_right_mono 
   933                       mult_right_mono_neg)
   934   done
   935 
   936 lemma mult_less_cancel_left_disj:
   937   "c * a < c * b \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"
   938   apply (cases "c = 0")
   939   apply (auto simp add: neq_iff mult_strict_left_mono 
   940                       mult_strict_left_mono_neg)
   941   apply (auto simp add: not_less 
   942                       not_le [symmetric, of "c*a"]
   943                       not_le [symmetric, of a])
   944   apply (erule_tac [!] notE)
   945   apply (auto simp add: less_imp_le mult_left_mono 
   946                       mult_left_mono_neg)
   947   done
   948 
   949 text{*The ``conjunction of implication'' lemmas produce two cases when the
   950 comparison is a goal, but give four when the comparison is an assumption.*}
   951 
   952 lemma mult_less_cancel_right:
   953   "a * c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)"
   954   using mult_less_cancel_right_disj [of a c b] by auto
   955 
   956 lemma mult_less_cancel_left:
   957   "c * a < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)"
   958   using mult_less_cancel_left_disj [of c a b] by auto
   959 
   960 lemma mult_le_cancel_right:
   961    "a * c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
   962   by (simp add: not_less [symmetric] mult_less_cancel_right_disj)
   963 
   964 lemma mult_le_cancel_left:
   965   "c * a \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
   966   by (simp add: not_less [symmetric] mult_less_cancel_left_disj)
   967 
   968 end
   969 
   970 text{*This list of rewrites simplifies ring terms by multiplying
   971 everything out and bringing sums and products into a canonical form
   972 (by ordered rewriting). As a result it decides ring equalities but
   973 also helps with inequalities. *}
   974 lemmas ring_simps = group_simps ring_distribs
   975 
   976 
   977 class pordered_comm_ring = comm_ring + pordered_comm_semiring
   978 begin
   979 
   980 subclass pordered_ring ..
   981 subclass pordered_cancel_comm_semiring ..
   982 
   983 end
   984 
   985 class ordered_semidom = comm_semiring_1_cancel + ordered_comm_semiring_strict +
   986   (*previously ordered_semiring*)
   987   assumes zero_less_one [simp]: "0 < 1"
   988 begin
   989 
   990 lemma pos_add_strict:
   991   shows "0 < a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
   992   using add_strict_mono [of zero a b c] by simp
   993 
   994 lemma zero_le_one [simp]: "0 \<le> 1"
   995   by (rule zero_less_one [THEN less_imp_le]) 
   996 
   997 lemma not_one_le_zero [simp]: "\<not> 1 \<le> 0"
   998   by (simp add: not_le) 
   999 
  1000 lemma not_one_less_zero [simp]: "\<not> 1 < 0"
  1001   by (simp add: not_less) 
  1002 
  1003 lemma less_1_mult:
  1004   assumes "1 < m" and "1 < n"
  1005   shows "1 < m * n"
  1006   using assms mult_strict_mono [of 1 m 1 n]
  1007     by (simp add:  less_trans [OF zero_less_one]) 
  1008 
  1009 end
  1010 
  1011 class ordered_idom = comm_ring_1 +
  1012   ordered_comm_semiring_strict + ordered_ab_group_add +
  1013   abs_if + sgn_if
  1014   (*previously ordered_ring*)
  1015 begin
  1016 
  1017 subclass ordered_ring_strict ..
  1018 subclass pordered_comm_ring ..
  1019 subclass idom ..
  1020 
  1021 subclass ordered_semidom
  1022 proof
  1023   have "0 \<le> 1 * 1" by (rule zero_le_square)
  1024   thus "0 < 1" by (simp add: le_less)
  1025 qed 
  1026 
  1027 lemma linorder_neqE_ordered_idom:
  1028   assumes "x \<noteq> y" obtains "x < y" | "y < x"
  1029   using assms by (rule neqE)
  1030 
  1031 text {* These cancellation simprules also produce two cases when the comparison is a goal. *}
  1032 
  1033 lemma mult_le_cancel_right1:
  1034   "c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)"
  1035   by (insert mult_le_cancel_right [of 1 c b], simp)
  1036 
  1037 lemma mult_le_cancel_right2:
  1038   "a * c \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)"
  1039   by (insert mult_le_cancel_right [of a c 1], simp)
  1040 
  1041 lemma mult_le_cancel_left1:
  1042   "c \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)"
  1043   by (insert mult_le_cancel_left [of c 1 b], simp)
  1044 
  1045 lemma mult_le_cancel_left2:
  1046   "c * a \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)"
  1047   by (insert mult_le_cancel_left [of c a 1], simp)
  1048 
  1049 lemma mult_less_cancel_right1:
  1050   "c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)"
  1051   by (insert mult_less_cancel_right [of 1 c b], simp)
  1052 
  1053 lemma mult_less_cancel_right2:
  1054   "a * c < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"
  1055   by (insert mult_less_cancel_right [of a c 1], simp)
  1056 
  1057 lemma mult_less_cancel_left1:
  1058   "c < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)"
  1059   by (insert mult_less_cancel_left [of c 1 b], simp)
  1060 
  1061 lemma mult_less_cancel_left2:
  1062   "c * a < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"
  1063   by (insert mult_less_cancel_left [of c a 1], simp)
  1064 
  1065 lemma sgn_sgn [simp]:
  1066   "sgn (sgn a) = sgn a"
  1067   unfolding sgn_if by simp
  1068 
  1069 lemma sgn_0_0:
  1070   "sgn a = 0 \<longleftrightarrow> a = 0"
  1071   unfolding sgn_if by simp
  1072 
  1073 lemma sgn_1_pos:
  1074   "sgn a = 1 \<longleftrightarrow> a > 0"
  1075   unfolding sgn_if by (simp add: neg_equal_zero)
  1076 
  1077 lemma sgn_1_neg:
  1078   "sgn a = - 1 \<longleftrightarrow> a < 0"
  1079   unfolding sgn_if by (auto simp add: equal_neg_zero)
  1080 
  1081 lemma sgn_times:
  1082   "sgn (a * b) = sgn a * sgn b"
  1083   by (auto simp add: sgn_if zero_less_mult_iff)
  1084 
  1085 end
  1086 
  1087 class ordered_field = field + ordered_idom
  1088 
  1089 text {* Simprules for comparisons where common factors can be cancelled. *}
  1090 
  1091 lemmas mult_compare_simps =
  1092     mult_le_cancel_right mult_le_cancel_left
  1093     mult_le_cancel_right1 mult_le_cancel_right2
  1094     mult_le_cancel_left1 mult_le_cancel_left2
  1095     mult_less_cancel_right mult_less_cancel_left
  1096     mult_less_cancel_right1 mult_less_cancel_right2
  1097     mult_less_cancel_left1 mult_less_cancel_left2
  1098     mult_cancel_right mult_cancel_left
  1099     mult_cancel_right1 mult_cancel_right2
  1100     mult_cancel_left1 mult_cancel_left2
  1101 
  1102 -- {* FIXME continue localization here *}
  1103 
  1104 lemma inverse_nonzero_iff_nonzero [simp]:
  1105    "(inverse a = 0) = (a = (0::'a::{division_ring,division_by_zero}))"
  1106 by (force dest: inverse_zero_imp_zero) 
  1107 
  1108 lemma inverse_minus_eq [simp]:
  1109    "inverse(-a) = -inverse(a::'a::{division_ring,division_by_zero})"
  1110 proof cases
  1111   assume "a=0" thus ?thesis by (simp add: inverse_zero)
  1112 next
  1113   assume "a\<noteq>0" 
  1114   thus ?thesis by (simp add: nonzero_inverse_minus_eq)
  1115 qed
  1116 
  1117 lemma inverse_eq_imp_eq:
  1118   "inverse a = inverse b ==> a = (b::'a::{division_ring,division_by_zero})"
  1119 apply (cases "a=0 | b=0") 
  1120  apply (force dest!: inverse_zero_imp_zero
  1121               simp add: eq_commute [of "0::'a"])
  1122 apply (force dest!: nonzero_inverse_eq_imp_eq) 
  1123 done
  1124 
  1125 lemma inverse_eq_iff_eq [simp]:
  1126   "(inverse a = inverse b) = (a = (b::'a::{division_ring,division_by_zero}))"
  1127 by (force dest!: inverse_eq_imp_eq)
  1128 
  1129 lemma inverse_inverse_eq [simp]:
  1130      "inverse(inverse (a::'a::{division_ring,division_by_zero})) = a"
  1131   proof cases
  1132     assume "a=0" thus ?thesis by simp
  1133   next
  1134     assume "a\<noteq>0" 
  1135     thus ?thesis by (simp add: nonzero_inverse_inverse_eq)
  1136   qed
  1137 
  1138 text{*This version builds in division by zero while also re-orienting
  1139       the right-hand side.*}
  1140 lemma inverse_mult_distrib [simp]:
  1141      "inverse(a*b) = inverse(a) * inverse(b::'a::{field,division_by_zero})"
  1142   proof cases
  1143     assume "a \<noteq> 0 & b \<noteq> 0" 
  1144     thus ?thesis
  1145       by (simp add: nonzero_inverse_mult_distrib mult_commute)
  1146   next
  1147     assume "~ (a \<noteq> 0 & b \<noteq> 0)" 
  1148     thus ?thesis
  1149       by force
  1150   qed
  1151 
  1152 text{*There is no slick version using division by zero.*}
  1153 lemma inverse_add:
  1154   "[|a \<noteq> 0;  b \<noteq> 0|]
  1155    ==> inverse a + inverse b = (a+b) * inverse a * inverse (b::'a::field)"
  1156 by (simp add: division_ring_inverse_add mult_ac)
  1157 
  1158 lemma inverse_divide [simp]:
  1159   "inverse (a/b) = b / (a::'a::{field,division_by_zero})"
  1160 by (simp add: divide_inverse mult_commute)
  1161 
  1162 
  1163 subsection {* Calculations with fractions *}
  1164 
  1165 text{* There is a whole bunch of simp-rules just for class @{text
  1166 field} but none for class @{text field} and @{text nonzero_divides}
  1167 because the latter are covered by a simproc. *}
  1168 
  1169 lemma nonzero_mult_divide_mult_cancel_left[simp,noatp]:
  1170 assumes [simp]: "b\<noteq>0" and [simp]: "c\<noteq>0" shows "(c*a)/(c*b) = a/(b::'a::field)"
  1171 proof -
  1172   have "(c*a)/(c*b) = c * a * (inverse b * inverse c)"
  1173     by (simp add: divide_inverse nonzero_inverse_mult_distrib)
  1174   also have "... =  a * inverse b * (inverse c * c)"
  1175     by (simp only: mult_ac)
  1176   also have "... =  a * inverse b"
  1177     by simp
  1178     finally show ?thesis 
  1179     by (simp add: divide_inverse)
  1180 qed
  1181 
  1182 lemma mult_divide_mult_cancel_left:
  1183   "c\<noteq>0 ==> (c*a) / (c*b) = a / (b::'a::{field,division_by_zero})"
  1184 apply (cases "b = 0")
  1185 apply (simp_all add: nonzero_mult_divide_mult_cancel_left)
  1186 done
  1187 
  1188 lemma nonzero_mult_divide_mult_cancel_right [noatp]:
  1189   "[|b\<noteq>0; c\<noteq>0|] ==> (a*c) / (b*c) = a/(b::'a::field)"
  1190 by (simp add: mult_commute [of _ c] nonzero_mult_divide_mult_cancel_left) 
  1191 
  1192 lemma mult_divide_mult_cancel_right:
  1193   "c\<noteq>0 ==> (a*c) / (b*c) = a / (b::'a::{field,division_by_zero})"
  1194 apply (cases "b = 0")
  1195 apply (simp_all add: nonzero_mult_divide_mult_cancel_right)
  1196 done
  1197 
  1198 lemma divide_1 [simp]: "a/1 = (a::'a::field)"
  1199 by (simp add: divide_inverse)
  1200 
  1201 lemma times_divide_eq_right: "a * (b/c) = (a*b) / (c::'a::field)"
  1202 by (simp add: divide_inverse mult_assoc)
  1203 
  1204 lemma times_divide_eq_left: "(b/c) * a = (b*a) / (c::'a::field)"
  1205 by (simp add: divide_inverse mult_ac)
  1206 
  1207 lemmas times_divide_eq = times_divide_eq_right times_divide_eq_left
  1208 
  1209 lemma divide_divide_eq_right [simp,noatp]:
  1210   "a / (b/c) = (a*c) / (b::'a::{field,division_by_zero})"
  1211 by (simp add: divide_inverse mult_ac)
  1212 
  1213 lemma divide_divide_eq_left [simp,noatp]:
  1214   "(a / b) / (c::'a::{field,division_by_zero}) = a / (b*c)"
  1215 by (simp add: divide_inverse mult_assoc)
  1216 
  1217 lemma add_frac_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==>
  1218     x / y + w / z = (x * z + w * y) / (y * z)"
  1219 apply (subgoal_tac "x / y = (x * z) / (y * z)")
  1220 apply (erule ssubst)
  1221 apply (subgoal_tac "w / z = (w * y) / (y * z)")
  1222 apply (erule ssubst)
  1223 apply (rule add_divide_distrib [THEN sym])
  1224 apply (subst mult_commute)
  1225 apply (erule nonzero_mult_divide_mult_cancel_left [THEN sym])
  1226 apply assumption
  1227 apply (erule nonzero_mult_divide_mult_cancel_right [THEN sym])
  1228 apply assumption
  1229 done
  1230 
  1231 
  1232 subsubsection{*Special Cancellation Simprules for Division*}
  1233 
  1234 lemma mult_divide_mult_cancel_left_if[simp,noatp]:
  1235 fixes c :: "'a :: {field,division_by_zero}"
  1236 shows "(c*a) / (c*b) = (if c=0 then 0 else a/b)"
  1237 by (simp add: mult_divide_mult_cancel_left)
  1238 
  1239 lemma nonzero_mult_divide_cancel_right[simp,noatp]:
  1240   "b \<noteq> 0 \<Longrightarrow> a * b / b = (a::'a::field)"
  1241 using nonzero_mult_divide_mult_cancel_right[of 1 b a] by simp
  1242 
  1243 lemma nonzero_mult_divide_cancel_left[simp,noatp]:
  1244   "a \<noteq> 0 \<Longrightarrow> a * b / a = (b::'a::field)"
  1245 using nonzero_mult_divide_mult_cancel_left[of 1 a b] by simp
  1246 
  1247 
  1248 lemma nonzero_divide_mult_cancel_right[simp,noatp]:
  1249   "\<lbrakk> a\<noteq>0; b\<noteq>0 \<rbrakk> \<Longrightarrow> b / (a * b) = 1/(a::'a::field)"
  1250 using nonzero_mult_divide_mult_cancel_right[of a b 1] by simp
  1251 
  1252 lemma nonzero_divide_mult_cancel_left[simp,noatp]:
  1253   "\<lbrakk> a\<noteq>0; b\<noteq>0 \<rbrakk> \<Longrightarrow> a / (a * b) = 1/(b::'a::field)"
  1254 using nonzero_mult_divide_mult_cancel_left[of b a 1] by simp
  1255 
  1256 
  1257 lemma nonzero_mult_divide_mult_cancel_left2[simp,noatp]:
  1258   "[|b\<noteq>0; c\<noteq>0|] ==> (c*a) / (b*c) = a/(b::'a::field)"
  1259 using nonzero_mult_divide_mult_cancel_left[of b c a] by(simp add:mult_ac)
  1260 
  1261 lemma nonzero_mult_divide_mult_cancel_right2[simp,noatp]:
  1262   "[|b\<noteq>0; c\<noteq>0|] ==> (a*c) / (c*b) = a/(b::'a::field)"
  1263 using nonzero_mult_divide_mult_cancel_right[of b c a] by(simp add:mult_ac)
  1264 
  1265 
  1266 subsection {* Division and Unary Minus *}
  1267 
  1268 lemma nonzero_minus_divide_left: "b \<noteq> 0 ==> - (a/b) = (-a) / (b::'a::field)"
  1269 by (simp add: divide_inverse minus_mult_left)
  1270 
  1271 lemma nonzero_minus_divide_right: "b \<noteq> 0 ==> - (a/b) = a / -(b::'a::field)"
  1272 by (simp add: divide_inverse nonzero_inverse_minus_eq minus_mult_right)
  1273 
  1274 lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (-a)/(-b) = a / (b::'a::field)"
  1275 by (simp add: divide_inverse nonzero_inverse_minus_eq)
  1276 
  1277 lemma minus_divide_left: "- (a/b) = (-a) / (b::'a::field)"
  1278 by (simp add: divide_inverse minus_mult_left [symmetric])
  1279 
  1280 lemma minus_divide_right: "- (a/b) = a / -(b::'a::{field,division_by_zero})"
  1281 by (simp add: divide_inverse minus_mult_right [symmetric])
  1282 
  1283 
  1284 text{*The effect is to extract signs from divisions*}
  1285 lemmas divide_minus_left = minus_divide_left [symmetric]
  1286 lemmas divide_minus_right = minus_divide_right [symmetric]
  1287 declare divide_minus_left [simp]   divide_minus_right [simp]
  1288 
  1289 text{*Also, extract signs from products*}
  1290 lemmas mult_minus_left = minus_mult_left [symmetric]
  1291 lemmas mult_minus_right = minus_mult_right [symmetric]
  1292 declare mult_minus_left [simp]   mult_minus_right [simp]
  1293 
  1294 lemma minus_divide_divide [simp]:
  1295   "(-a)/(-b) = a / (b::'a::{field,division_by_zero})"
  1296 apply (cases "b=0", simp) 
  1297 apply (simp add: nonzero_minus_divide_divide) 
  1298 done
  1299 
  1300 lemma diff_divide_distrib: "(a-b)/(c::'a::field) = a/c - b/c"
  1301 by (simp add: diff_minus add_divide_distrib) 
  1302 
  1303 lemma add_divide_eq_iff:
  1304   "(z::'a::field) \<noteq> 0 \<Longrightarrow> x + y/z = (z*x + y)/z"
  1305 by(simp add:add_divide_distrib nonzero_mult_divide_cancel_left)
  1306 
  1307 lemma divide_add_eq_iff:
  1308   "(z::'a::field) \<noteq> 0 \<Longrightarrow> x/z + y = (x + z*y)/z"
  1309 by(simp add:add_divide_distrib nonzero_mult_divide_cancel_left)
  1310 
  1311 lemma diff_divide_eq_iff:
  1312   "(z::'a::field) \<noteq> 0 \<Longrightarrow> x - y/z = (z*x - y)/z"
  1313 by(simp add:diff_divide_distrib nonzero_mult_divide_cancel_left)
  1314 
  1315 lemma divide_diff_eq_iff:
  1316   "(z::'a::field) \<noteq> 0 \<Longrightarrow> x/z - y = (x - z*y)/z"
  1317 by(simp add:diff_divide_distrib nonzero_mult_divide_cancel_left)
  1318 
  1319 lemma nonzero_eq_divide_eq: "c\<noteq>0 ==> ((a::'a::field) = b/c) = (a*c = b)"
  1320 proof -
  1321   assume [simp]: "c\<noteq>0"
  1322   have "(a = b/c) = (a*c = (b/c)*c)" by simp
  1323   also have "... = (a*c = b)" by (simp add: divide_inverse mult_assoc)
  1324   finally show ?thesis .
  1325 qed
  1326 
  1327 lemma nonzero_divide_eq_eq: "c\<noteq>0 ==> (b/c = (a::'a::field)) = (b = a*c)"
  1328 proof -
  1329   assume [simp]: "c\<noteq>0"
  1330   have "(b/c = a) = ((b/c)*c = a*c)"  by simp
  1331   also have "... = (b = a*c)"  by (simp add: divide_inverse mult_assoc) 
  1332   finally show ?thesis .
  1333 qed
  1334 
  1335 lemma eq_divide_eq:
  1336   "((a::'a::{field,division_by_zero}) = b/c) = (if c\<noteq>0 then a*c = b else a=0)"
  1337 by (simp add: nonzero_eq_divide_eq) 
  1338 
  1339 lemma divide_eq_eq:
  1340   "(b/c = (a::'a::{field,division_by_zero})) = (if c\<noteq>0 then b = a*c else a=0)"
  1341 by (force simp add: nonzero_divide_eq_eq) 
  1342 
  1343 lemma divide_eq_imp: "(c::'a::{division_by_zero,field}) ~= 0 ==>
  1344     b = a * c ==> b / c = a"
  1345   by (subst divide_eq_eq, simp)
  1346 
  1347 lemma eq_divide_imp: "(c::'a::{division_by_zero,field}) ~= 0 ==>
  1348     a * c = b ==> a = b / c"
  1349   by (subst eq_divide_eq, simp)
  1350 
  1351 
  1352 lemmas field_eq_simps = ring_simps
  1353   (* pull / out*)
  1354   add_divide_eq_iff divide_add_eq_iff
  1355   diff_divide_eq_iff divide_diff_eq_iff
  1356   (* multiply eqn *)
  1357   nonzero_eq_divide_eq nonzero_divide_eq_eq
  1358 (* is added later:
  1359   times_divide_eq_left times_divide_eq_right
  1360 *)
  1361 
  1362 text{*An example:*}
  1363 lemma fixes a b c d e f :: "'a::field"
  1364 shows "\<lbrakk>a\<noteq>b; c\<noteq>d; e\<noteq>f \<rbrakk> \<Longrightarrow> ((a-b)*(c-d)*(e-f))/((c-d)*(e-f)*(a-b)) = 1"
  1365 apply(subgoal_tac "(c-d)*(e-f)*(a-b) \<noteq> 0")
  1366  apply(simp add:field_eq_simps)
  1367 apply(simp)
  1368 done
  1369 
  1370 
  1371 lemma diff_frac_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==>
  1372     x / y - w / z = (x * z - w * y) / (y * z)"
  1373 by (simp add:field_eq_simps times_divide_eq)
  1374 
  1375 lemma frac_eq_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==>
  1376     (x / y = w / z) = (x * z = w * y)"
  1377 by (simp add:field_eq_simps times_divide_eq)
  1378 
  1379 
  1380 subsection {* Ordered Fields *}
  1381 
  1382 lemma positive_imp_inverse_positive: 
  1383 assumes a_gt_0: "0 < a"  shows "0 < inverse (a::'a::ordered_field)"
  1384 proof -
  1385   have "0 < a * inverse a" 
  1386     by (simp add: a_gt_0 [THEN order_less_imp_not_eq2] zero_less_one)
  1387   thus "0 < inverse a" 
  1388     by (simp add: a_gt_0 [THEN order_less_not_sym] zero_less_mult_iff)
  1389 qed
  1390 
  1391 lemma negative_imp_inverse_negative:
  1392   "a < 0 ==> inverse a < (0::'a::ordered_field)"
  1393 by (insert positive_imp_inverse_positive [of "-a"], 
  1394     simp add: nonzero_inverse_minus_eq order_less_imp_not_eq)
  1395 
  1396 lemma inverse_le_imp_le:
  1397 assumes invle: "inverse a \<le> inverse b" and apos:  "0 < a"
  1398 shows "b \<le> (a::'a::ordered_field)"
  1399 proof (rule classical)
  1400   assume "~ b \<le> a"
  1401   hence "a < b"  by (simp add: linorder_not_le)
  1402   hence bpos: "0 < b"  by (blast intro: apos order_less_trans)
  1403   hence "a * inverse a \<le> a * inverse b"
  1404     by (simp add: apos invle order_less_imp_le mult_left_mono)
  1405   hence "(a * inverse a) * b \<le> (a * inverse b) * b"
  1406     by (simp add: bpos order_less_imp_le mult_right_mono)
  1407   thus "b \<le> a"  by (simp add: mult_assoc apos bpos order_less_imp_not_eq2)
  1408 qed
  1409 
  1410 lemma inverse_positive_imp_positive:
  1411 assumes inv_gt_0: "0 < inverse a" and nz: "a \<noteq> 0"
  1412 shows "0 < (a::'a::ordered_field)"
  1413 proof -
  1414   have "0 < inverse (inverse a)"
  1415     using inv_gt_0 by (rule positive_imp_inverse_positive)
  1416   thus "0 < a"
  1417     using nz by (simp add: nonzero_inverse_inverse_eq)
  1418 qed
  1419 
  1420 lemma inverse_positive_iff_positive [simp]:
  1421   "(0 < inverse a) = (0 < (a::'a::{ordered_field,division_by_zero}))"
  1422 apply (cases "a = 0", simp)
  1423 apply (blast intro: inverse_positive_imp_positive positive_imp_inverse_positive)
  1424 done
  1425 
  1426 lemma inverse_negative_imp_negative:
  1427 assumes inv_less_0: "inverse a < 0" and nz:  "a \<noteq> 0"
  1428 shows "a < (0::'a::ordered_field)"
  1429 proof -
  1430   have "inverse (inverse a) < 0"
  1431     using inv_less_0 by (rule negative_imp_inverse_negative)
  1432   thus "a < 0" using nz by (simp add: nonzero_inverse_inverse_eq)
  1433 qed
  1434 
  1435 lemma inverse_negative_iff_negative [simp]:
  1436   "(inverse a < 0) = (a < (0::'a::{ordered_field,division_by_zero}))"
  1437 apply (cases "a = 0", simp)
  1438 apply (blast intro: inverse_negative_imp_negative negative_imp_inverse_negative)
  1439 done
  1440 
  1441 lemma inverse_nonnegative_iff_nonnegative [simp]:
  1442   "(0 \<le> inverse a) = (0 \<le> (a::'a::{ordered_field,division_by_zero}))"
  1443 by (simp add: linorder_not_less [symmetric])
  1444 
  1445 lemma inverse_nonpositive_iff_nonpositive [simp]:
  1446   "(inverse a \<le> 0) = (a \<le> (0::'a::{ordered_field,division_by_zero}))"
  1447 by (simp add: linorder_not_less [symmetric])
  1448 
  1449 lemma ordered_field_no_lb: "\<forall> x. \<exists>y. y < (x::'a::ordered_field)"
  1450 proof
  1451   fix x::'a
  1452   have m1: "- (1::'a) < 0" by simp
  1453   from add_strict_right_mono[OF m1, where c=x] 
  1454   have "(- 1) + x < x" by simp
  1455   thus "\<exists>y. y < x" by blast
  1456 qed
  1457 
  1458 lemma ordered_field_no_ub: "\<forall> x. \<exists>y. y > (x::'a::ordered_field)"
  1459 proof
  1460   fix x::'a
  1461   have m1: " (1::'a) > 0" by simp
  1462   from add_strict_right_mono[OF m1, where c=x] 
  1463   have "1 + x > x" by simp
  1464   thus "\<exists>y. y > x" by blast
  1465 qed
  1466 
  1467 subsection{*Anti-Monotonicity of @{term inverse}*}
  1468 
  1469 lemma less_imp_inverse_less:
  1470 assumes less: "a < b" and apos:  "0 < a"
  1471 shows "inverse b < inverse (a::'a::ordered_field)"
  1472 proof (rule ccontr)
  1473   assume "~ inverse b < inverse a"
  1474   hence "inverse a \<le> inverse b"
  1475     by (simp add: linorder_not_less)
  1476   hence "~ (a < b)"
  1477     by (simp add: linorder_not_less inverse_le_imp_le [OF _ apos])
  1478   thus False
  1479     by (rule notE [OF _ less])
  1480 qed
  1481 
  1482 lemma inverse_less_imp_less:
  1483   "[|inverse a < inverse b; 0 < a|] ==> b < (a::'a::ordered_field)"
  1484 apply (simp add: order_less_le [of "inverse a"] order_less_le [of "b"])
  1485 apply (force dest!: inverse_le_imp_le nonzero_inverse_eq_imp_eq) 
  1486 done
  1487 
  1488 text{*Both premises are essential. Consider -1 and 1.*}
  1489 lemma inverse_less_iff_less [simp,noatp]:
  1490   "[|0 < a; 0 < b|] ==> (inverse a < inverse b) = (b < (a::'a::ordered_field))"
  1491 by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less) 
  1492 
  1493 lemma le_imp_inverse_le:
  1494   "[|a \<le> b; 0 < a|] ==> inverse b \<le> inverse (a::'a::ordered_field)"
  1495 by (force simp add: order_le_less less_imp_inverse_less)
  1496 
  1497 lemma inverse_le_iff_le [simp,noatp]:
  1498  "[|0 < a; 0 < b|] ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::ordered_field))"
  1499 by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le) 
  1500 
  1501 
  1502 text{*These results refer to both operands being negative.  The opposite-sign
  1503 case is trivial, since inverse preserves signs.*}
  1504 lemma inverse_le_imp_le_neg:
  1505   "[|inverse a \<le> inverse b; b < 0|] ==> b \<le> (a::'a::ordered_field)"
  1506 apply (rule classical) 
  1507 apply (subgoal_tac "a < 0") 
  1508  prefer 2 apply (force simp add: linorder_not_le intro: order_less_trans) 
  1509 apply (insert inverse_le_imp_le [of "-b" "-a"])
  1510 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
  1511 done
  1512 
  1513 lemma less_imp_inverse_less_neg:
  1514    "[|a < b; b < 0|] ==> inverse b < inverse (a::'a::ordered_field)"
  1515 apply (subgoal_tac "a < 0") 
  1516  prefer 2 apply (blast intro: order_less_trans) 
  1517 apply (insert less_imp_inverse_less [of "-b" "-a"])
  1518 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
  1519 done
  1520 
  1521 lemma inverse_less_imp_less_neg:
  1522    "[|inverse a < inverse b; b < 0|] ==> b < (a::'a::ordered_field)"
  1523 apply (rule classical) 
  1524 apply (subgoal_tac "a < 0") 
  1525  prefer 2
  1526  apply (force simp add: linorder_not_less intro: order_le_less_trans) 
  1527 apply (insert inverse_less_imp_less [of "-b" "-a"])
  1528 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
  1529 done
  1530 
  1531 lemma inverse_less_iff_less_neg [simp,noatp]:
  1532   "[|a < 0; b < 0|] ==> (inverse a < inverse b) = (b < (a::'a::ordered_field))"
  1533 apply (insert inverse_less_iff_less [of "-b" "-a"])
  1534 apply (simp del: inverse_less_iff_less 
  1535             add: order_less_imp_not_eq nonzero_inverse_minus_eq)
  1536 done
  1537 
  1538 lemma le_imp_inverse_le_neg:
  1539   "[|a \<le> b; b < 0|] ==> inverse b \<le> inverse (a::'a::ordered_field)"
  1540 by (force simp add: order_le_less less_imp_inverse_less_neg)
  1541 
  1542 lemma inverse_le_iff_le_neg [simp,noatp]:
  1543  "[|a < 0; b < 0|] ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::ordered_field))"
  1544 by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg) 
  1545 
  1546 
  1547 subsection{*Inverses and the Number One*}
  1548 
  1549 lemma one_less_inverse_iff:
  1550   "(1 < inverse x) = (0 < x & x < (1::'a::{ordered_field,division_by_zero}))"
  1551 proof cases
  1552   assume "0 < x"
  1553     with inverse_less_iff_less [OF zero_less_one, of x]
  1554     show ?thesis by simp
  1555 next
  1556   assume notless: "~ (0 < x)"
  1557   have "~ (1 < inverse x)"
  1558   proof
  1559     assume "1 < inverse x"
  1560     also with notless have "... \<le> 0" by (simp add: linorder_not_less)
  1561     also have "... < 1" by (rule zero_less_one) 
  1562     finally show False by auto
  1563   qed
  1564   with notless show ?thesis by simp
  1565 qed
  1566 
  1567 lemma inverse_eq_1_iff [simp]:
  1568   "(inverse x = 1) = (x = (1::'a::{field,division_by_zero}))"
  1569 by (insert inverse_eq_iff_eq [of x 1], simp) 
  1570 
  1571 lemma one_le_inverse_iff:
  1572   "(1 \<le> inverse x) = (0 < x & x \<le> (1::'a::{ordered_field,division_by_zero}))"
  1573 by (force simp add: order_le_less one_less_inverse_iff zero_less_one 
  1574                     eq_commute [of 1]) 
  1575 
  1576 lemma inverse_less_1_iff:
  1577   "(inverse x < 1) = (x \<le> 0 | 1 < (x::'a::{ordered_field,division_by_zero}))"
  1578 by (simp add: linorder_not_le [symmetric] one_le_inverse_iff) 
  1579 
  1580 lemma inverse_le_1_iff:
  1581   "(inverse x \<le> 1) = (x \<le> 0 | 1 \<le> (x::'a::{ordered_field,division_by_zero}))"
  1582 by (simp add: linorder_not_less [symmetric] one_less_inverse_iff) 
  1583 
  1584 
  1585 subsection{*Simplification of Inequalities Involving Literal Divisors*}
  1586 
  1587 lemma pos_le_divide_eq: "0 < (c::'a::ordered_field) ==> (a \<le> b/c) = (a*c \<le> b)"
  1588 proof -
  1589   assume less: "0<c"
  1590   hence "(a \<le> b/c) = (a*c \<le> (b/c)*c)"
  1591     by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
  1592   also have "... = (a*c \<le> b)"
  1593     by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc) 
  1594   finally show ?thesis .
  1595 qed
  1596 
  1597 lemma neg_le_divide_eq: "c < (0::'a::ordered_field) ==> (a \<le> b/c) = (b \<le> a*c)"
  1598 proof -
  1599   assume less: "c<0"
  1600   hence "(a \<le> b/c) = ((b/c)*c \<le> a*c)"
  1601     by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
  1602   also have "... = (b \<le> a*c)"
  1603     by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc) 
  1604   finally show ?thesis .
  1605 qed
  1606 
  1607 lemma le_divide_eq:
  1608   "(a \<le> b/c) = 
  1609    (if 0 < c then a*c \<le> b
  1610              else if c < 0 then b \<le> a*c
  1611              else  a \<le> (0::'a::{ordered_field,division_by_zero}))"
  1612 apply (cases "c=0", simp) 
  1613 apply (force simp add: pos_le_divide_eq neg_le_divide_eq linorder_neq_iff) 
  1614 done
  1615 
  1616 lemma pos_divide_le_eq: "0 < (c::'a::ordered_field) ==> (b/c \<le> a) = (b \<le> a*c)"
  1617 proof -
  1618   assume less: "0<c"
  1619   hence "(b/c \<le> a) = ((b/c)*c \<le> a*c)"
  1620     by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
  1621   also have "... = (b \<le> a*c)"
  1622     by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc) 
  1623   finally show ?thesis .
  1624 qed
  1625 
  1626 lemma neg_divide_le_eq: "c < (0::'a::ordered_field) ==> (b/c \<le> a) = (a*c \<le> b)"
  1627 proof -
  1628   assume less: "c<0"
  1629   hence "(b/c \<le> a) = (a*c \<le> (b/c)*c)"
  1630     by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
  1631   also have "... = (a*c \<le> b)"
  1632     by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc) 
  1633   finally show ?thesis .
  1634 qed
  1635 
  1636 lemma divide_le_eq:
  1637   "(b/c \<le> a) = 
  1638    (if 0 < c then b \<le> a*c
  1639              else if c < 0 then a*c \<le> b
  1640              else 0 \<le> (a::'a::{ordered_field,division_by_zero}))"
  1641 apply (cases "c=0", simp) 
  1642 apply (force simp add: pos_divide_le_eq neg_divide_le_eq linorder_neq_iff) 
  1643 done
  1644 
  1645 lemma pos_less_divide_eq:
  1646      "0 < (c::'a::ordered_field) ==> (a < b/c) = (a*c < b)"
  1647 proof -
  1648   assume less: "0<c"
  1649   hence "(a < b/c) = (a*c < (b/c)*c)"
  1650     by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])
  1651   also have "... = (a*c < b)"
  1652     by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc) 
  1653   finally show ?thesis .
  1654 qed
  1655 
  1656 lemma neg_less_divide_eq:
  1657  "c < (0::'a::ordered_field) ==> (a < b/c) = (b < a*c)"
  1658 proof -
  1659   assume less: "c<0"
  1660   hence "(a < b/c) = ((b/c)*c < a*c)"
  1661     by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])
  1662   also have "... = (b < a*c)"
  1663     by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc) 
  1664   finally show ?thesis .
  1665 qed
  1666 
  1667 lemma less_divide_eq:
  1668   "(a < b/c) = 
  1669    (if 0 < c then a*c < b
  1670              else if c < 0 then b < a*c
  1671              else  a < (0::'a::{ordered_field,division_by_zero}))"
  1672 apply (cases "c=0", simp) 
  1673 apply (force simp add: pos_less_divide_eq neg_less_divide_eq linorder_neq_iff) 
  1674 done
  1675 
  1676 lemma pos_divide_less_eq:
  1677      "0 < (c::'a::ordered_field) ==> (b/c < a) = (b < a*c)"
  1678 proof -
  1679   assume less: "0<c"
  1680   hence "(b/c < a) = ((b/c)*c < a*c)"
  1681     by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])
  1682   also have "... = (b < a*c)"
  1683     by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc) 
  1684   finally show ?thesis .
  1685 qed
  1686 
  1687 lemma neg_divide_less_eq:
  1688  "c < (0::'a::ordered_field) ==> (b/c < a) = (a*c < b)"
  1689 proof -
  1690   assume less: "c<0"
  1691   hence "(b/c < a) = (a*c < (b/c)*c)"
  1692     by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])
  1693   also have "... = (a*c < b)"
  1694     by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc) 
  1695   finally show ?thesis .
  1696 qed
  1697 
  1698 lemma divide_less_eq:
  1699   "(b/c < a) = 
  1700    (if 0 < c then b < a*c
  1701              else if c < 0 then a*c < b
  1702              else 0 < (a::'a::{ordered_field,division_by_zero}))"
  1703 apply (cases "c=0", simp) 
  1704 apply (force simp add: pos_divide_less_eq neg_divide_less_eq linorder_neq_iff) 
  1705 done
  1706 
  1707 
  1708 subsection{*Field simplification*}
  1709 
  1710 text{* Lemmas @{text field_simps} multiply with denominators in
  1711 in(equations) if they can be proved to be non-zero (for equations) or
  1712 positive/negative (for inequations). *}
  1713 
  1714 lemmas field_simps = field_eq_simps
  1715   (* multiply ineqn *)
  1716   pos_divide_less_eq neg_divide_less_eq
  1717   pos_less_divide_eq neg_less_divide_eq
  1718   pos_divide_le_eq neg_divide_le_eq
  1719   pos_le_divide_eq neg_le_divide_eq
  1720 
  1721 text{* Lemmas @{text sign_simps} is a first attempt to automate proofs
  1722 of positivity/negativity needed for @{text field_simps}. Have not added @{text
  1723 sign_simps} to @{text field_simps} because the former can lead to case
  1724 explosions. *}
  1725 
  1726 lemmas sign_simps = group_simps
  1727   zero_less_mult_iff  mult_less_0_iff
  1728 
  1729 (* Only works once linear arithmetic is installed:
  1730 text{*An example:*}
  1731 lemma fixes a b c d e f :: "'a::ordered_field"
  1732 shows "\<lbrakk>a>b; c<d; e<f; 0 < u \<rbrakk> \<Longrightarrow>
  1733  ((a-b)*(c-d)*(e-f))/((c-d)*(e-f)*(a-b)) <
  1734  ((e-f)*(a-b)*(c-d))/((e-f)*(a-b)*(c-d)) + u"
  1735 apply(subgoal_tac "(c-d)*(e-f)*(a-b) > 0")
  1736  prefer 2 apply(simp add:sign_simps)
  1737 apply(subgoal_tac "(c-d)*(e-f)*(a-b)*u > 0")
  1738  prefer 2 apply(simp add:sign_simps)
  1739 apply(simp add:field_simps)
  1740 done
  1741 *)
  1742 
  1743 
  1744 subsection{*Division and Signs*}
  1745 
  1746 lemma zero_less_divide_iff:
  1747      "((0::'a::{ordered_field,division_by_zero}) < a/b) = (0 < a & 0 < b | a < 0 & b < 0)"
  1748 by (simp add: divide_inverse zero_less_mult_iff)
  1749 
  1750 lemma divide_less_0_iff:
  1751      "(a/b < (0::'a::{ordered_field,division_by_zero})) = 
  1752       (0 < a & b < 0 | a < 0 & 0 < b)"
  1753 by (simp add: divide_inverse mult_less_0_iff)
  1754 
  1755 lemma zero_le_divide_iff:
  1756      "((0::'a::{ordered_field,division_by_zero}) \<le> a/b) =
  1757       (0 \<le> a & 0 \<le> b | a \<le> 0 & b \<le> 0)"
  1758 by (simp add: divide_inverse zero_le_mult_iff)
  1759 
  1760 lemma divide_le_0_iff:
  1761      "(a/b \<le> (0::'a::{ordered_field,division_by_zero})) =
  1762       (0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> b)"
  1763 by (simp add: divide_inverse mult_le_0_iff)
  1764 
  1765 lemma divide_eq_0_iff [simp,noatp]:
  1766      "(a/b = 0) = (a=0 | b=(0::'a::{field,division_by_zero}))"
  1767 by (simp add: divide_inverse)
  1768 
  1769 lemma divide_pos_pos:
  1770   "0 < (x::'a::ordered_field) ==> 0 < y ==> 0 < x / y"
  1771 by(simp add:field_simps)
  1772 
  1773 
  1774 lemma divide_nonneg_pos:
  1775   "0 <= (x::'a::ordered_field) ==> 0 < y ==> 0 <= x / y"
  1776 by(simp add:field_simps)
  1777 
  1778 lemma divide_neg_pos:
  1779   "(x::'a::ordered_field) < 0 ==> 0 < y ==> x / y < 0"
  1780 by(simp add:field_simps)
  1781 
  1782 lemma divide_nonpos_pos:
  1783   "(x::'a::ordered_field) <= 0 ==> 0 < y ==> x / y <= 0"
  1784 by(simp add:field_simps)
  1785 
  1786 lemma divide_pos_neg:
  1787   "0 < (x::'a::ordered_field) ==> y < 0 ==> x / y < 0"
  1788 by(simp add:field_simps)
  1789 
  1790 lemma divide_nonneg_neg:
  1791   "0 <= (x::'a::ordered_field) ==> y < 0 ==> x / y <= 0" 
  1792 by(simp add:field_simps)
  1793 
  1794 lemma divide_neg_neg:
  1795   "(x::'a::ordered_field) < 0 ==> y < 0 ==> 0 < x / y"
  1796 by(simp add:field_simps)
  1797 
  1798 lemma divide_nonpos_neg:
  1799   "(x::'a::ordered_field) <= 0 ==> y < 0 ==> 0 <= x / y"
  1800 by(simp add:field_simps)
  1801 
  1802 
  1803 subsection{*Cancellation Laws for Division*}
  1804 
  1805 lemma divide_cancel_right [simp,noatp]:
  1806      "(a/c = b/c) = (c = 0 | a = (b::'a::{field,division_by_zero}))"
  1807 apply (cases "c=0", simp)
  1808 apply (simp add: divide_inverse)
  1809 done
  1810 
  1811 lemma divide_cancel_left [simp,noatp]:
  1812      "(c/a = c/b) = (c = 0 | a = (b::'a::{field,division_by_zero}))" 
  1813 apply (cases "c=0", simp)
  1814 apply (simp add: divide_inverse)
  1815 done
  1816 
  1817 
  1818 subsection {* Division and the Number One *}
  1819 
  1820 text{*Simplify expressions equated with 1*}
  1821 lemma divide_eq_1_iff [simp,noatp]:
  1822      "(a/b = 1) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
  1823 apply (cases "b=0", simp)
  1824 apply (simp add: right_inverse_eq)
  1825 done
  1826 
  1827 lemma one_eq_divide_iff [simp,noatp]:
  1828      "(1 = a/b) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
  1829 by (simp add: eq_commute [of 1])
  1830 
  1831 lemma zero_eq_1_divide_iff [simp,noatp]:
  1832      "((0::'a::{ordered_field,division_by_zero}) = 1/a) = (a = 0)"
  1833 apply (cases "a=0", simp)
  1834 apply (auto simp add: nonzero_eq_divide_eq)
  1835 done
  1836 
  1837 lemma one_divide_eq_0_iff [simp,noatp]:
  1838      "(1/a = (0::'a::{ordered_field,division_by_zero})) = (a = 0)"
  1839 apply (cases "a=0", simp)
  1840 apply (insert zero_neq_one [THEN not_sym])
  1841 apply (auto simp add: nonzero_divide_eq_eq)
  1842 done
  1843 
  1844 text{*Simplify expressions such as @{text "0 < 1/x"} to @{text "0 < x"}*}
  1845 lemmas zero_less_divide_1_iff = zero_less_divide_iff [of 1, simplified]
  1846 lemmas divide_less_0_1_iff = divide_less_0_iff [of 1, simplified]
  1847 lemmas zero_le_divide_1_iff = zero_le_divide_iff [of 1, simplified]
  1848 lemmas divide_le_0_1_iff = divide_le_0_iff [of 1, simplified]
  1849 
  1850 declare zero_less_divide_1_iff [simp]
  1851 declare divide_less_0_1_iff [simp,noatp]
  1852 declare zero_le_divide_1_iff [simp]
  1853 declare divide_le_0_1_iff [simp,noatp]
  1854 
  1855 
  1856 subsection {* Ordering Rules for Division *}
  1857 
  1858 lemma divide_strict_right_mono:
  1859      "[|a < b; 0 < c|] ==> a / c < b / (c::'a::ordered_field)"
  1860 by (simp add: order_less_imp_not_eq2 divide_inverse mult_strict_right_mono 
  1861               positive_imp_inverse_positive)
  1862 
  1863 lemma divide_right_mono:
  1864      "[|a \<le> b; 0 \<le> c|] ==> a/c \<le> b/(c::'a::{ordered_field,division_by_zero})"
  1865 by (force simp add: divide_strict_right_mono order_le_less)
  1866 
  1867 lemma divide_right_mono_neg: "(a::'a::{division_by_zero,ordered_field}) <= b 
  1868     ==> c <= 0 ==> b / c <= a / c"
  1869 apply (drule divide_right_mono [of _ _ "- c"])
  1870 apply auto
  1871 done
  1872 
  1873 lemma divide_strict_right_mono_neg:
  1874      "[|b < a; c < 0|] ==> a / c < b / (c::'a::ordered_field)"
  1875 apply (drule divide_strict_right_mono [of _ _ "-c"], simp)
  1876 apply (simp add: order_less_imp_not_eq nonzero_minus_divide_right [symmetric])
  1877 done
  1878 
  1879 text{*The last premise ensures that @{term a} and @{term b} 
  1880       have the same sign*}
  1881 lemma divide_strict_left_mono:
  1882   "[|b < a; 0 < c; 0 < a*b|] ==> c / a < c / (b::'a::ordered_field)"
  1883 by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono)
  1884 
  1885 lemma divide_left_mono:
  1886   "[|b \<le> a; 0 \<le> c; 0 < a*b|] ==> c / a \<le> c / (b::'a::ordered_field)"
  1887 by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_right_mono)
  1888 
  1889 lemma divide_left_mono_neg: "(a::'a::{division_by_zero,ordered_field}) <= b 
  1890     ==> c <= 0 ==> 0 < a * b ==> c / a <= c / b"
  1891   apply (drule divide_left_mono [of _ _ "- c"])
  1892   apply (auto simp add: mult_commute)
  1893 done
  1894 
  1895 lemma divide_strict_left_mono_neg:
  1896   "[|a < b; c < 0; 0 < a*b|] ==> c / a < c / (b::'a::ordered_field)"
  1897 by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono_neg)
  1898 
  1899 
  1900 text{*Simplify quotients that are compared with the value 1.*}
  1901 
  1902 lemma le_divide_eq_1 [noatp]:
  1903   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1904   shows "(1 \<le> b / a) = ((0 < a & a \<le> b) | (a < 0 & b \<le> a))"
  1905 by (auto simp add: le_divide_eq)
  1906 
  1907 lemma divide_le_eq_1 [noatp]:
  1908   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1909   shows "(b / a \<le> 1) = ((0 < a & b \<le> a) | (a < 0 & a \<le> b) | a=0)"
  1910 by (auto simp add: divide_le_eq)
  1911 
  1912 lemma less_divide_eq_1 [noatp]:
  1913   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1914   shows "(1 < b / a) = ((0 < a & a < b) | (a < 0 & b < a))"
  1915 by (auto simp add: less_divide_eq)
  1916 
  1917 lemma divide_less_eq_1 [noatp]:
  1918   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1919   shows "(b / a < 1) = ((0 < a & b < a) | (a < 0 & a < b) | a=0)"
  1920 by (auto simp add: divide_less_eq)
  1921 
  1922 
  1923 subsection{*Conditional Simplification Rules: No Case Splits*}
  1924 
  1925 lemma le_divide_eq_1_pos [simp,noatp]:
  1926   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1927   shows "0 < a \<Longrightarrow> (1 \<le> b/a) = (a \<le> b)"
  1928 by (auto simp add: le_divide_eq)
  1929 
  1930 lemma le_divide_eq_1_neg [simp,noatp]:
  1931   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1932   shows "a < 0 \<Longrightarrow> (1 \<le> b/a) = (b \<le> a)"
  1933 by (auto simp add: le_divide_eq)
  1934 
  1935 lemma divide_le_eq_1_pos [simp,noatp]:
  1936   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1937   shows "0 < a \<Longrightarrow> (b/a \<le> 1) = (b \<le> a)"
  1938 by (auto simp add: divide_le_eq)
  1939 
  1940 lemma divide_le_eq_1_neg [simp,noatp]:
  1941   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1942   shows "a < 0 \<Longrightarrow> (b/a \<le> 1) = (a \<le> b)"
  1943 by (auto simp add: divide_le_eq)
  1944 
  1945 lemma less_divide_eq_1_pos [simp,noatp]:
  1946   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1947   shows "0 < a \<Longrightarrow> (1 < b/a) = (a < b)"
  1948 by (auto simp add: less_divide_eq)
  1949 
  1950 lemma less_divide_eq_1_neg [simp,noatp]:
  1951   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1952   shows "a < 0 \<Longrightarrow> (1 < b/a) = (b < a)"
  1953 by (auto simp add: less_divide_eq)
  1954 
  1955 lemma divide_less_eq_1_pos [simp,noatp]:
  1956   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1957   shows "0 < a \<Longrightarrow> (b/a < 1) = (b < a)"
  1958 by (auto simp add: divide_less_eq)
  1959 
  1960 lemma divide_less_eq_1_neg [simp,noatp]:
  1961   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1962   shows "a < 0 \<Longrightarrow> b/a < 1 <-> a < b"
  1963 by (auto simp add: divide_less_eq)
  1964 
  1965 lemma eq_divide_eq_1 [simp,noatp]:
  1966   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1967   shows "(1 = b/a) = ((a \<noteq> 0 & a = b))"
  1968 by (auto simp add: eq_divide_eq)
  1969 
  1970 lemma divide_eq_eq_1 [simp,noatp]:
  1971   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1972   shows "(b/a = 1) = ((a \<noteq> 0 & a = b))"
  1973 by (auto simp add: divide_eq_eq)
  1974 
  1975 
  1976 subsection {* Reasoning about inequalities with division *}
  1977 
  1978 lemma mult_right_le_one_le: "0 <= (x::'a::ordered_idom) ==> 0 <= y ==> y <= 1
  1979     ==> x * y <= x"
  1980   by (auto simp add: mult_compare_simps);
  1981 
  1982 lemma mult_left_le_one_le: "0 <= (x::'a::ordered_idom) ==> 0 <= y ==> y <= 1
  1983     ==> y * x <= x"
  1984   by (auto simp add: mult_compare_simps);
  1985 
  1986 lemma mult_imp_div_pos_le: "0 < (y::'a::ordered_field) ==> x <= z * y ==>
  1987     x / y <= z";
  1988   by (subst pos_divide_le_eq, assumption+);
  1989 
  1990 lemma mult_imp_le_div_pos: "0 < (y::'a::ordered_field) ==> z * y <= x ==>
  1991     z <= x / y"
  1992 by(simp add:field_simps)
  1993 
  1994 lemma mult_imp_div_pos_less: "0 < (y::'a::ordered_field) ==> x < z * y ==>
  1995     x / y < z"
  1996 by(simp add:field_simps)
  1997 
  1998 lemma mult_imp_less_div_pos: "0 < (y::'a::ordered_field) ==> z * y < x ==>
  1999     z < x / y"
  2000 by(simp add:field_simps)
  2001 
  2002 lemma frac_le: "(0::'a::ordered_field) <= x ==> 
  2003     x <= y ==> 0 < w ==> w <= z  ==> x / z <= y / w"
  2004   apply (rule mult_imp_div_pos_le)
  2005   apply simp
  2006   apply (subst times_divide_eq_left)
  2007   apply (rule mult_imp_le_div_pos, assumption)
  2008   apply (rule mult_mono)
  2009   apply simp_all
  2010 done
  2011 
  2012 lemma frac_less: "(0::'a::ordered_field) <= x ==> 
  2013     x < y ==> 0 < w ==> w <= z  ==> x / z < y / w"
  2014   apply (rule mult_imp_div_pos_less)
  2015   apply simp;
  2016   apply (subst times_divide_eq_left);
  2017   apply (rule mult_imp_less_div_pos, assumption)
  2018   apply (erule mult_less_le_imp_less)
  2019   apply simp_all
  2020 done
  2021 
  2022 lemma frac_less2: "(0::'a::ordered_field) < x ==> 
  2023     x <= y ==> 0 < w ==> w < z  ==> x / z < y / w"
  2024   apply (rule mult_imp_div_pos_less)
  2025   apply simp_all
  2026   apply (subst times_divide_eq_left);
  2027   apply (rule mult_imp_less_div_pos, assumption)
  2028   apply (erule mult_le_less_imp_less)
  2029   apply simp_all
  2030 done
  2031 
  2032 text{*It's not obvious whether these should be simprules or not. 
  2033   Their effect is to gather terms into one big fraction, like
  2034   a*b*c / x*y*z. The rationale for that is unclear, but many proofs 
  2035   seem to need them.*}
  2036 
  2037 declare times_divide_eq [simp]
  2038 
  2039 
  2040 subsection {* Ordered Fields are Dense *}
  2041 
  2042 context ordered_semidom
  2043 begin
  2044 
  2045 lemma less_add_one: "a < a + 1"
  2046 proof -
  2047   have "a + 0 < a + 1"
  2048     by (blast intro: zero_less_one add_strict_left_mono)
  2049   thus ?thesis by simp
  2050 qed
  2051 
  2052 lemma zero_less_two: "0 < 1 + 1"
  2053   by (blast intro: less_trans zero_less_one less_add_one)
  2054 
  2055 end
  2056 
  2057 lemma less_half_sum: "a < b ==> a < (a+b) / (1+1::'a::ordered_field)"
  2058 by (simp add: field_simps zero_less_two)
  2059 
  2060 lemma gt_half_sum: "a < b ==> (a+b)/(1+1::'a::ordered_field) < b"
  2061 by (simp add: field_simps zero_less_two)
  2062 
  2063 instance ordered_field < dense_linear_order
  2064 proof
  2065   fix x y :: 'a
  2066   have "x < x + 1" by simp
  2067   then show "\<exists>y. x < y" .. 
  2068   have "x - 1 < x" by simp
  2069   then show "\<exists>y. y < x" ..
  2070   show "x < y \<Longrightarrow> \<exists>z>x. z < y" by (blast intro!: less_half_sum gt_half_sum)
  2071 qed
  2072 
  2073 
  2074 subsection {* Absolute Value *}
  2075 
  2076 context ordered_idom
  2077 begin
  2078 
  2079 lemma mult_sgn_abs: "sgn x * abs x = x"
  2080   unfolding abs_if sgn_if by auto
  2081 
  2082 end
  2083 
  2084 lemma abs_one [simp]: "abs 1 = (1::'a::ordered_idom)"
  2085   by (simp add: abs_if zero_less_one [THEN order_less_not_sym])
  2086 
  2087 class pordered_ring_abs = pordered_ring + pordered_ab_group_add_abs +
  2088   assumes abs_eq_mult:
  2089     "(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>"
  2090 
  2091 
  2092 class lordered_ring = pordered_ring + lordered_ab_group_add_abs
  2093 begin
  2094 
  2095 subclass lordered_ab_group_add_meet ..
  2096 subclass lordered_ab_group_add_join ..
  2097 
  2098 end
  2099 
  2100 lemma abs_le_mult: "abs (a * b) \<le> (abs a) * (abs (b::'a::lordered_ring))" 
  2101 proof -
  2102   let ?x = "pprt a * pprt b - pprt a * nprt b - nprt a * pprt b + nprt a * nprt b"
  2103   let ?y = "pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b"
  2104   have a: "(abs a) * (abs b) = ?x"
  2105     by (simp only: abs_prts[of a] abs_prts[of b] ring_simps)
  2106   {
  2107     fix u v :: 'a
  2108     have bh: "\<lbrakk>u = a; v = b\<rbrakk> \<Longrightarrow> 
  2109               u * v = pprt a * pprt b + pprt a * nprt b + 
  2110                       nprt a * pprt b + nprt a * nprt b"
  2111       apply (subst prts[of u], subst prts[of v])
  2112       apply (simp add: ring_simps) 
  2113       done
  2114   }
  2115   note b = this[OF refl[of a] refl[of b]]
  2116   note addm = add_mono[of "0::'a" _ "0::'a", simplified]
  2117   note addm2 = add_mono[of _ "0::'a" _ "0::'a", simplified]
  2118   have xy: "- ?x <= ?y"
  2119     apply (simp)
  2120     apply (rule_tac y="0::'a" in order_trans)
  2121     apply (rule addm2)
  2122     apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)
  2123     apply (rule addm)
  2124     apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)
  2125     done
  2126   have yx: "?y <= ?x"
  2127     apply (simp add:diff_def)
  2128     apply (rule_tac y=0 in order_trans)
  2129     apply (rule addm2, (simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)+)
  2130     apply (rule addm, (simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)+)
  2131     done
  2132   have i1: "a*b <= abs a * abs b" by (simp only: a b yx)
  2133   have i2: "- (abs a * abs b) <= a*b" by (simp only: a b xy)
  2134   show ?thesis
  2135     apply (rule abs_leI)
  2136     apply (simp add: i1)
  2137     apply (simp add: i2[simplified minus_le_iff])
  2138     done
  2139 qed
  2140 
  2141 instance lordered_ring \<subseteq> pordered_ring_abs
  2142 proof
  2143   fix a b :: "'a\<Colon> lordered_ring"
  2144   assume "(0 \<le> a \<or> a \<le> 0) \<and> (0 \<le> b \<or> b \<le> 0)"
  2145   show "abs (a*b) = abs a * abs b"
  2146 proof -
  2147   have s: "(0 <= a*b) | (a*b <= 0)"
  2148     apply (auto)    
  2149     apply (rule_tac split_mult_pos_le)
  2150     apply (rule_tac contrapos_np[of "a*b <= 0"])
  2151     apply (simp)
  2152     apply (rule_tac split_mult_neg_le)
  2153     apply (insert prems)
  2154     apply (blast)
  2155     done
  2156   have mulprts: "a * b = (pprt a + nprt a) * (pprt b + nprt b)"
  2157     by (simp add: prts[symmetric])
  2158   show ?thesis
  2159   proof cases
  2160     assume "0 <= a * b"
  2161     then show ?thesis
  2162       apply (simp_all add: mulprts abs_prts)
  2163       apply (insert prems)
  2164       apply (auto simp add: 
  2165 	ring_simps 
  2166 	iffD1[OF zero_le_iff_zero_nprt] iffD1[OF le_zero_iff_zero_pprt]
  2167 	iffD1[OF le_zero_iff_pprt_id] iffD1[OF zero_le_iff_nprt_id])
  2168 	apply(drule (1) mult_nonneg_nonpos[of a b], simp)
  2169 	apply(drule (1) mult_nonneg_nonpos2[of b a], simp)
  2170       done
  2171   next
  2172     assume "~(0 <= a*b)"
  2173     with s have "a*b <= 0" by simp
  2174     then show ?thesis
  2175       apply (simp_all add: mulprts abs_prts)
  2176       apply (insert prems)
  2177       apply (auto simp add: ring_simps)
  2178       apply(drule (1) mult_nonneg_nonneg[of a b],simp)
  2179       apply(drule (1) mult_nonpos_nonpos[of a b],simp)
  2180       done
  2181   qed
  2182 qed
  2183 qed
  2184 
  2185 instance ordered_idom \<subseteq> pordered_ring_abs
  2186 by default (auto simp add: abs_if not_less
  2187   equal_neg_zero neg_equal_zero mult_less_0_iff)
  2188 
  2189 lemma abs_mult: "abs (a * b) = abs a * abs (b::'a::ordered_idom)" 
  2190   by (simp add: abs_eq_mult linorder_linear)
  2191 
  2192 lemma abs_mult_self: "abs a * abs a = a * (a::'a::ordered_idom)"
  2193   by (simp add: abs_if) 
  2194 
  2195 lemma nonzero_abs_inverse:
  2196      "a \<noteq> 0 ==> abs (inverse (a::'a::ordered_field)) = inverse (abs a)"
  2197 apply (auto simp add: linorder_neq_iff abs_if nonzero_inverse_minus_eq 
  2198                       negative_imp_inverse_negative)
  2199 apply (blast intro: positive_imp_inverse_positive elim: order_less_asym) 
  2200 done
  2201 
  2202 lemma abs_inverse [simp]:
  2203      "abs (inverse (a::'a::{ordered_field,division_by_zero})) = 
  2204       inverse (abs a)"
  2205 apply (cases "a=0", simp) 
  2206 apply (simp add: nonzero_abs_inverse) 
  2207 done
  2208 
  2209 lemma nonzero_abs_divide:
  2210      "b \<noteq> 0 ==> abs (a / (b::'a::ordered_field)) = abs a / abs b"
  2211 by (simp add: divide_inverse abs_mult nonzero_abs_inverse) 
  2212 
  2213 lemma abs_divide [simp]:
  2214      "abs (a / (b::'a::{ordered_field,division_by_zero})) = abs a / abs b"
  2215 apply (cases "b=0", simp) 
  2216 apply (simp add: nonzero_abs_divide) 
  2217 done
  2218 
  2219 lemma abs_mult_less:
  2220      "[| abs a < c; abs b < d |] ==> abs a * abs b < c*(d::'a::ordered_idom)"
  2221 proof -
  2222   assume ac: "abs a < c"
  2223   hence cpos: "0<c" by (blast intro: order_le_less_trans abs_ge_zero)
  2224   assume "abs b < d"
  2225   thus ?thesis by (simp add: ac cpos mult_strict_mono) 
  2226 qed
  2227 
  2228 lemmas eq_minus_self_iff = equal_neg_zero
  2229 
  2230 lemma less_minus_self_iff: "(a < -a) = (a < (0::'a::ordered_idom))"
  2231   unfolding order_less_le less_eq_neg_nonpos equal_neg_zero ..
  2232 
  2233 lemma abs_less_iff: "(abs a < b) = (a < b & -a < (b::'a::ordered_idom))" 
  2234 apply (simp add: order_less_le abs_le_iff)  
  2235 apply (auto simp add: abs_if neg_less_eq_nonneg less_eq_neg_nonpos)
  2236 done
  2237 
  2238 lemma abs_mult_pos: "(0::'a::ordered_idom) <= x ==> 
  2239     (abs y) * x = abs (y * x)"
  2240   apply (subst abs_mult)
  2241   apply simp
  2242 done
  2243 
  2244 lemma abs_div_pos: "(0::'a::{division_by_zero,ordered_field}) < y ==> 
  2245     abs x / y = abs (x / y)"
  2246   apply (subst abs_divide)
  2247   apply (simp add: order_less_imp_le)
  2248 done
  2249 
  2250 
  2251 subsection {* Bounds of products via negative and positive Part *}
  2252 
  2253 lemma mult_le_prts:
  2254   assumes
  2255   "a1 <= (a::'a::lordered_ring)"
  2256   "a <= a2"
  2257   "b1 <= b"
  2258   "b <= b2"
  2259   shows
  2260   "a * b <= pprt a2 * pprt b2 + pprt a1 * nprt b2 + nprt a2 * pprt b1 + nprt a1 * nprt b1"
  2261 proof - 
  2262   have "a * b = (pprt a + nprt a) * (pprt b + nprt b)" 
  2263     apply (subst prts[symmetric])+
  2264     apply simp
  2265     done
  2266   then have "a * b = pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b"
  2267     by (simp add: ring_simps)
  2268   moreover have "pprt a * pprt b <= pprt a2 * pprt b2"
  2269     by (simp_all add: prems mult_mono)
  2270   moreover have "pprt a * nprt b <= pprt a1 * nprt b2"
  2271   proof -
  2272     have "pprt a * nprt b <= pprt a * nprt b2"
  2273       by (simp add: mult_left_mono prems)
  2274     moreover have "pprt a * nprt b2 <= pprt a1 * nprt b2"
  2275       by (simp add: mult_right_mono_neg prems)
  2276     ultimately show ?thesis
  2277       by simp
  2278   qed
  2279   moreover have "nprt a * pprt b <= nprt a2 * pprt b1"
  2280   proof - 
  2281     have "nprt a * pprt b <= nprt a2 * pprt b"
  2282       by (simp add: mult_right_mono prems)
  2283     moreover have "nprt a2 * pprt b <= nprt a2 * pprt b1"
  2284       by (simp add: mult_left_mono_neg prems)
  2285     ultimately show ?thesis
  2286       by simp
  2287   qed
  2288   moreover have "nprt a * nprt b <= nprt a1 * nprt b1"
  2289   proof -
  2290     have "nprt a * nprt b <= nprt a * nprt b1"
  2291       by (simp add: mult_left_mono_neg prems)
  2292     moreover have "nprt a * nprt b1 <= nprt a1 * nprt b1"
  2293       by (simp add: mult_right_mono_neg prems)
  2294     ultimately show ?thesis
  2295       by simp
  2296   qed
  2297   ultimately show ?thesis
  2298     by - (rule add_mono | simp)+
  2299 qed
  2300 
  2301 lemma mult_ge_prts:
  2302   assumes
  2303   "a1 <= (a::'a::lordered_ring)"
  2304   "a <= a2"
  2305   "b1 <= b"
  2306   "b <= b2"
  2307   shows
  2308   "a * b >= nprt a1 * pprt b2 + nprt a2 * nprt b2 + pprt a1 * pprt b1 + pprt a2 * nprt b1"
  2309 proof - 
  2310   from prems have a1:"- a2 <= -a" by auto
  2311   from prems have a2: "-a <= -a1" by auto
  2312   from mult_le_prts[of "-a2" "-a" "-a1" "b1" b "b2", OF a1 a2 prems(3) prems(4), simplified nprt_neg pprt_neg] 
  2313   have le: "- (a * b) <= - nprt a1 * pprt b2 + - nprt a2 * nprt b2 + - pprt a1 * pprt b1 + - pprt a2 * nprt b1" by simp  
  2314   then have "-(- nprt a1 * pprt b2 + - nprt a2 * nprt b2 + - pprt a1 * pprt b1 + - pprt a2 * nprt b1) <= a * b"
  2315     by (simp only: minus_le_iff)
  2316   then show ?thesis by simp
  2317 qed
  2318 
  2319 end