src/HOL/Fields.thy
author haftmann
Fri Jun 19 07:53:35 2015 +0200 (2015-06-19)
changeset 60517 f16e4fb20652
parent 60353 838025c6e278
child 60570 7ed2cde6806d
permissions -rw-r--r--
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
     1 (*  Title:      HOL/Fields.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 section {* Fields *}
    11 
    12 theory Fields
    13 imports Rings
    14 begin
    15 
    16 subsection {* Division rings *}
    17 
    18 text {*
    19   A division ring is like a field, but without the commutativity requirement.
    20 *}
    21 
    22 class inverse = divide +
    23   fixes inverse :: "'a \<Rightarrow> 'a"
    24 begin
    25   
    26 abbreviation inverse_divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "'/" 70)
    27 where
    28   "inverse_divide \<equiv> divide"
    29 
    30 end
    31 
    32 text{* Lemmas @{text divide_simps} move division to the outside and eliminates them on (in)equalities. *}
    33 
    34 named_theorems divide_simps "rewrite rules to eliminate divisions"
    35 
    36 class division_ring = ring_1 + inverse +
    37   assumes left_inverse [simp]:  "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
    38   assumes right_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> a * inverse a = 1"
    39   assumes divide_inverse: "a / b = a * inverse b"
    40   assumes inverse_zero [simp]: "inverse 0 = 0"
    41 begin
    42 
    43 subclass ring_1_no_zero_divisors
    44 proof
    45   fix a b :: 'a
    46   assume a: "a \<noteq> 0" and b: "b \<noteq> 0"
    47   show "a * b \<noteq> 0"
    48   proof
    49     assume ab: "a * b = 0"
    50     hence "0 = inverse a * (a * b) * inverse b" by simp
    51     also have "\<dots> = (inverse a * a) * (b * inverse b)"
    52       by (simp only: mult.assoc)
    53     also have "\<dots> = 1" using a b by simp
    54     finally show False by simp
    55   qed
    56 qed
    57 
    58 lemma nonzero_imp_inverse_nonzero:
    59   "a \<noteq> 0 \<Longrightarrow> inverse a \<noteq> 0"
    60 proof
    61   assume ianz: "inverse a = 0"
    62   assume "a \<noteq> 0"
    63   hence "1 = a * inverse a" by simp
    64   also have "... = 0" by (simp add: ianz)
    65   finally have "1 = 0" .
    66   thus False by (simp add: eq_commute)
    67 qed
    68 
    69 lemma inverse_zero_imp_zero:
    70   "inverse a = 0 \<Longrightarrow> a = 0"
    71 apply (rule classical)
    72 apply (drule nonzero_imp_inverse_nonzero)
    73 apply auto
    74 done
    75 
    76 lemma inverse_unique:
    77   assumes ab: "a * b = 1"
    78   shows "inverse a = b"
    79 proof -
    80   have "a \<noteq> 0" using ab by (cases "a = 0") simp_all
    81   moreover have "inverse a * (a * b) = inverse a" by (simp add: ab)
    82   ultimately show ?thesis by (simp add: mult.assoc [symmetric])
    83 qed
    84 
    85 lemma nonzero_inverse_minus_eq:
    86   "a \<noteq> 0 \<Longrightarrow> inverse (- a) = - inverse a"
    87 by (rule inverse_unique) simp
    88 
    89 lemma nonzero_inverse_inverse_eq:
    90   "a \<noteq> 0 \<Longrightarrow> inverse (inverse a) = a"
    91 by (rule inverse_unique) simp
    92 
    93 lemma nonzero_inverse_eq_imp_eq:
    94   assumes "inverse a = inverse b" and "a \<noteq> 0" and "b \<noteq> 0"
    95   shows "a = b"
    96 proof -
    97   from `inverse a = inverse b`
    98   have "inverse (inverse a) = inverse (inverse b)" by (rule arg_cong)
    99   with `a \<noteq> 0` and `b \<noteq> 0` show "a = b"
   100     by (simp add: nonzero_inverse_inverse_eq)
   101 qed
   102 
   103 lemma inverse_1 [simp]: "inverse 1 = 1"
   104 by (rule inverse_unique) simp
   105 
   106 lemma nonzero_inverse_mult_distrib:
   107   assumes "a \<noteq> 0" and "b \<noteq> 0"
   108   shows "inverse (a * b) = inverse b * inverse a"
   109 proof -
   110   have "a * (b * inverse b) * inverse a = 1" using assms by simp
   111   hence "a * b * (inverse b * inverse a) = 1" by (simp only: mult.assoc)
   112   thus ?thesis by (rule inverse_unique)
   113 qed
   114 
   115 lemma division_ring_inverse_add:
   116   "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a + inverse b = inverse a * (a + b) * inverse b"
   117 by (simp add: algebra_simps)
   118 
   119 lemma division_ring_inverse_diff:
   120   "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a - inverse b = inverse a * (b - a) * inverse b"
   121 by (simp add: algebra_simps)
   122 
   123 lemma right_inverse_eq: "b \<noteq> 0 \<Longrightarrow> a / b = 1 \<longleftrightarrow> a = b"
   124 proof
   125   assume neq: "b \<noteq> 0"
   126   {
   127     hence "a = (a / b) * b" by (simp add: divide_inverse mult.assoc)
   128     also assume "a / b = 1"
   129     finally show "a = b" by simp
   130   next
   131     assume "a = b"
   132     with neq show "a / b = 1" by (simp add: divide_inverse)
   133   }
   134 qed
   135 
   136 lemma nonzero_inverse_eq_divide: "a \<noteq> 0 \<Longrightarrow> inverse a = 1 / a"
   137 by (simp add: divide_inverse)
   138 
   139 lemma divide_self [simp]: "a \<noteq> 0 \<Longrightarrow> a / a = 1"
   140 by (simp add: divide_inverse)
   141 
   142 lemma divide_zero_left [simp]: "0 / a = 0"
   143 by (simp add: divide_inverse)
   144 
   145 lemma inverse_eq_divide [field_simps, divide_simps]: "inverse a = 1 / a"
   146 by (simp add: divide_inverse)
   147 
   148 lemma add_divide_distrib: "(a+b) / c = a/c + b/c"
   149 by (simp add: divide_inverse algebra_simps)
   150 
   151 lemma divide_1 [simp]: "a / 1 = a"
   152   by (simp add: divide_inverse)
   153 
   154 lemma times_divide_eq_right [simp]: "a * (b / c) = (a * b) / c"
   155   by (simp add: divide_inverse mult.assoc)
   156 
   157 lemma minus_divide_left: "- (a / b) = (-a) / b"
   158   by (simp add: divide_inverse)
   159 
   160 lemma nonzero_minus_divide_right: "b \<noteq> 0 ==> - (a / b) = a / (- b)"
   161   by (simp add: divide_inverse nonzero_inverse_minus_eq)
   162 
   163 lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (-a) / (-b) = a / b"
   164   by (simp add: divide_inverse nonzero_inverse_minus_eq)
   165 
   166 lemma divide_minus_left [simp]: "(-a) / b = - (a / b)"
   167   by (simp add: divide_inverse)
   168 
   169 lemma diff_divide_distrib: "(a - b) / c = a / c - b / c"
   170   using add_divide_distrib [of a "- b" c] by simp
   171 
   172 lemma nonzero_eq_divide_eq [field_simps]: "c \<noteq> 0 \<Longrightarrow> a = b / c \<longleftrightarrow> a * c = b"
   173 proof -
   174   assume [simp]: "c \<noteq> 0"
   175   have "a = b / c \<longleftrightarrow> a * c = (b / c) * c" by simp
   176   also have "... \<longleftrightarrow> a * c = b" by (simp add: divide_inverse mult.assoc)
   177   finally show ?thesis .
   178 qed
   179 
   180 lemma nonzero_divide_eq_eq [field_simps]: "c \<noteq> 0 \<Longrightarrow> b / c = a \<longleftrightarrow> b = a * c"
   181 proof -
   182   assume [simp]: "c \<noteq> 0"
   183   have "b / c = a \<longleftrightarrow> (b / c) * c = a * c" by simp
   184   also have "... \<longleftrightarrow> b = a * c" by (simp add: divide_inverse mult.assoc)
   185   finally show ?thesis .
   186 qed
   187 
   188 lemma nonzero_neg_divide_eq_eq [field_simps]: "b \<noteq> 0 \<Longrightarrow> - (a / b) = c \<longleftrightarrow> - a = c * b"
   189   using nonzero_divide_eq_eq[of b "-a" c] by simp
   190 
   191 lemma nonzero_neg_divide_eq_eq2 [field_simps]: "b \<noteq> 0 \<Longrightarrow> c = - (a / b) \<longleftrightarrow> c * b = - a"
   192   using nonzero_neg_divide_eq_eq[of b a c] by auto
   193 
   194 lemma divide_eq_imp: "c \<noteq> 0 \<Longrightarrow> b = a * c \<Longrightarrow> b / c = a"
   195   by (simp add: divide_inverse mult.assoc)
   196 
   197 lemma eq_divide_imp: "c \<noteq> 0 \<Longrightarrow> a * c = b \<Longrightarrow> a = b / c"
   198   by (drule sym) (simp add: divide_inverse mult.assoc)
   199 
   200 lemma add_divide_eq_iff [field_simps]:
   201   "z \<noteq> 0 \<Longrightarrow> x + y / z = (x * z + y) / z"
   202   by (simp add: add_divide_distrib nonzero_eq_divide_eq)
   203 
   204 lemma divide_add_eq_iff [field_simps]:
   205   "z \<noteq> 0 \<Longrightarrow> x / z + y = (x + y * z) / z"
   206   by (simp add: add_divide_distrib nonzero_eq_divide_eq)
   207 
   208 lemma diff_divide_eq_iff [field_simps]:
   209   "z \<noteq> 0 \<Longrightarrow> x - y / z = (x * z - y) / z"
   210   by (simp add: diff_divide_distrib nonzero_eq_divide_eq eq_diff_eq)
   211 
   212 lemma minus_divide_add_eq_iff [field_simps]:
   213   "z \<noteq> 0 \<Longrightarrow> - (x / z) + y = (- x + y * z) / z"
   214   by (simp add: add_divide_distrib diff_divide_eq_iff)
   215 
   216 lemma divide_diff_eq_iff [field_simps]:
   217   "z \<noteq> 0 \<Longrightarrow> x / z - y = (x - y * z) / z"
   218   by (simp add: field_simps)
   219 
   220 lemma minus_divide_diff_eq_iff [field_simps]:
   221   "z \<noteq> 0 \<Longrightarrow> - (x / z) - y = (- x - y * z) / z"
   222   by (simp add: divide_diff_eq_iff[symmetric])
   223 
   224 lemma division_ring_divide_zero [simp]:
   225   "a / 0 = 0"
   226   by (simp add: divide_inverse)
   227 
   228 lemma divide_self_if [simp]:
   229   "a / a = (if a = 0 then 0 else 1)"
   230   by simp
   231 
   232 lemma inverse_nonzero_iff_nonzero [simp]:
   233   "inverse a = 0 \<longleftrightarrow> a = 0"
   234   by rule (fact inverse_zero_imp_zero, simp)
   235 
   236 lemma inverse_minus_eq [simp]:
   237   "inverse (- a) = - inverse a"
   238 proof cases
   239   assume "a=0" thus ?thesis by simp
   240 next
   241   assume "a\<noteq>0"
   242   thus ?thesis by (simp add: nonzero_inverse_minus_eq)
   243 qed
   244 
   245 lemma inverse_inverse_eq [simp]:
   246   "inverse (inverse a) = a"
   247 proof cases
   248   assume "a=0" thus ?thesis by simp
   249 next
   250   assume "a\<noteq>0"
   251   thus ?thesis by (simp add: nonzero_inverse_inverse_eq)
   252 qed
   253 
   254 lemma inverse_eq_imp_eq:
   255   "inverse a = inverse b \<Longrightarrow> a = b"
   256   by (drule arg_cong [where f="inverse"], simp)
   257 
   258 lemma inverse_eq_iff_eq [simp]:
   259   "inverse a = inverse b \<longleftrightarrow> a = b"
   260   by (force dest!: inverse_eq_imp_eq)
   261 
   262 lemma add_divide_eq_if_simps [divide_simps]:
   263     "a + b / z = (if z = 0 then a else (a * z + b) / z)"
   264     "a / z + b = (if z = 0 then b else (a + b * z) / z)"
   265     "- (a / z) + b = (if z = 0 then b else (-a + b * z) / z)"
   266     "a - b / z = (if z = 0 then a else (a * z - b) / z)"
   267     "a / z - b = (if z = 0 then -b else (a - b * z) / z)"
   268     "- (a / z) - b = (if z = 0 then -b else (- a - b * z) / z)"
   269   by (simp_all add: add_divide_eq_iff divide_add_eq_iff diff_divide_eq_iff divide_diff_eq_iff
   270       minus_divide_diff_eq_iff)
   271 
   272 lemma [divide_simps]:
   273   shows divide_eq_eq: "b / c = a \<longleftrightarrow> (if c \<noteq> 0 then b = a * c else a = 0)"
   274     and eq_divide_eq: "a = b / c \<longleftrightarrow> (if c \<noteq> 0 then a * c = b else a = 0)"
   275     and minus_divide_eq_eq: "- (b / c) = a \<longleftrightarrow> (if c \<noteq> 0 then - b = a * c else a = 0)"
   276     and eq_minus_divide_eq: "a = - (b / c) \<longleftrightarrow> (if c \<noteq> 0 then a * c = - b else a = 0)"
   277   by (auto simp add:  field_simps)
   278 
   279 end
   280 
   281 subsection {* Fields *}
   282 
   283 class field = comm_ring_1 + inverse +
   284   assumes field_inverse: "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
   285   assumes field_divide_inverse: "a / b = a * inverse b"
   286   assumes field_inverse_zero: "inverse 0 = 0"
   287 begin
   288 
   289 subclass division_ring
   290 proof
   291   fix a :: 'a
   292   assume "a \<noteq> 0"
   293   thus "inverse a * a = 1" by (rule field_inverse)
   294   thus "a * inverse a = 1" by (simp only: mult.commute)
   295 next
   296   fix a b :: 'a
   297   show "a / b = a * inverse b" by (rule field_divide_inverse)
   298 next
   299   show "inverse 0 = 0"
   300     by (fact field_inverse_zero) 
   301 qed
   302 
   303 subclass idom_divide
   304 proof
   305   fix b a
   306   assume "b \<noteq> 0"
   307   then show "a * b / b = a"
   308     by (simp add: divide_inverse ac_simps)
   309 next
   310   fix a
   311   show "a / 0 = 0"
   312     by (simp add: divide_inverse)
   313 qed
   314 
   315 text{*There is no slick version using division by zero.*}
   316 lemma inverse_add:
   317   "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a + inverse b = (a + b) * inverse a * inverse b"
   318   by (simp add: division_ring_inverse_add ac_simps)
   319 
   320 lemma nonzero_mult_divide_mult_cancel_left [simp]:
   321   assumes [simp]: "c \<noteq> 0"
   322   shows "(c * a) / (c * b) = a / b"
   323 proof (cases "b = 0")
   324   case True then show ?thesis by simp
   325 next
   326   case False
   327   then have "(c*a)/(c*b) = c * a * (inverse b * inverse c)"
   328     by (simp add: divide_inverse nonzero_inverse_mult_distrib)
   329   also have "... =  a * inverse b * (inverse c * c)"
   330     by (simp only: ac_simps)
   331   also have "... =  a * inverse b" by simp
   332     finally show ?thesis by (simp add: divide_inverse)
   333 qed
   334 
   335 lemma nonzero_mult_divide_mult_cancel_right [simp]:
   336   "c \<noteq> 0 \<Longrightarrow> (a * c) / (b * c) = a / b"
   337   using nonzero_mult_divide_mult_cancel_left [of c a b] by (simp add: ac_simps)
   338 
   339 lemma times_divide_eq_left [simp]: "(b / c) * a = (b * a) / c"
   340   by (simp add: divide_inverse ac_simps)
   341 
   342 lemma add_frac_eq:
   343   assumes "y \<noteq> 0" and "z \<noteq> 0"
   344   shows "x / y + w / z = (x * z + w * y) / (y * z)"
   345 proof -
   346   have "x / y + w / z = (x * z) / (y * z) + (y * w) / (y * z)"
   347     using assms by simp
   348   also have "\<dots> = (x * z + y * w) / (y * z)"
   349     by (simp only: add_divide_distrib)
   350   finally show ?thesis
   351     by (simp only: mult.commute)
   352 qed
   353 
   354 text{*Special Cancellation Simprules for Division*}
   355 
   356 lemma nonzero_divide_mult_cancel_right [simp]:
   357   "b \<noteq> 0 \<Longrightarrow> b / (a * b) = 1 / a"
   358   using nonzero_mult_divide_mult_cancel_right [of b 1 a] by simp
   359 
   360 lemma nonzero_divide_mult_cancel_left [simp]:
   361   "a \<noteq> 0 \<Longrightarrow> a / (a * b) = 1 / b"
   362   using nonzero_mult_divide_mult_cancel_left [of a 1 b] by simp
   363 
   364 lemma nonzero_mult_divide_mult_cancel_left2 [simp]:
   365   "c \<noteq> 0 \<Longrightarrow> (c * a) / (b * c) = a / b"
   366   using nonzero_mult_divide_mult_cancel_left [of c a b] by (simp add: ac_simps)
   367 
   368 lemma nonzero_mult_divide_mult_cancel_right2 [simp]:
   369   "c \<noteq> 0 \<Longrightarrow> (a * c) / (c * b) = a / b"
   370   using nonzero_mult_divide_mult_cancel_right [of b c a] by (simp add: ac_simps)
   371 
   372 lemma diff_frac_eq:
   373   "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> x / y - w / z = (x * z - w * y) / (y * z)"
   374   by (simp add: field_simps)
   375 
   376 lemma frac_eq_eq:
   377   "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> (x / y = w / z) = (x * z = w * y)"
   378   by (simp add: field_simps)
   379 
   380 lemma divide_minus1 [simp]: "x / - 1 = - x"
   381   using nonzero_minus_divide_right [of "1" x] by simp
   382 
   383 text{*This version builds in division by zero while also re-orienting
   384       the right-hand side.*}
   385 lemma inverse_mult_distrib [simp]:
   386   "inverse (a * b) = inverse a * inverse b"
   387 proof cases
   388   assume "a \<noteq> 0 & b \<noteq> 0"
   389   thus ?thesis by (simp add: nonzero_inverse_mult_distrib ac_simps)
   390 next
   391   assume "~ (a \<noteq> 0 & b \<noteq> 0)"
   392   thus ?thesis by force
   393 qed
   394 
   395 lemma inverse_divide [simp]:
   396   "inverse (a / b) = b / a"
   397   by (simp add: divide_inverse mult.commute)
   398 
   399 
   400 text {* Calculations with fractions *}
   401 
   402 text{* There is a whole bunch of simp-rules just for class @{text
   403 field} but none for class @{text field} and @{text nonzero_divides}
   404 because the latter are covered by a simproc. *}
   405 
   406 lemma mult_divide_mult_cancel_left:
   407   "c \<noteq> 0 \<Longrightarrow> (c * a) / (c * b) = a / b"
   408 apply (cases "b = 0")
   409 apply simp_all
   410 done
   411 
   412 lemma mult_divide_mult_cancel_right:
   413   "c \<noteq> 0 \<Longrightarrow> (a * c) / (b * c) = a / b"
   414 apply (cases "b = 0")
   415 apply simp_all
   416 done
   417 
   418 lemma divide_divide_eq_right [simp]:
   419   "a / (b / c) = (a * c) / b"
   420   by (simp add: divide_inverse ac_simps)
   421 
   422 lemma divide_divide_eq_left [simp]:
   423   "(a / b) / c = a / (b * c)"
   424   by (simp add: divide_inverse mult.assoc)
   425 
   426 lemma divide_divide_times_eq:
   427   "(x / y) / (z / w) = (x * w) / (y * z)"
   428   by simp
   429 
   430 text {*Special Cancellation Simprules for Division*}
   431 
   432 lemma mult_divide_mult_cancel_left_if [simp]:
   433   shows "(c * a) / (c * b) = (if c = 0 then 0 else a / b)"
   434   by simp
   435 
   436 
   437 text {* Division and Unary Minus *}
   438 
   439 lemma minus_divide_right:
   440   "- (a / b) = a / - b"
   441   by (simp add: divide_inverse)
   442 
   443 lemma divide_minus_right [simp]:
   444   "a / - b = - (a / b)"
   445   by (simp add: divide_inverse)
   446 
   447 lemma minus_divide_divide:
   448   "(- a) / (- b) = a / b"
   449 apply (cases "b=0", simp)
   450 apply (simp add: nonzero_minus_divide_divide)
   451 done
   452 
   453 lemma inverse_eq_1_iff [simp]:
   454   "inverse x = 1 \<longleftrightarrow> x = 1"
   455   by (insert inverse_eq_iff_eq [of x 1], simp)
   456 
   457 lemma divide_eq_0_iff [simp]:
   458   "a / b = 0 \<longleftrightarrow> a = 0 \<or> b = 0"
   459   by (simp add: divide_inverse)
   460 
   461 lemma divide_cancel_right [simp]:
   462   "a / c = b / c \<longleftrightarrow> c = 0 \<or> a = b"
   463   apply (cases "c=0", simp)
   464   apply (simp add: divide_inverse)
   465   done
   466 
   467 lemma divide_cancel_left [simp]:
   468   "c / a = c / b \<longleftrightarrow> c = 0 \<or> a = b"
   469   apply (cases "c=0", simp)
   470   apply (simp add: divide_inverse)
   471   done
   472 
   473 lemma divide_eq_1_iff [simp]:
   474   "a / b = 1 \<longleftrightarrow> b \<noteq> 0 \<and> a = b"
   475   apply (cases "b=0", simp)
   476   apply (simp add: right_inverse_eq)
   477   done
   478 
   479 lemma one_eq_divide_iff [simp]:
   480   "1 = a / b \<longleftrightarrow> b \<noteq> 0 \<and> a = b"
   481   by (simp add: eq_commute [of 1])
   482 
   483 lemma times_divide_times_eq:
   484   "(x / y) * (z / w) = (x * z) / (y * w)"
   485   by simp
   486 
   487 lemma add_frac_num:
   488   "y \<noteq> 0 \<Longrightarrow> x / y + z = (x + z * y) / y"
   489   by (simp add: add_divide_distrib)
   490 
   491 lemma add_num_frac:
   492   "y \<noteq> 0 \<Longrightarrow> z + x / y = (x + z * y) / y"
   493   by (simp add: add_divide_distrib add.commute)
   494 
   495 end
   496 
   497 
   498 subsection {* Ordered fields *}
   499 
   500 class linordered_field = field + linordered_idom
   501 begin
   502 
   503 lemma positive_imp_inverse_positive:
   504   assumes a_gt_0: "0 < a"
   505   shows "0 < inverse a"
   506 proof -
   507   have "0 < a * inverse a"
   508     by (simp add: a_gt_0 [THEN less_imp_not_eq2])
   509   thus "0 < inverse a"
   510     by (simp add: a_gt_0 [THEN less_not_sym] zero_less_mult_iff)
   511 qed
   512 
   513 lemma negative_imp_inverse_negative:
   514   "a < 0 \<Longrightarrow> inverse a < 0"
   515   by (insert positive_imp_inverse_positive [of "-a"],
   516     simp add: nonzero_inverse_minus_eq less_imp_not_eq)
   517 
   518 lemma inverse_le_imp_le:
   519   assumes invle: "inverse a \<le> inverse b" and apos: "0 < a"
   520   shows "b \<le> a"
   521 proof (rule classical)
   522   assume "~ b \<le> a"
   523   hence "a < b"  by (simp add: linorder_not_le)
   524   hence bpos: "0 < b"  by (blast intro: apos less_trans)
   525   hence "a * inverse a \<le> a * inverse b"
   526     by (simp add: apos invle less_imp_le mult_left_mono)
   527   hence "(a * inverse a) * b \<le> (a * inverse b) * b"
   528     by (simp add: bpos less_imp_le mult_right_mono)
   529   thus "b \<le> a"  by (simp add: mult.assoc apos bpos less_imp_not_eq2)
   530 qed
   531 
   532 lemma inverse_positive_imp_positive:
   533   assumes inv_gt_0: "0 < inverse a" and nz: "a \<noteq> 0"
   534   shows "0 < a"
   535 proof -
   536   have "0 < inverse (inverse a)"
   537     using inv_gt_0 by (rule positive_imp_inverse_positive)
   538   thus "0 < a"
   539     using nz by (simp add: nonzero_inverse_inverse_eq)
   540 qed
   541 
   542 lemma inverse_negative_imp_negative:
   543   assumes inv_less_0: "inverse a < 0" and nz: "a \<noteq> 0"
   544   shows "a < 0"
   545 proof -
   546   have "inverse (inverse a) < 0"
   547     using inv_less_0 by (rule negative_imp_inverse_negative)
   548   thus "a < 0" using nz by (simp add: nonzero_inverse_inverse_eq)
   549 qed
   550 
   551 lemma linordered_field_no_lb:
   552   "\<forall>x. \<exists>y. y < x"
   553 proof
   554   fix x::'a
   555   have m1: "- (1::'a) < 0" by simp
   556   from add_strict_right_mono[OF m1, where c=x]
   557   have "(- 1) + x < x" by simp
   558   thus "\<exists>y. y < x" by blast
   559 qed
   560 
   561 lemma linordered_field_no_ub:
   562   "\<forall> x. \<exists>y. y > x"
   563 proof
   564   fix x::'a
   565   have m1: " (1::'a) > 0" by simp
   566   from add_strict_right_mono[OF m1, where c=x]
   567   have "1 + x > x" by simp
   568   thus "\<exists>y. y > x" by blast
   569 qed
   570 
   571 lemma less_imp_inverse_less:
   572   assumes less: "a < b" and apos:  "0 < a"
   573   shows "inverse b < inverse a"
   574 proof (rule ccontr)
   575   assume "~ inverse b < inverse a"
   576   hence "inverse a \<le> inverse b" by simp
   577   hence "~ (a < b)"
   578     by (simp add: not_less inverse_le_imp_le [OF _ apos])
   579   thus False by (rule notE [OF _ less])
   580 qed
   581 
   582 lemma inverse_less_imp_less:
   583   "inverse a < inverse b \<Longrightarrow> 0 < a \<Longrightarrow> b < a"
   584 apply (simp add: less_le [of "inverse a"] less_le [of "b"])
   585 apply (force dest!: inverse_le_imp_le nonzero_inverse_eq_imp_eq)
   586 done
   587 
   588 text{*Both premises are essential. Consider -1 and 1.*}
   589 lemma inverse_less_iff_less [simp]:
   590   "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> inverse a < inverse b \<longleftrightarrow> b < a"
   591   by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less)
   592 
   593 lemma le_imp_inverse_le:
   594   "a \<le> b \<Longrightarrow> 0 < a \<Longrightarrow> inverse b \<le> inverse a"
   595   by (force simp add: le_less less_imp_inverse_less)
   596 
   597 lemma inverse_le_iff_le [simp]:
   598   "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> inverse a \<le> inverse b \<longleftrightarrow> b \<le> a"
   599   by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le)
   600 
   601 
   602 text{*These results refer to both operands being negative.  The opposite-sign
   603 case is trivial, since inverse preserves signs.*}
   604 lemma inverse_le_imp_le_neg:
   605   "inverse a \<le> inverse b \<Longrightarrow> b < 0 \<Longrightarrow> b \<le> a"
   606 apply (rule classical)
   607 apply (subgoal_tac "a < 0")
   608  prefer 2 apply force
   609 apply (insert inverse_le_imp_le [of "-b" "-a"])
   610 apply (simp add: nonzero_inverse_minus_eq)
   611 done
   612 
   613 lemma less_imp_inverse_less_neg:
   614    "a < b \<Longrightarrow> b < 0 \<Longrightarrow> inverse b < inverse a"
   615 apply (subgoal_tac "a < 0")
   616  prefer 2 apply (blast intro: less_trans)
   617 apply (insert less_imp_inverse_less [of "-b" "-a"])
   618 apply (simp add: nonzero_inverse_minus_eq)
   619 done
   620 
   621 lemma inverse_less_imp_less_neg:
   622    "inverse a < inverse b \<Longrightarrow> b < 0 \<Longrightarrow> b < a"
   623 apply (rule classical)
   624 apply (subgoal_tac "a < 0")
   625  prefer 2
   626  apply force
   627 apply (insert inverse_less_imp_less [of "-b" "-a"])
   628 apply (simp add: nonzero_inverse_minus_eq)
   629 done
   630 
   631 lemma inverse_less_iff_less_neg [simp]:
   632   "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> inverse a < inverse b \<longleftrightarrow> b < a"
   633 apply (insert inverse_less_iff_less [of "-b" "-a"])
   634 apply (simp del: inverse_less_iff_less
   635             add: nonzero_inverse_minus_eq)
   636 done
   637 
   638 lemma le_imp_inverse_le_neg:
   639   "a \<le> b \<Longrightarrow> b < 0 ==> inverse b \<le> inverse a"
   640   by (force simp add: le_less less_imp_inverse_less_neg)
   641 
   642 lemma inverse_le_iff_le_neg [simp]:
   643   "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> inverse a \<le> inverse b \<longleftrightarrow> b \<le> a"
   644   by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg)
   645 
   646 lemma one_less_inverse:
   647   "0 < a \<Longrightarrow> a < 1 \<Longrightarrow> 1 < inverse a"
   648   using less_imp_inverse_less [of a 1, unfolded inverse_1] .
   649 
   650 lemma one_le_inverse:
   651   "0 < a \<Longrightarrow> a \<le> 1 \<Longrightarrow> 1 \<le> inverse a"
   652   using le_imp_inverse_le [of a 1, unfolded inverse_1] .
   653 
   654 lemma pos_le_divide_eq [field_simps]:
   655   assumes "0 < c"
   656   shows "a \<le> b / c \<longleftrightarrow> a * c \<le> b"
   657 proof -
   658   from assms have "a \<le> b / c \<longleftrightarrow> a * c \<le> (b / c) * c"
   659     using mult_le_cancel_right [of a c "b * inverse c"] by (auto simp add: field_simps)
   660   also have "... \<longleftrightarrow> a * c \<le> b"
   661     by (simp add: less_imp_not_eq2 [OF assms] divide_inverse mult.assoc)
   662   finally show ?thesis .
   663 qed
   664 
   665 lemma pos_less_divide_eq [field_simps]:
   666   assumes "0 < c"
   667   shows "a < b / c \<longleftrightarrow> a * c < b"
   668 proof -
   669   from assms have "a < b / c \<longleftrightarrow> a * c < (b / c) * c"
   670     using mult_less_cancel_right [of a c "b / c"] by auto
   671   also have "... = (a*c < b)"
   672     by (simp add: less_imp_not_eq2 [OF assms] divide_inverse mult.assoc)
   673   finally show ?thesis .
   674 qed
   675 
   676 lemma neg_less_divide_eq [field_simps]:
   677   assumes "c < 0"
   678   shows "a < b / c \<longleftrightarrow> b < a * c"
   679 proof -
   680   from assms have "a < b / c \<longleftrightarrow> (b / c) * c < a * c"
   681     using mult_less_cancel_right [of "b / c" c a] by auto
   682   also have "... \<longleftrightarrow> b < a * c"
   683     by (simp add: less_imp_not_eq [OF assms] divide_inverse mult.assoc)
   684   finally show ?thesis .
   685 qed
   686 
   687 lemma neg_le_divide_eq [field_simps]:
   688   assumes "c < 0"
   689   shows "a \<le> b / c \<longleftrightarrow> b \<le> a * c"
   690 proof -
   691   from assms have "a \<le> b / c \<longleftrightarrow> (b / c) * c \<le> a * c"
   692     using mult_le_cancel_right [of "b * inverse c" c a] by (auto simp add: field_simps)
   693   also have "... \<longleftrightarrow> b \<le> a * c"
   694     by (simp add: less_imp_not_eq [OF assms] divide_inverse mult.assoc)
   695   finally show ?thesis .
   696 qed
   697 
   698 lemma pos_divide_le_eq [field_simps]:
   699   assumes "0 < c"
   700   shows "b / c \<le> a \<longleftrightarrow> b \<le> a * c"
   701 proof -
   702   from assms have "b / c \<le> a \<longleftrightarrow> (b / c) * c \<le> a * c"
   703     using mult_le_cancel_right [of "b / c" c a] by auto
   704   also have "... \<longleftrightarrow> b \<le> a * c"
   705     by (simp add: less_imp_not_eq2 [OF assms] divide_inverse mult.assoc)
   706   finally show ?thesis .
   707 qed
   708 
   709 lemma pos_divide_less_eq [field_simps]:
   710   assumes "0 < c"
   711   shows "b / c < a \<longleftrightarrow> b < a * c"
   712 proof -
   713   from assms have "b / c < a \<longleftrightarrow> (b / c) * c < a * c"
   714     using mult_less_cancel_right [of "b / c" c a] by auto
   715   also have "... \<longleftrightarrow> b < a * c"
   716     by (simp add: less_imp_not_eq2 [OF assms] divide_inverse mult.assoc)
   717   finally show ?thesis .
   718 qed
   719 
   720 lemma neg_divide_le_eq [field_simps]:
   721   assumes "c < 0"
   722   shows "b / c \<le> a \<longleftrightarrow> a * c \<le> b"
   723 proof -
   724   from assms have "b / c \<le> a \<longleftrightarrow> a * c \<le> (b / c) * c"
   725     using mult_le_cancel_right [of a c "b / c"] by auto
   726   also have "... \<longleftrightarrow> a * c \<le> b"
   727     by (simp add: less_imp_not_eq [OF assms] divide_inverse mult.assoc)
   728   finally show ?thesis .
   729 qed
   730 
   731 lemma neg_divide_less_eq [field_simps]:
   732   assumes "c < 0"
   733   shows "b / c < a \<longleftrightarrow> a * c < b"
   734 proof -
   735   from assms have "b / c < a \<longleftrightarrow> a * c < b / c * c"
   736     using mult_less_cancel_right [of a c "b / c"] by auto
   737   also have "... \<longleftrightarrow> a * c < b"
   738     by (simp add: less_imp_not_eq [OF assms] divide_inverse mult.assoc)
   739   finally show ?thesis .
   740 qed
   741 
   742 text{* The following @{text field_simps} rules are necessary, as minus is always moved atop of
   743 division but we want to get rid of division. *}
   744 
   745 lemma pos_le_minus_divide_eq [field_simps]: "0 < c \<Longrightarrow> a \<le> - (b / c) \<longleftrightarrow> a * c \<le> - b"
   746   unfolding minus_divide_left by (rule pos_le_divide_eq)
   747 
   748 lemma neg_le_minus_divide_eq [field_simps]: "c < 0 \<Longrightarrow> a \<le> - (b / c) \<longleftrightarrow> - b \<le> a * c"
   749   unfolding minus_divide_left by (rule neg_le_divide_eq)
   750 
   751 lemma pos_less_minus_divide_eq [field_simps]: "0 < c \<Longrightarrow> a < - (b / c) \<longleftrightarrow> a * c < - b"
   752   unfolding minus_divide_left by (rule pos_less_divide_eq)
   753 
   754 lemma neg_less_minus_divide_eq [field_simps]: "c < 0 \<Longrightarrow> a < - (b / c) \<longleftrightarrow> - b < a * c"
   755   unfolding minus_divide_left by (rule neg_less_divide_eq)
   756 
   757 lemma pos_minus_divide_less_eq [field_simps]: "0 < c \<Longrightarrow> - (b / c) < a \<longleftrightarrow> - b < a * c"
   758   unfolding minus_divide_left by (rule pos_divide_less_eq)
   759 
   760 lemma neg_minus_divide_less_eq [field_simps]: "c < 0 \<Longrightarrow> - (b / c) < a \<longleftrightarrow> a * c < - b"
   761   unfolding minus_divide_left by (rule neg_divide_less_eq)
   762 
   763 lemma pos_minus_divide_le_eq [field_simps]: "0 < c \<Longrightarrow> - (b / c) \<le> a \<longleftrightarrow> - b \<le> a * c"
   764   unfolding minus_divide_left by (rule pos_divide_le_eq)
   765 
   766 lemma neg_minus_divide_le_eq [field_simps]: "c < 0 \<Longrightarrow> - (b / c) \<le> a \<longleftrightarrow> a * c \<le> - b"
   767   unfolding minus_divide_left by (rule neg_divide_le_eq)
   768 
   769 lemma frac_less_eq:
   770   "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> x / y < w / z \<longleftrightarrow> (x * z - w * y) / (y * z) < 0"
   771   by (subst less_iff_diff_less_0) (simp add: diff_frac_eq )
   772 
   773 lemma frac_le_eq:
   774   "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> x / y \<le> w / z \<longleftrightarrow> (x * z - w * y) / (y * z) \<le> 0"
   775   by (subst le_iff_diff_le_0) (simp add: diff_frac_eq )
   776 
   777 text{* Lemmas @{text sign_simps} is a first attempt to automate proofs
   778 of positivity/negativity needed for @{text field_simps}. Have not added @{text
   779 sign_simps} to @{text field_simps} because the former can lead to case
   780 explosions. *}
   781 
   782 lemmas sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff
   783 
   784 lemmas (in -) sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff
   785 
   786 (* Only works once linear arithmetic is installed:
   787 text{*An example:*}
   788 lemma fixes a b c d e f :: "'a::linordered_field"
   789 shows "\<lbrakk>a>b; c<d; e<f; 0 < u \<rbrakk> \<Longrightarrow>
   790  ((a-b)*(c-d)*(e-f))/((c-d)*(e-f)*(a-b)) <
   791  ((e-f)*(a-b)*(c-d))/((e-f)*(a-b)*(c-d)) + u"
   792 apply(subgoal_tac "(c-d)*(e-f)*(a-b) > 0")
   793  prefer 2 apply(simp add:sign_simps)
   794 apply(subgoal_tac "(c-d)*(e-f)*(a-b)*u > 0")
   795  prefer 2 apply(simp add:sign_simps)
   796 apply(simp add:field_simps)
   797 done
   798 *)
   799 
   800 lemma divide_pos_pos[simp]:
   801   "0 < x ==> 0 < y ==> 0 < x / y"
   802 by(simp add:field_simps)
   803 
   804 lemma divide_nonneg_pos:
   805   "0 <= x ==> 0 < y ==> 0 <= x / y"
   806 by(simp add:field_simps)
   807 
   808 lemma divide_neg_pos:
   809   "x < 0 ==> 0 < y ==> x / y < 0"
   810 by(simp add:field_simps)
   811 
   812 lemma divide_nonpos_pos:
   813   "x <= 0 ==> 0 < y ==> x / y <= 0"
   814 by(simp add:field_simps)
   815 
   816 lemma divide_pos_neg:
   817   "0 < x ==> y < 0 ==> x / y < 0"
   818 by(simp add:field_simps)
   819 
   820 lemma divide_nonneg_neg:
   821   "0 <= x ==> y < 0 ==> x / y <= 0"
   822 by(simp add:field_simps)
   823 
   824 lemma divide_neg_neg:
   825   "x < 0 ==> y < 0 ==> 0 < x / y"
   826 by(simp add:field_simps)
   827 
   828 lemma divide_nonpos_neg:
   829   "x <= 0 ==> y < 0 ==> 0 <= x / y"
   830 by(simp add:field_simps)
   831 
   832 lemma divide_strict_right_mono:
   833      "[|a < b; 0 < c|] ==> a / c < b / c"
   834 by (simp add: less_imp_not_eq2 divide_inverse mult_strict_right_mono
   835               positive_imp_inverse_positive)
   836 
   837 
   838 lemma divide_strict_right_mono_neg:
   839      "[|b < a; c < 0|] ==> a / c < b / c"
   840 apply (drule divide_strict_right_mono [of _ _ "-c"], simp)
   841 apply (simp add: less_imp_not_eq nonzero_minus_divide_right [symmetric])
   842 done
   843 
   844 text{*The last premise ensures that @{term a} and @{term b}
   845       have the same sign*}
   846 lemma divide_strict_left_mono:
   847   "[|b < a; 0 < c; 0 < a*b|] ==> c / a < c / b"
   848   by (auto simp: field_simps zero_less_mult_iff mult_strict_right_mono)
   849 
   850 lemma divide_left_mono:
   851   "[|b \<le> a; 0 \<le> c; 0 < a*b|] ==> c / a \<le> c / b"
   852   by (auto simp: field_simps zero_less_mult_iff mult_right_mono)
   853 
   854 lemma divide_strict_left_mono_neg:
   855   "[|a < b; c < 0; 0 < a*b|] ==> c / a < c / b"
   856   by (auto simp: field_simps zero_less_mult_iff mult_strict_right_mono_neg)
   857 
   858 lemma mult_imp_div_pos_le: "0 < y ==> x <= z * y ==>
   859     x / y <= z"
   860 by (subst pos_divide_le_eq, assumption+)
   861 
   862 lemma mult_imp_le_div_pos: "0 < y ==> z * y <= x ==>
   863     z <= x / y"
   864 by(simp add:field_simps)
   865 
   866 lemma mult_imp_div_pos_less: "0 < y ==> x < z * y ==>
   867     x / y < z"
   868 by(simp add:field_simps)
   869 
   870 lemma mult_imp_less_div_pos: "0 < y ==> z * y < x ==>
   871     z < x / y"
   872 by(simp add:field_simps)
   873 
   874 lemma frac_le: "0 <= x ==>
   875     x <= y ==> 0 < w ==> w <= z  ==> x / z <= y / w"
   876   apply (rule mult_imp_div_pos_le)
   877   apply simp
   878   apply (subst times_divide_eq_left)
   879   apply (rule mult_imp_le_div_pos, assumption)
   880   apply (rule mult_mono)
   881   apply simp_all
   882 done
   883 
   884 lemma frac_less: "0 <= x ==>
   885     x < y ==> 0 < w ==> w <= z  ==> x / z < y / w"
   886   apply (rule mult_imp_div_pos_less)
   887   apply simp
   888   apply (subst times_divide_eq_left)
   889   apply (rule mult_imp_less_div_pos, assumption)
   890   apply (erule mult_less_le_imp_less)
   891   apply simp_all
   892 done
   893 
   894 lemma frac_less2: "0 < x ==>
   895     x <= y ==> 0 < w ==> w < z  ==> x / z < y / w"
   896   apply (rule mult_imp_div_pos_less)
   897   apply simp_all
   898   apply (rule mult_imp_less_div_pos, assumption)
   899   apply (erule mult_le_less_imp_less)
   900   apply simp_all
   901 done
   902 
   903 lemma less_half_sum: "a < b ==> a < (a+b) / (1+1)"
   904 by (simp add: field_simps zero_less_two)
   905 
   906 lemma gt_half_sum: "a < b ==> (a+b)/(1+1) < b"
   907 by (simp add: field_simps zero_less_two)
   908 
   909 subclass unbounded_dense_linorder
   910 proof
   911   fix x y :: 'a
   912   from less_add_one show "\<exists>y. x < y" ..
   913   from less_add_one have "x + (- 1) < (x + 1) + (- 1)" by (rule add_strict_right_mono)
   914   then have "x - 1 < x + 1 - 1" by simp
   915   then have "x - 1 < x" by (simp add: algebra_simps)
   916   then show "\<exists>y. y < x" ..
   917   show "x < y \<Longrightarrow> \<exists>z>x. z < y" by (blast intro!: less_half_sum gt_half_sum)
   918 qed
   919 
   920 lemma nonzero_abs_inverse:
   921      "a \<noteq> 0 ==> \<bar>inverse a\<bar> = inverse \<bar>a\<bar>"
   922 apply (auto simp add: neq_iff abs_if nonzero_inverse_minus_eq
   923                       negative_imp_inverse_negative)
   924 apply (blast intro: positive_imp_inverse_positive elim: less_asym)
   925 done
   926 
   927 lemma nonzero_abs_divide:
   928      "b \<noteq> 0 ==> \<bar>a / b\<bar> = \<bar>a\<bar> / \<bar>b\<bar>"
   929   by (simp add: divide_inverse abs_mult nonzero_abs_inverse)
   930 
   931 lemma field_le_epsilon:
   932   assumes e: "\<And>e. 0 < e \<Longrightarrow> x \<le> y + e"
   933   shows "x \<le> y"
   934 proof (rule dense_le)
   935   fix t assume "t < x"
   936   hence "0 < x - t" by (simp add: less_diff_eq)
   937   from e [OF this] have "x + 0 \<le> x + (y - t)" by (simp add: algebra_simps)
   938   then have "0 \<le> y - t" by (simp only: add_le_cancel_left)
   939   then show "t \<le> y" by (simp add: algebra_simps)
   940 qed
   941 
   942 lemma inverse_positive_iff_positive [simp]:
   943   "(0 < inverse a) = (0 < a)"
   944 apply (cases "a = 0", simp)
   945 apply (blast intro: inverse_positive_imp_positive positive_imp_inverse_positive)
   946 done
   947 
   948 lemma inverse_negative_iff_negative [simp]:
   949   "(inverse a < 0) = (a < 0)"
   950 apply (cases "a = 0", simp)
   951 apply (blast intro: inverse_negative_imp_negative negative_imp_inverse_negative)
   952 done
   953 
   954 lemma inverse_nonnegative_iff_nonnegative [simp]:
   955   "0 \<le> inverse a \<longleftrightarrow> 0 \<le> a"
   956   by (simp add: not_less [symmetric])
   957 
   958 lemma inverse_nonpositive_iff_nonpositive [simp]:
   959   "inverse a \<le> 0 \<longleftrightarrow> a \<le> 0"
   960   by (simp add: not_less [symmetric])
   961 
   962 lemma one_less_inverse_iff: "1 < inverse x \<longleftrightarrow> 0 < x \<and> x < 1"
   963   using less_trans[of 1 x 0 for x]
   964   by (cases x 0 rule: linorder_cases) (auto simp add: field_simps)
   965 
   966 lemma one_le_inverse_iff: "1 \<le> inverse x \<longleftrightarrow> 0 < x \<and> x \<le> 1"
   967 proof (cases "x = 1")
   968   case True then show ?thesis by simp
   969 next
   970   case False then have "inverse x \<noteq> 1" by simp
   971   then have "1 \<noteq> inverse x" by blast
   972   then have "1 \<le> inverse x \<longleftrightarrow> 1 < inverse x" by (simp add: le_less)
   973   with False show ?thesis by (auto simp add: one_less_inverse_iff)
   974 qed
   975 
   976 lemma inverse_less_1_iff: "inverse x < 1 \<longleftrightarrow> x \<le> 0 \<or> 1 < x"
   977   by (simp add: not_le [symmetric] one_le_inverse_iff)
   978 
   979 lemma inverse_le_1_iff: "inverse x \<le> 1 \<longleftrightarrow> x \<le> 0 \<or> 1 \<le> x"
   980   by (simp add: not_less [symmetric] one_less_inverse_iff)
   981 
   982 lemma [divide_simps]:
   983   shows le_divide_eq: "a \<le> b / c \<longleftrightarrow> (if 0 < c then a * c \<le> b else if c < 0 then b \<le> a * c else a \<le> 0)"
   984     and divide_le_eq: "b / c \<le> a \<longleftrightarrow> (if 0 < c then b \<le> a * c else if c < 0 then a * c \<le> b else 0 \<le> a)"
   985     and less_divide_eq: "a < b / c \<longleftrightarrow> (if 0 < c then a * c < b else if c < 0 then b < a * c else a < 0)"
   986     and divide_less_eq: "b / c < a \<longleftrightarrow> (if 0 < c then b < a * c else if c < 0 then a * c < b else 0 < a)"
   987     and le_minus_divide_eq: "a \<le> - (b / c) \<longleftrightarrow> (if 0 < c then a * c \<le> - b else if c < 0 then - b \<le> a * c else a \<le> 0)"
   988     and minus_divide_le_eq: "- (b / c) \<le> a \<longleftrightarrow> (if 0 < c then - b \<le> a * c else if c < 0 then a * c \<le> - b else 0 \<le> a)"
   989     and less_minus_divide_eq: "a < - (b / c) \<longleftrightarrow> (if 0 < c then a * c < - b else if c < 0 then - b < a * c else  a < 0)"
   990     and minus_divide_less_eq: "- (b / c) < a \<longleftrightarrow> (if 0 < c then - b < a * c else if c < 0 then a * c < - b else 0 < a)"
   991   by (auto simp: field_simps not_less dest: antisym)
   992 
   993 text {*Division and Signs*}
   994 
   995 lemma
   996   shows zero_less_divide_iff: "0 < a / b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0"
   997     and divide_less_0_iff: "a / b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b"
   998     and zero_le_divide_iff: "0 \<le> a / b \<longleftrightarrow> 0 \<le> a \<and> 0 \<le> b \<or> a \<le> 0 \<and> b \<le> 0"
   999     and divide_le_0_iff: "a / b \<le> 0 \<longleftrightarrow> 0 \<le> a \<and> b \<le> 0 \<or> a \<le> 0 \<and> 0 \<le> b"
  1000   by (auto simp add: divide_simps)
  1001 
  1002 text {* Division and the Number One *}
  1003 
  1004 text{*Simplify expressions equated with 1*}
  1005 
  1006 lemma zero_eq_1_divide_iff [simp]: "0 = 1 / a \<longleftrightarrow> a = 0"
  1007   by (cases "a = 0") (auto simp: field_simps)
  1008 
  1009 lemma one_divide_eq_0_iff [simp]: "1 / a = 0 \<longleftrightarrow> a = 0"
  1010   using zero_eq_1_divide_iff[of a] by simp
  1011 
  1012 text{*Simplify expressions such as @{text "0 < 1/x"} to @{text "0 < x"}*}
  1013 
  1014 lemma zero_le_divide_1_iff [simp]:
  1015   "0 \<le> 1 / a \<longleftrightarrow> 0 \<le> a"
  1016   by (simp add: zero_le_divide_iff)
  1017 
  1018 lemma zero_less_divide_1_iff [simp]:
  1019   "0 < 1 / a \<longleftrightarrow> 0 < a"
  1020   by (simp add: zero_less_divide_iff)
  1021 
  1022 lemma divide_le_0_1_iff [simp]:
  1023   "1 / a \<le> 0 \<longleftrightarrow> a \<le> 0"
  1024   by (simp add: divide_le_0_iff)
  1025 
  1026 lemma divide_less_0_1_iff [simp]:
  1027   "1 / a < 0 \<longleftrightarrow> a < 0"
  1028   by (simp add: divide_less_0_iff)
  1029 
  1030 lemma divide_right_mono:
  1031      "[|a \<le> b; 0 \<le> c|] ==> a/c \<le> b/c"
  1032 by (force simp add: divide_strict_right_mono le_less)
  1033 
  1034 lemma divide_right_mono_neg: "a <= b
  1035     ==> c <= 0 ==> b / c <= a / c"
  1036 apply (drule divide_right_mono [of _ _ "- c"])
  1037 apply auto
  1038 done
  1039 
  1040 lemma divide_left_mono_neg: "a <= b
  1041     ==> c <= 0 ==> 0 < a * b ==> c / a <= c / b"
  1042   apply (drule divide_left_mono [of _ _ "- c"])
  1043   apply (auto simp add: mult.commute)
  1044 done
  1045 
  1046 lemma inverse_le_iff: "inverse a \<le> inverse b \<longleftrightarrow> (0 < a * b \<longrightarrow> b \<le> a) \<and> (a * b \<le> 0 \<longrightarrow> a \<le> b)"
  1047   by (cases a 0 b 0 rule: linorder_cases[case_product linorder_cases])
  1048      (auto simp add: field_simps zero_less_mult_iff mult_le_0_iff)
  1049 
  1050 lemma inverse_less_iff: "inverse a < inverse b \<longleftrightarrow> (0 < a * b \<longrightarrow> b < a) \<and> (a * b \<le> 0 \<longrightarrow> a < b)"
  1051   by (subst less_le) (auto simp: inverse_le_iff)
  1052 
  1053 lemma divide_le_cancel: "a / c \<le> b / c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
  1054   by (simp add: divide_inverse mult_le_cancel_right)
  1055 
  1056 lemma divide_less_cancel: "a / c < b / c \<longleftrightarrow> (0 < c \<longrightarrow> a < b) \<and> (c < 0 \<longrightarrow> b < a) \<and> c \<noteq> 0"
  1057   by (auto simp add: divide_inverse mult_less_cancel_right)
  1058 
  1059 text{*Simplify quotients that are compared with the value 1.*}
  1060 
  1061 lemma le_divide_eq_1:
  1062   "(1 \<le> b / a) = ((0 < a & a \<le> b) | (a < 0 & b \<le> a))"
  1063 by (auto simp add: le_divide_eq)
  1064 
  1065 lemma divide_le_eq_1:
  1066   "(b / a \<le> 1) = ((0 < a & b \<le> a) | (a < 0 & a \<le> b) | a=0)"
  1067 by (auto simp add: divide_le_eq)
  1068 
  1069 lemma less_divide_eq_1:
  1070   "(1 < b / a) = ((0 < a & a < b) | (a < 0 & b < a))"
  1071 by (auto simp add: less_divide_eq)
  1072 
  1073 lemma divide_less_eq_1:
  1074   "(b / a < 1) = ((0 < a & b < a) | (a < 0 & a < b) | a=0)"
  1075 by (auto simp add: divide_less_eq)
  1076 
  1077 lemma divide_nonneg_nonneg [simp]:
  1078   "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> x / y"
  1079   by (auto simp add: divide_simps)
  1080 
  1081 lemma divide_nonpos_nonpos:
  1082   "x \<le> 0 \<Longrightarrow> y \<le> 0 \<Longrightarrow> 0 \<le> x / y"
  1083   by (auto simp add: divide_simps)
  1084 
  1085 lemma divide_nonneg_nonpos:
  1086   "0 \<le> x \<Longrightarrow> y \<le> 0 \<Longrightarrow> x / y \<le> 0"
  1087   by (auto simp add: divide_simps)
  1088 
  1089 lemma divide_nonpos_nonneg:
  1090   "x \<le> 0 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x / y \<le> 0"
  1091   by (auto simp add: divide_simps)
  1092 
  1093 text {*Conditional Simplification Rules: No Case Splits*}
  1094 
  1095 lemma le_divide_eq_1_pos [simp]:
  1096   "0 < a \<Longrightarrow> (1 \<le> b/a) = (a \<le> b)"
  1097 by (auto simp add: le_divide_eq)
  1098 
  1099 lemma le_divide_eq_1_neg [simp]:
  1100   "a < 0 \<Longrightarrow> (1 \<le> b/a) = (b \<le> a)"
  1101 by (auto simp add: le_divide_eq)
  1102 
  1103 lemma divide_le_eq_1_pos [simp]:
  1104   "0 < a \<Longrightarrow> (b/a \<le> 1) = (b \<le> a)"
  1105 by (auto simp add: divide_le_eq)
  1106 
  1107 lemma divide_le_eq_1_neg [simp]:
  1108   "a < 0 \<Longrightarrow> (b/a \<le> 1) = (a \<le> b)"
  1109 by (auto simp add: divide_le_eq)
  1110 
  1111 lemma less_divide_eq_1_pos [simp]:
  1112   "0 < a \<Longrightarrow> (1 < b/a) = (a < b)"
  1113 by (auto simp add: less_divide_eq)
  1114 
  1115 lemma less_divide_eq_1_neg [simp]:
  1116   "a < 0 \<Longrightarrow> (1 < b/a) = (b < a)"
  1117 by (auto simp add: less_divide_eq)
  1118 
  1119 lemma divide_less_eq_1_pos [simp]:
  1120   "0 < a \<Longrightarrow> (b/a < 1) = (b < a)"
  1121 by (auto simp add: divide_less_eq)
  1122 
  1123 lemma divide_less_eq_1_neg [simp]:
  1124   "a < 0 \<Longrightarrow> b/a < 1 <-> a < b"
  1125 by (auto simp add: divide_less_eq)
  1126 
  1127 lemma eq_divide_eq_1 [simp]:
  1128   "(1 = b/a) = ((a \<noteq> 0 & a = b))"
  1129 by (auto simp add: eq_divide_eq)
  1130 
  1131 lemma divide_eq_eq_1 [simp]:
  1132   "(b/a = 1) = ((a \<noteq> 0 & a = b))"
  1133 by (auto simp add: divide_eq_eq)
  1134 
  1135 lemma abs_inverse [simp]:
  1136      "\<bar>inverse a\<bar> =
  1137       inverse \<bar>a\<bar>"
  1138 apply (cases "a=0", simp)
  1139 apply (simp add: nonzero_abs_inverse)
  1140 done
  1141 
  1142 lemma abs_divide [simp]:
  1143      "\<bar>a / b\<bar> = \<bar>a\<bar> / \<bar>b\<bar>"
  1144 apply (cases "b=0", simp)
  1145 apply (simp add: nonzero_abs_divide)
  1146 done
  1147 
  1148 lemma abs_div_pos: "0 < y ==>
  1149     \<bar>x\<bar> / y = \<bar>x / y\<bar>"
  1150   apply (subst abs_divide)
  1151   apply (simp add: order_less_imp_le)
  1152 done
  1153 
  1154 lemma zero_le_divide_abs_iff [simp]: "(0 \<le> a / abs b) = (0 \<le> a | b = 0)"
  1155 by (auto simp: zero_le_divide_iff)
  1156 
  1157 lemma divide_le_0_abs_iff [simp]: "(a / abs b \<le> 0) = (a \<le> 0 | b = 0)"
  1158 by (auto simp: divide_le_0_iff)
  1159 
  1160 lemma field_le_mult_one_interval:
  1161   assumes *: "\<And>z. \<lbrakk> 0 < z ; z < 1 \<rbrakk> \<Longrightarrow> z * x \<le> y"
  1162   shows "x \<le> y"
  1163 proof (cases "0 < x")
  1164   assume "0 < x"
  1165   thus ?thesis
  1166     using dense_le_bounded[of 0 1 "y/x"] *
  1167     unfolding le_divide_eq if_P[OF `0 < x`] by simp
  1168 next
  1169   assume "\<not>0 < x" hence "x \<le> 0" by simp
  1170   obtain s::'a where s: "0 < s" "s < 1" using dense[of 0 "1\<Colon>'a"] by auto
  1171   hence "x \<le> s * x" using mult_le_cancel_right[of 1 x s] `x \<le> 0` by auto
  1172   also note *[OF s]
  1173   finally show ?thesis .
  1174 qed
  1175 
  1176 end
  1177 
  1178 hide_fact (open) field_inverse field_divide_inverse field_inverse_zero
  1179 
  1180 code_identifier
  1181   code_module Fields \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
  1182 
  1183 end