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