src/HOL/Ring_and_Field.thy
author paulson
Fri Jan 09 10:46:18 2004 +0100 (2004-01-09)
changeset 14348 744c868ee0b7
parent 14341 a09441bd4f1e
child 14353 79f9fbef9106
permissions -rw-r--r--
Defining the type class "ringpower" and deleting superseded theorems for
types nat, int, real, hypreal
     1 (*  Title:   HOL/Ring_and_Field.thy
     2     ID:      $Id$
     3     Author:  Gertrud Bauer and Markus Wenzel, TU Muenchen
     4              Lawrence C Paulson, University of Cambridge
     5     License: GPL (GNU GENERAL PUBLIC LICENSE)
     6 *)
     7 
     8 header {*
     9   \title{Ring and field structures}
    10   \author{Gertrud Bauer and Markus Wenzel}
    11 *}
    12 
    13 theory Ring_and_Field = Inductive:
    14 
    15 text{*Lemmas and extension to semirings by L. C. Paulson*}
    16 
    17 subsection {* Abstract algebraic structures *}
    18 
    19 axclass semiring \<subseteq> zero, one, plus, times
    20   add_assoc: "(a + b) + c = a + (b + c)"
    21   add_commute: "a + b = b + a"
    22   add_0 [simp]: "0 + a = a"
    23   add_left_imp_eq: "a + b = a + c ==> b=c"
    24     --{*This axiom is needed for semirings only: for rings, etc., it is
    25         redundant. Including it allows many more of the following results
    26         to be proved for semirings too. The drawback is that this redundant
    27         axiom must be proved for instances of rings.*}
    28 
    29   mult_assoc: "(a * b) * c = a * (b * c)"
    30   mult_commute: "a * b = b * a"
    31   mult_1 [simp]: "1 * a = a"
    32 
    33   left_distrib: "(a + b) * c = a * c + b * c"
    34   zero_neq_one [simp]: "0 \<noteq> 1"
    35 
    36 axclass ring \<subseteq> semiring, minus
    37   left_minus [simp]: "- a + a = 0"
    38   diff_minus: "a - b = a + (-b)"
    39 
    40 axclass ordered_semiring \<subseteq> semiring, linorder
    41   zero_less_one: "0 < 1" --{*This axiom too is needed for semirings only.*}
    42   add_left_mono: "a \<le> b ==> c + a \<le> c + b"
    43   mult_strict_left_mono: "a < b ==> 0 < c ==> c * a < c * b"
    44 
    45 axclass ordered_ring \<subseteq> ordered_semiring, ring
    46   abs_if: "\<bar>a\<bar> = (if a < 0 then -a else a)"
    47 
    48 axclass field \<subseteq> ring, inverse
    49   left_inverse [simp]: "a \<noteq> 0 ==> inverse a * a = 1"
    50   divide_inverse:      "b \<noteq> 0 ==> a / b = a * inverse b"
    51 
    52 axclass ordered_field \<subseteq> ordered_ring, field
    53 
    54 axclass division_by_zero \<subseteq> zero, inverse
    55   inverse_zero [simp]: "inverse 0 = 0"
    56   divide_zero [simp]: "a / 0 = 0"
    57 
    58 
    59 subsection {* Derived Rules for Addition *}
    60 
    61 lemma add_0_right [simp]: "a + 0 = (a::'a::semiring)"
    62 proof -
    63   have "a + 0 = 0 + a" by (simp only: add_commute)
    64   also have "... = a" by simp
    65   finally show ?thesis .
    66 qed
    67 
    68 lemma add_left_commute: "a + (b + c) = b + (a + (c::'a::semiring))"
    69   by (rule mk_left_commute [of "op +", OF add_assoc add_commute])
    70 
    71 theorems add_ac = add_assoc add_commute add_left_commute
    72 
    73 lemma right_minus [simp]: "a + -(a::'a::ring) = 0"
    74 proof -
    75   have "a + -a = -a + a" by (simp add: add_ac)
    76   also have "... = 0" by simp
    77   finally show ?thesis .
    78 qed
    79 
    80 lemma right_minus_eq: "(a - b = 0) = (a = (b::'a::ring))"
    81 proof
    82   have "a = a - b + b" by (simp add: diff_minus add_ac)
    83   also assume "a - b = 0"
    84   finally show "a = b" by simp
    85 next
    86   assume "a = b"
    87   thus "a - b = 0" by (simp add: diff_minus)
    88 qed
    89 
    90 lemma add_left_cancel [simp]:
    91      "(a + b = a + c) = (b = (c::'a::semiring))"
    92 by (blast dest: add_left_imp_eq) 
    93 
    94 lemma add_right_cancel [simp]:
    95      "(b + a = c + a) = (b = (c::'a::semiring))"
    96   by (simp add: add_commute)
    97 
    98 lemma minus_minus [simp]: "- (- (a::'a::ring)) = a"
    99   proof (rule add_left_cancel [of "-a", THEN iffD1])
   100     show "(-a + -(-a) = -a + a)"
   101     by simp
   102   qed
   103 
   104 lemma equals_zero_I: "a+b = 0 ==> -a = (b::'a::ring)"
   105 apply (rule right_minus_eq [THEN iffD1, symmetric])
   106 apply (simp add: diff_minus add_commute) 
   107 done
   108 
   109 lemma minus_zero [simp]: "- 0 = (0::'a::ring)"
   110 by (simp add: equals_zero_I)
   111 
   112 lemma diff_self [simp]: "a - (a::'a::ring) = 0"
   113   by (simp add: diff_minus)
   114 
   115 lemma diff_0 [simp]: "(0::'a::ring) - a = -a"
   116 by (simp add: diff_minus)
   117 
   118 lemma diff_0_right [simp]: "a - (0::'a::ring) = a" 
   119 by (simp add: diff_minus)
   120 
   121 lemma diff_minus_eq_add [simp]: "a - - b = a + (b::'a::ring)"
   122 by (simp add: diff_minus)
   123 
   124 lemma neg_equal_iff_equal [simp]: "(-a = -b) = (a = (b::'a::ring))" 
   125   proof 
   126     assume "- a = - b"
   127     hence "- (- a) = - (- b)"
   128       by simp
   129     thus "a=b" by simp
   130   next
   131     assume "a=b"
   132     thus "-a = -b" by simp
   133   qed
   134 
   135 lemma neg_equal_0_iff_equal [simp]: "(-a = 0) = (a = (0::'a::ring))"
   136 by (subst neg_equal_iff_equal [symmetric], simp)
   137 
   138 lemma neg_0_equal_iff_equal [simp]: "(0 = -a) = (0 = (a::'a::ring))"
   139 by (subst neg_equal_iff_equal [symmetric], simp)
   140 
   141 text{*The next two equations can make the simplifier loop!*}
   142 
   143 lemma equation_minus_iff: "(a = - b) = (b = - (a::'a::ring))"
   144   proof -
   145   have "(- (-a) = - b) = (- a = b)" by (rule neg_equal_iff_equal)
   146   thus ?thesis by (simp add: eq_commute)
   147   qed
   148 
   149 lemma minus_equation_iff: "(- a = b) = (- (b::'a::ring) = a)"
   150   proof -
   151   have "(- a = - (-b)) = (a = -b)" by (rule neg_equal_iff_equal)
   152   thus ?thesis by (simp add: eq_commute)
   153   qed
   154 
   155 
   156 subsection {* Derived rules for multiplication *}
   157 
   158 lemma mult_1_right [simp]: "a * (1::'a::semiring) = a"
   159 proof -
   160   have "a * 1 = 1 * a" by (simp add: mult_commute)
   161   also have "... = a" by simp
   162   finally show ?thesis .
   163 qed
   164 
   165 lemma mult_left_commute: "a * (b * c) = b * (a * (c::'a::semiring))"
   166   by (rule mk_left_commute [of "op *", OF mult_assoc mult_commute])
   167 
   168 theorems mult_ac = mult_assoc mult_commute mult_left_commute
   169 
   170 lemma mult_left_zero [simp]: "0 * a = (0::'a::semiring)"
   171 proof -
   172   have "0*a + 0*a = 0*a + 0"
   173     by (simp add: left_distrib [symmetric])
   174   thus ?thesis by (simp only: add_left_cancel)
   175 qed
   176 
   177 lemma mult_right_zero [simp]: "a * 0 = (0::'a::semiring)"
   178   by (simp add: mult_commute)
   179 
   180 
   181 subsection {* Distribution rules *}
   182 
   183 lemma right_distrib: "a * (b + c) = a * b + a * (c::'a::semiring)"
   184 proof -
   185   have "a * (b + c) = (b + c) * a" by (simp add: mult_ac)
   186   also have "... = b * a + c * a" by (simp only: left_distrib)
   187   also have "... = a * b + a * c" by (simp add: mult_ac)
   188   finally show ?thesis .
   189 qed
   190 
   191 theorems ring_distrib = right_distrib left_distrib
   192 
   193 text{*For the @{text combine_numerals} simproc*}
   194 lemma combine_common_factor: "a*e + (b*e + c) = (a+b)*e + (c::'a::semiring)"
   195 by (simp add: left_distrib add_ac)
   196 
   197 lemma minus_add_distrib [simp]: "- (a + b) = -a + -(b::'a::ring)"
   198 apply (rule equals_zero_I)
   199 apply (simp add: add_ac) 
   200 done
   201 
   202 lemma minus_mult_left: "- (a * b) = (-a) * (b::'a::ring)"
   203 apply (rule equals_zero_I)
   204 apply (simp add: left_distrib [symmetric]) 
   205 done
   206 
   207 lemma minus_mult_right: "- (a * b) = a * -(b::'a::ring)"
   208 apply (rule equals_zero_I)
   209 apply (simp add: right_distrib [symmetric]) 
   210 done
   211 
   212 lemma minus_mult_minus [simp]: "(- a) * (- b) = a * (b::'a::ring)"
   213   by (simp add: minus_mult_left [symmetric] minus_mult_right [symmetric])
   214 
   215 lemma right_diff_distrib: "a * (b - c) = a * b - a * (c::'a::ring)"
   216 by (simp add: right_distrib diff_minus 
   217               minus_mult_left [symmetric] minus_mult_right [symmetric]) 
   218 
   219 lemma left_diff_distrib: "(a - b) * c = a * c - b * (c::'a::ring)"
   220 by (simp add: mult_commute [of _ c] right_diff_distrib) 
   221 
   222 lemma minus_diff_eq [simp]: "- (a - b) = b - (a::'a::ring)"
   223 by (simp add: diff_minus add_commute) 
   224 
   225 
   226 subsection {* Ordering Rules for Addition *}
   227 
   228 lemma add_right_mono: "a \<le> (b::'a::ordered_semiring) ==> a + c \<le> b + c"
   229 by (simp add: add_commute [of _ c] add_left_mono)
   230 
   231 text {* non-strict, in both arguments *}
   232 lemma add_mono: "[|a \<le> b;  c \<le> d|] ==> a + c \<le> b + (d::'a::ordered_semiring)"
   233   apply (erule add_right_mono [THEN order_trans])
   234   apply (simp add: add_commute add_left_mono)
   235   done
   236 
   237 lemma add_strict_left_mono:
   238      "a < b ==> c + a < c + (b::'a::ordered_semiring)"
   239  by (simp add: order_less_le add_left_mono) 
   240 
   241 lemma add_strict_right_mono:
   242      "a < b ==> a + c < b + (c::'a::ordered_semiring)"
   243  by (simp add: add_commute [of _ c] add_strict_left_mono)
   244 
   245 text{*Strict monotonicity in both arguments*}
   246 lemma add_strict_mono: "[|a<b; c<d|] ==> a + c < b + (d::'a::ordered_semiring)"
   247 apply (erule add_strict_right_mono [THEN order_less_trans])
   248 apply (erule add_strict_left_mono)
   249 done
   250 
   251 lemma add_less_le_mono: "[| a<b; c\<le>d |] ==> a + c < b + (d::'a::ordered_semiring)"
   252 apply (erule add_strict_right_mono [THEN order_less_le_trans])
   253 apply (erule add_left_mono) 
   254 done
   255 
   256 lemma add_le_less_mono:
   257      "[| a\<le>b; c<d |] ==> a + c < b + (d::'a::ordered_semiring)"
   258 apply (erule add_right_mono [THEN order_le_less_trans])
   259 apply (erule add_strict_left_mono) 
   260 done
   261 
   262 lemma add_less_imp_less_left:
   263       assumes less: "c + a < c + b"  shows "a < (b::'a::ordered_semiring)"
   264   proof (rule ccontr)
   265     assume "~ a < b"
   266     hence "b \<le> a" by (simp add: linorder_not_less)
   267     hence "c+b \<le> c+a" by (rule add_left_mono)
   268     with this and less show False 
   269       by (simp add: linorder_not_less [symmetric])
   270   qed
   271 
   272 lemma add_less_imp_less_right:
   273       "a + c < b + c ==> a < (b::'a::ordered_semiring)"
   274 apply (rule add_less_imp_less_left [of c])
   275 apply (simp add: add_commute)  
   276 done
   277 
   278 lemma add_less_cancel_left [simp]:
   279     "(c+a < c+b) = (a < (b::'a::ordered_semiring))"
   280 by (blast intro: add_less_imp_less_left add_strict_left_mono) 
   281 
   282 lemma add_less_cancel_right [simp]:
   283     "(a+c < b+c) = (a < (b::'a::ordered_semiring))"
   284 by (blast intro: add_less_imp_less_right add_strict_right_mono)
   285 
   286 lemma add_le_cancel_left [simp]:
   287     "(c+a \<le> c+b) = (a \<le> (b::'a::ordered_semiring))"
   288 by (simp add: linorder_not_less [symmetric]) 
   289 
   290 lemma add_le_cancel_right [simp]:
   291     "(a+c \<le> b+c) = (a \<le> (b::'a::ordered_semiring))"
   292 by (simp add: linorder_not_less [symmetric]) 
   293 
   294 lemma add_le_imp_le_left:
   295       "c + a \<le> c + b ==> a \<le> (b::'a::ordered_semiring)"
   296 by simp
   297 
   298 lemma add_le_imp_le_right:
   299       "a + c \<le> b + c ==> a \<le> (b::'a::ordered_semiring)"
   300 by simp
   301 
   302 
   303 subsection {* Ordering Rules for Unary Minus *}
   304 
   305 lemma le_imp_neg_le:
   306       assumes "a \<le> (b::'a::ordered_ring)" shows "-b \<le> -a"
   307   proof -
   308   have "-a+a \<le> -a+b"
   309     by (rule add_left_mono) 
   310   hence "0 \<le> -a+b"
   311     by simp
   312   hence "0 + (-b) \<le> (-a + b) + (-b)"
   313     by (rule add_right_mono) 
   314   thus ?thesis
   315     by (simp add: add_assoc)
   316   qed
   317 
   318 lemma neg_le_iff_le [simp]: "(-b \<le> -a) = (a \<le> (b::'a::ordered_ring))"
   319   proof 
   320     assume "- b \<le> - a"
   321     hence "- (- a) \<le> - (- b)"
   322       by (rule le_imp_neg_le)
   323     thus "a\<le>b" by simp
   324   next
   325     assume "a\<le>b"
   326     thus "-b \<le> -a" by (rule le_imp_neg_le)
   327   qed
   328 
   329 lemma neg_le_0_iff_le [simp]: "(-a \<le> 0) = (0 \<le> (a::'a::ordered_ring))"
   330 by (subst neg_le_iff_le [symmetric], simp)
   331 
   332 lemma neg_0_le_iff_le [simp]: "(0 \<le> -a) = (a \<le> (0::'a::ordered_ring))"
   333 by (subst neg_le_iff_le [symmetric], simp)
   334 
   335 lemma neg_less_iff_less [simp]: "(-b < -a) = (a < (b::'a::ordered_ring))"
   336 by (force simp add: order_less_le) 
   337 
   338 lemma neg_less_0_iff_less [simp]: "(-a < 0) = (0 < (a::'a::ordered_ring))"
   339 by (subst neg_less_iff_less [symmetric], simp)
   340 
   341 lemma neg_0_less_iff_less [simp]: "(0 < -a) = (a < (0::'a::ordered_ring))"
   342 by (subst neg_less_iff_less [symmetric], simp)
   343 
   344 text{*The next several equations can make the simplifier loop!*}
   345 
   346 lemma less_minus_iff: "(a < - b) = (b < - (a::'a::ordered_ring))"
   347   proof -
   348   have "(- (-a) < - b) = (b < - a)" by (rule neg_less_iff_less)
   349   thus ?thesis by simp
   350   qed
   351 
   352 lemma minus_less_iff: "(- a < b) = (- b < (a::'a::ordered_ring))"
   353   proof -
   354   have "(- a < - (-b)) = (- b < a)" by (rule neg_less_iff_less)
   355   thus ?thesis by simp
   356   qed
   357 
   358 lemma le_minus_iff: "(a \<le> - b) = (b \<le> - (a::'a::ordered_ring))"
   359 apply (simp add: linorder_not_less [symmetric])
   360 apply (rule minus_less_iff) 
   361 done
   362 
   363 lemma minus_le_iff: "(- a \<le> b) = (- b \<le> (a::'a::ordered_ring))"
   364 apply (simp add: linorder_not_less [symmetric])
   365 apply (rule less_minus_iff) 
   366 done
   367 
   368 
   369 subsection{*Subtraction Laws*}
   370 
   371 lemma add_diff_eq: "a + (b - c) = (a + b) - (c::'a::ring)"
   372 by (simp add: diff_minus add_ac)
   373 
   374 lemma diff_add_eq: "(a - b) + c = (a + c) - (b::'a::ring)"
   375 by (simp add: diff_minus add_ac)
   376 
   377 lemma diff_eq_eq: "(a-b = c) = (a = c + (b::'a::ring))"
   378 by (auto simp add: diff_minus add_assoc)
   379 
   380 lemma eq_diff_eq: "(a = c-b) = (a + (b::'a::ring) = c)"
   381 by (auto simp add: diff_minus add_assoc)
   382 
   383 lemma diff_diff_eq: "(a - b) - c = a - (b + (c::'a::ring))"
   384 by (simp add: diff_minus add_ac)
   385 
   386 lemma diff_diff_eq2: "a - (b - c) = (a + c) - (b::'a::ring)"
   387 by (simp add: diff_minus add_ac)
   388 
   389 text{*Further subtraction laws for ordered rings*}
   390 
   391 lemma less_iff_diff_less_0: "(a < b) = (a - b < (0::'a::ordered_ring))"
   392 proof -
   393   have  "(a < b) = (a + (- b) < b + (-b))"  
   394     by (simp only: add_less_cancel_right)
   395   also have "... =  (a - b < 0)" by (simp add: diff_minus)
   396   finally show ?thesis .
   397 qed
   398 
   399 lemma diff_less_eq: "(a-b < c) = (a < c + (b::'a::ordered_ring))"
   400 apply (subst less_iff_diff_less_0)
   401 apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst])
   402 apply (simp add: diff_minus add_ac)
   403 done
   404 
   405 lemma less_diff_eq: "(a < c-b) = (a + (b::'a::ordered_ring) < c)"
   406 apply (subst less_iff_diff_less_0)
   407 apply (rule less_iff_diff_less_0 [of _ "c-b", THEN ssubst])
   408 apply (simp add: diff_minus add_ac)
   409 done
   410 
   411 lemma diff_le_eq: "(a-b \<le> c) = (a \<le> c + (b::'a::ordered_ring))"
   412 by (simp add: linorder_not_less [symmetric] less_diff_eq)
   413 
   414 lemma le_diff_eq: "(a \<le> c-b) = (a + (b::'a::ordered_ring) \<le> c)"
   415 by (simp add: linorder_not_less [symmetric] diff_less_eq)
   416 
   417 text{*This list of rewrites simplifies (in)equalities by bringing subtractions
   418   to the top and then moving negative terms to the other side.
   419   Use with @{text add_ac}*}
   420 lemmas compare_rls =
   421        diff_minus [symmetric]
   422        add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2
   423        diff_less_eq less_diff_eq diff_le_eq le_diff_eq
   424        diff_eq_eq eq_diff_eq
   425 
   426 
   427 subsection{*Lemmas for the @{text cancel_numerals} simproc*}
   428 
   429 lemma eq_iff_diff_eq_0: "(a = b) = (a-b = (0::'a::ring))"
   430 by (simp add: compare_rls)
   431 
   432 lemma le_iff_diff_le_0: "(a \<le> b) = (a-b \<le> (0::'a::ordered_ring))"
   433 by (simp add: compare_rls)
   434 
   435 lemma eq_add_iff1:
   436      "(a*e + c = b*e + d) = ((a-b)*e + c = (d::'a::ring))"
   437 apply (simp add: diff_minus left_distrib add_ac)
   438 apply (simp add: compare_rls minus_mult_left [symmetric]) 
   439 done
   440 
   441 lemma eq_add_iff2:
   442      "(a*e + c = b*e + d) = (c = (b-a)*e + (d::'a::ring))"
   443 apply (simp add: diff_minus left_distrib add_ac)
   444 apply (simp add: compare_rls minus_mult_left [symmetric]) 
   445 done
   446 
   447 lemma less_add_iff1:
   448      "(a*e + c < b*e + d) = ((a-b)*e + c < (d::'a::ordered_ring))"
   449 apply (simp add: diff_minus left_distrib add_ac)
   450 apply (simp add: compare_rls minus_mult_left [symmetric]) 
   451 done
   452 
   453 lemma less_add_iff2:
   454      "(a*e + c < b*e + d) = (c < (b-a)*e + (d::'a::ordered_ring))"
   455 apply (simp add: diff_minus left_distrib add_ac)
   456 apply (simp add: compare_rls minus_mult_left [symmetric]) 
   457 done
   458 
   459 lemma le_add_iff1:
   460      "(a*e + c \<le> b*e + d) = ((a-b)*e + c \<le> (d::'a::ordered_ring))"
   461 apply (simp add: diff_minus left_distrib add_ac)
   462 apply (simp add: compare_rls minus_mult_left [symmetric]) 
   463 done
   464 
   465 lemma le_add_iff2:
   466      "(a*e + c \<le> b*e + d) = (c \<le> (b-a)*e + (d::'a::ordered_ring))"
   467 apply (simp add: diff_minus left_distrib add_ac)
   468 apply (simp add: compare_rls minus_mult_left [symmetric]) 
   469 done
   470 
   471 
   472 subsection {* Ordering Rules for Multiplication *}
   473 
   474 lemma mult_strict_right_mono:
   475      "[|a < b; 0 < c|] ==> a * c < b * (c::'a::ordered_semiring)"
   476 by (simp add: mult_commute [of _ c] mult_strict_left_mono)
   477 
   478 lemma mult_left_mono:
   479      "[|a \<le> b; 0 \<le> c|] ==> c * a \<le> c * (b::'a::ordered_semiring)"
   480   apply (case_tac "c=0", simp)
   481   apply (force simp add: mult_strict_left_mono order_le_less) 
   482   done
   483 
   484 lemma mult_right_mono:
   485      "[|a \<le> b; 0 \<le> c|] ==> a*c \<le> b * (c::'a::ordered_semiring)"
   486   by (simp add: mult_left_mono mult_commute [of _ c]) 
   487 
   488 lemma mult_left_le_imp_le:
   489      "[|c*a \<le> c*b; 0 < c|] ==> a \<le> (b::'a::ordered_semiring)"
   490   by (force simp add: mult_strict_left_mono linorder_not_less [symmetric])
   491  
   492 lemma mult_right_le_imp_le:
   493      "[|a*c \<le> b*c; 0 < c|] ==> a \<le> (b::'a::ordered_semiring)"
   494   by (force simp add: mult_strict_right_mono linorder_not_less [symmetric])
   495 
   496 lemma mult_left_less_imp_less:
   497      "[|c*a < c*b; 0 \<le> c|] ==> a < (b::'a::ordered_semiring)"
   498   by (force simp add: mult_left_mono linorder_not_le [symmetric])
   499  
   500 lemma mult_right_less_imp_less:
   501      "[|a*c < b*c; 0 \<le> c|] ==> a < (b::'a::ordered_semiring)"
   502   by (force simp add: mult_right_mono linorder_not_le [symmetric])
   503 
   504 lemma mult_strict_left_mono_neg:
   505      "[|b < a; c < 0|] ==> c * a < c * (b::'a::ordered_ring)"
   506 apply (drule mult_strict_left_mono [of _ _ "-c"])
   507 apply (simp_all add: minus_mult_left [symmetric]) 
   508 done
   509 
   510 lemma mult_strict_right_mono_neg:
   511      "[|b < a; c < 0|] ==> a * c < b * (c::'a::ordered_ring)"
   512 apply (drule mult_strict_right_mono [of _ _ "-c"])
   513 apply (simp_all add: minus_mult_right [symmetric]) 
   514 done
   515 
   516 
   517 subsection{* Products of Signs *}
   518 
   519 lemma mult_pos: "[| (0::'a::ordered_semiring) < a; 0 < b |] ==> 0 < a*b"
   520 by (drule mult_strict_left_mono [of 0 b], auto)
   521 
   522 lemma mult_pos_neg: "[| (0::'a::ordered_semiring) < a; b < 0 |] ==> a*b < 0"
   523 by (drule mult_strict_left_mono [of b 0], auto)
   524 
   525 lemma mult_neg: "[| a < (0::'a::ordered_ring); b < 0 |] ==> 0 < a*b"
   526 by (drule mult_strict_right_mono_neg, auto)
   527 
   528 lemma zero_less_mult_pos:
   529      "[| 0 < a*b; 0 < a|] ==> 0 < (b::'a::ordered_semiring)"
   530 apply (case_tac "b\<le>0") 
   531  apply (auto simp add: order_le_less linorder_not_less)
   532 apply (drule_tac mult_pos_neg [of a b]) 
   533  apply (auto dest: order_less_not_sym)
   534 done
   535 
   536 lemma zero_less_mult_iff:
   537      "((0::'a::ordered_ring) < a*b) = (0 < a & 0 < b | a < 0 & b < 0)"
   538 apply (auto simp add: order_le_less linorder_not_less mult_pos mult_neg)
   539 apply (blast dest: zero_less_mult_pos) 
   540 apply (simp add: mult_commute [of a b]) 
   541 apply (blast dest: zero_less_mult_pos) 
   542 done
   543 
   544 text{*A field has no "zero divisors", and this theorem holds without the
   545       assumption of an ordering.  See @{text field_mult_eq_0_iff} below.*}
   546 lemma mult_eq_0_iff [simp]: "(a*b = (0::'a::ordered_ring)) = (a = 0 | b = 0)"
   547 apply (case_tac "a < 0")
   548 apply (auto simp add: linorder_not_less order_le_less linorder_neq_iff)
   549 apply (force dest: mult_strict_right_mono_neg mult_strict_right_mono)+
   550 done
   551 
   552 lemma zero_le_mult_iff:
   553      "((0::'a::ordered_ring) \<le> a*b) = (0 \<le> a & 0 \<le> b | a \<le> 0 & b \<le> 0)"
   554 by (auto simp add: eq_commute [of 0] order_le_less linorder_not_less
   555                    zero_less_mult_iff)
   556 
   557 lemma mult_less_0_iff:
   558      "(a*b < (0::'a::ordered_ring)) = (0 < a & b < 0 | a < 0 & 0 < b)"
   559 apply (insert zero_less_mult_iff [of "-a" b]) 
   560 apply (force simp add: minus_mult_left[symmetric]) 
   561 done
   562 
   563 lemma mult_le_0_iff:
   564      "(a*b \<le> (0::'a::ordered_ring)) = (0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> b)"
   565 apply (insert zero_le_mult_iff [of "-a" b]) 
   566 apply (force simp add: minus_mult_left[symmetric]) 
   567 done
   568 
   569 lemma zero_le_square: "(0::'a::ordered_ring) \<le> a*a"
   570 by (simp add: zero_le_mult_iff linorder_linear) 
   571 
   572 lemma zero_le_one: "(0::'a::ordered_semiring) \<le> 1"
   573   by (rule zero_less_one [THEN order_less_imp_le]) 
   574 
   575 
   576 subsection{*More Monotonicity*}
   577 
   578 lemma mult_left_mono_neg:
   579      "[|b \<le> a; c \<le> 0|] ==> c * a \<le> c * (b::'a::ordered_ring)"
   580 apply (drule mult_left_mono [of _ _ "-c"]) 
   581 apply (simp_all add: minus_mult_left [symmetric]) 
   582 done
   583 
   584 lemma mult_right_mono_neg:
   585      "[|b \<le> a; c \<le> 0|] ==> a * c \<le> b * (c::'a::ordered_ring)"
   586   by (simp add: mult_left_mono_neg mult_commute [of _ c]) 
   587 
   588 text{*Strict monotonicity in both arguments*}
   589 lemma mult_strict_mono:
   590      "[|a<b; c<d; 0<b; 0\<le>c|] ==> a * c < b * (d::'a::ordered_semiring)"
   591 apply (case_tac "c=0")
   592  apply (simp add: mult_pos) 
   593 apply (erule mult_strict_right_mono [THEN order_less_trans])
   594  apply (force simp add: order_le_less) 
   595 apply (erule mult_strict_left_mono, assumption)
   596 done
   597 
   598 text{*This weaker variant has more natural premises*}
   599 lemma mult_strict_mono':
   600      "[| a<b; c<d; 0 \<le> a; 0 \<le> c|] ==> a * c < b * (d::'a::ordered_semiring)"
   601 apply (rule mult_strict_mono)
   602 apply (blast intro: order_le_less_trans)+
   603 done
   604 
   605 lemma mult_mono:
   606      "[|a \<le> b; c \<le> d; 0 \<le> b; 0 \<le> c|] 
   607       ==> a * c  \<le>  b * (d::'a::ordered_semiring)"
   608 apply (erule mult_right_mono [THEN order_trans], assumption)
   609 apply (erule mult_left_mono, assumption)
   610 done
   611 
   612 
   613 subsection{*Cancellation Laws for Relationships With a Common Factor*}
   614 
   615 text{*Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"},
   616    also with the relations @{text "\<le>"} and equality.*}
   617 
   618 lemma mult_less_cancel_right:
   619     "(a*c < b*c) = ((0 < c & a < b) | (c < 0 & b < (a::'a::ordered_ring)))"
   620 apply (case_tac "c = 0")
   621 apply (auto simp add: linorder_neq_iff mult_strict_right_mono 
   622                       mult_strict_right_mono_neg)
   623 apply (auto simp add: linorder_not_less 
   624                       linorder_not_le [symmetric, of "a*c"]
   625                       linorder_not_le [symmetric, of a])
   626 apply (erule_tac [!] notE)
   627 apply (auto simp add: order_less_imp_le mult_right_mono 
   628                       mult_right_mono_neg)
   629 done
   630 
   631 lemma mult_less_cancel_left:
   632     "(c*a < c*b) = ((0 < c & a < b) | (c < 0 & b < (a::'a::ordered_ring)))"
   633 by (simp add: mult_commute [of c] mult_less_cancel_right)
   634 
   635 lemma mult_le_cancel_right:
   636      "(a*c \<le> b*c) = ((0<c --> a\<le>b) & (c<0 --> b \<le> (a::'a::ordered_ring)))"
   637 by (simp add: linorder_not_less [symmetric] mult_less_cancel_right)
   638 
   639 lemma mult_le_cancel_left:
   640      "(c*a \<le> c*b) = ((0<c --> a\<le>b) & (c<0 --> b \<le> (a::'a::ordered_ring)))"
   641 by (simp add: mult_commute [of c] mult_le_cancel_right)
   642 
   643 lemma mult_less_imp_less_left:
   644       assumes less: "c*a < c*b" and nonneg: "0 \<le> c"
   645       shows "a < (b::'a::ordered_semiring)"
   646   proof (rule ccontr)
   647     assume "~ a < b"
   648     hence "b \<le> a" by (simp add: linorder_not_less)
   649     hence "c*b \<le> c*a" by (rule mult_left_mono)
   650     with this and less show False 
   651       by (simp add: linorder_not_less [symmetric])
   652   qed
   653 
   654 lemma mult_less_imp_less_right:
   655     "[|a*c < b*c; 0 \<le> c|] ==> a < (b::'a::ordered_semiring)"
   656   by (rule mult_less_imp_less_left, simp add: mult_commute)
   657 
   658 text{*Cancellation of equalities with a common factor*}
   659 lemma mult_cancel_right [simp]:
   660      "(a*c = b*c) = (c = (0::'a::ordered_ring) | a=b)"
   661 apply (cut_tac linorder_less_linear [of 0 c])
   662 apply (force dest: mult_strict_right_mono_neg mult_strict_right_mono
   663              simp add: linorder_neq_iff)
   664 done
   665 
   666 text{*These cancellation theorems require an ordering. Versions are proved
   667       below that work for fields without an ordering.*}
   668 lemma mult_cancel_left [simp]:
   669      "(c*a = c*b) = (c = (0::'a::ordered_ring) | a=b)"
   670 by (simp add: mult_commute [of c] mult_cancel_right)
   671 
   672 
   673 subsection {* Fields *}
   674 
   675 lemma right_inverse [simp]:
   676       assumes not0: "a \<noteq> 0" shows "a * inverse (a::'a::field) = 1"
   677 proof -
   678   have "a * inverse a = inverse a * a" by (simp add: mult_ac)
   679   also have "... = 1" using not0 by simp
   680   finally show ?thesis .
   681 qed
   682 
   683 lemma right_inverse_eq: "b \<noteq> 0 ==> (a / b = 1) = (a = (b::'a::field))"
   684 proof
   685   assume neq: "b \<noteq> 0"
   686   {
   687     hence "a = (a / b) * b" by (simp add: divide_inverse mult_ac)
   688     also assume "a / b = 1"
   689     finally show "a = b" by simp
   690   next
   691     assume "a = b"
   692     with neq show "a / b = 1" by (simp add: divide_inverse)
   693   }
   694 qed
   695 
   696 lemma nonzero_inverse_eq_divide: "a \<noteq> 0 ==> inverse (a::'a::field) = 1/a"
   697 by (simp add: divide_inverse)
   698 
   699 lemma divide_self [simp]: "a \<noteq> 0 ==> a / (a::'a::field) = 1"
   700   by (simp add: divide_inverse)
   701 
   702 lemma divide_inverse_zero: "a/b = a * inverse(b::'a::{field,division_by_zero})"
   703 apply (case_tac "b = 0")
   704 apply (simp_all add: divide_inverse)
   705 done
   706 
   707 lemma divide_zero_left [simp]: "0/a = (0::'a::{field,division_by_zero})"
   708 by (simp add: divide_inverse_zero)
   709 
   710 lemma inverse_eq_divide: "inverse (a::'a::{field,division_by_zero}) = 1/a"
   711 by (simp add: divide_inverse_zero)
   712 
   713 lemma nonzero_add_divide_distrib: "c \<noteq> 0 ==> (a+b)/(c::'a::field) = a/c + b/c"
   714 by (simp add: divide_inverse left_distrib) 
   715 
   716 lemma add_divide_distrib: "(a+b)/(c::'a::{field,division_by_zero}) = a/c + b/c"
   717 apply (case_tac "c=0", simp) 
   718 apply (simp add: nonzero_add_divide_distrib) 
   719 done
   720 
   721 text{*Compared with @{text mult_eq_0_iff}, this version removes the requirement
   722       of an ordering.*}
   723 lemma field_mult_eq_0_iff [simp]: "(a*b = (0::'a::field)) = (a = 0 | b = 0)"
   724   proof cases
   725     assume "a=0" thus ?thesis by simp
   726   next
   727     assume anz [simp]: "a\<noteq>0"
   728     thus ?thesis
   729     proof auto
   730       assume "a * b = 0"
   731       hence "inverse a * (a * b) = 0" by simp
   732       thus "b = 0"  by (simp (no_asm_use) add: mult_assoc [symmetric])
   733     qed
   734   qed
   735 
   736 text{*Cancellation of equalities with a common factor*}
   737 lemma field_mult_cancel_right_lemma:
   738       assumes cnz: "c \<noteq> (0::'a::field)"
   739 	  and eq:  "a*c = b*c"
   740 	 shows "a=b"
   741   proof -
   742   have "(a * c) * inverse c = (b * c) * inverse c"
   743     by (simp add: eq)
   744   thus "a=b"
   745     by (simp add: mult_assoc cnz)
   746   qed
   747 
   748 lemma field_mult_cancel_right [simp]:
   749      "(a*c = b*c) = (c = (0::'a::field) | a=b)"
   750   proof cases
   751     assume "c=0" thus ?thesis by simp
   752   next
   753     assume "c\<noteq>0" 
   754     thus ?thesis by (force dest: field_mult_cancel_right_lemma)
   755   qed
   756 
   757 lemma field_mult_cancel_left [simp]:
   758      "(c*a = c*b) = (c = (0::'a::field) | a=b)"
   759   by (simp add: mult_commute [of c] field_mult_cancel_right) 
   760 
   761 lemma nonzero_imp_inverse_nonzero: "a \<noteq> 0 ==> inverse a \<noteq> (0::'a::field)"
   762   proof
   763   assume ianz: "inverse a = 0"
   764   assume "a \<noteq> 0"
   765   hence "1 = a * inverse a" by simp
   766   also have "... = 0" by (simp add: ianz)
   767   finally have "1 = (0::'a::field)" .
   768   thus False by (simp add: eq_commute)
   769   qed
   770 
   771 
   772 subsection{*Basic Properties of @{term inverse}*}
   773 
   774 lemma inverse_zero_imp_zero: "inverse a = 0 ==> a = (0::'a::field)"
   775 apply (rule ccontr) 
   776 apply (blast dest: nonzero_imp_inverse_nonzero) 
   777 done
   778 
   779 lemma inverse_nonzero_imp_nonzero:
   780    "inverse a = 0 ==> a = (0::'a::field)"
   781 apply (rule ccontr) 
   782 apply (blast dest: nonzero_imp_inverse_nonzero) 
   783 done
   784 
   785 lemma inverse_nonzero_iff_nonzero [simp]:
   786    "(inverse a = 0) = (a = (0::'a::{field,division_by_zero}))"
   787 by (force dest: inverse_nonzero_imp_nonzero) 
   788 
   789 lemma nonzero_inverse_minus_eq:
   790       assumes [simp]: "a\<noteq>0"  shows "inverse(-a) = -inverse(a::'a::field)"
   791   proof -
   792     have "-a * inverse (- a) = -a * - inverse a"
   793       by simp
   794     thus ?thesis 
   795       by (simp only: field_mult_cancel_left, simp)
   796   qed
   797 
   798 lemma inverse_minus_eq [simp]:
   799      "inverse(-a) = -inverse(a::'a::{field,division_by_zero})";
   800   proof cases
   801     assume "a=0" thus ?thesis by (simp add: inverse_zero)
   802   next
   803     assume "a\<noteq>0" 
   804     thus ?thesis by (simp add: nonzero_inverse_minus_eq)
   805   qed
   806 
   807 lemma nonzero_inverse_eq_imp_eq:
   808       assumes inveq: "inverse a = inverse b"
   809 	  and anz:  "a \<noteq> 0"
   810 	  and bnz:  "b \<noteq> 0"
   811 	 shows "a = (b::'a::field)"
   812   proof -
   813   have "a * inverse b = a * inverse a"
   814     by (simp add: inveq)
   815   hence "(a * inverse b) * b = (a * inverse a) * b"
   816     by simp
   817   thus "a = b"
   818     by (simp add: mult_assoc anz bnz)
   819   qed
   820 
   821 lemma inverse_eq_imp_eq:
   822      "inverse a = inverse b ==> a = (b::'a::{field,division_by_zero})"
   823 apply (case_tac "a=0 | b=0") 
   824  apply (force dest!: inverse_zero_imp_zero
   825               simp add: eq_commute [of "0::'a"])
   826 apply (force dest!: nonzero_inverse_eq_imp_eq) 
   827 done
   828 
   829 lemma inverse_eq_iff_eq [simp]:
   830      "(inverse a = inverse b) = (a = (b::'a::{field,division_by_zero}))"
   831 by (force dest!: inverse_eq_imp_eq) 
   832 
   833 lemma nonzero_inverse_inverse_eq:
   834       assumes [simp]: "a \<noteq> 0"  shows "inverse(inverse (a::'a::field)) = a"
   835   proof -
   836   have "(inverse (inverse a) * inverse a) * a = a" 
   837     by (simp add: nonzero_imp_inverse_nonzero)
   838   thus ?thesis
   839     by (simp add: mult_assoc)
   840   qed
   841 
   842 lemma inverse_inverse_eq [simp]:
   843      "inverse(inverse (a::'a::{field,division_by_zero})) = a"
   844   proof cases
   845     assume "a=0" thus ?thesis by simp
   846   next
   847     assume "a\<noteq>0" 
   848     thus ?thesis by (simp add: nonzero_inverse_inverse_eq)
   849   qed
   850 
   851 lemma inverse_1 [simp]: "inverse 1 = (1::'a::field)"
   852   proof -
   853   have "inverse 1 * 1 = (1::'a::field)" 
   854     by (rule left_inverse [OF zero_neq_one [symmetric]])
   855   thus ?thesis  by simp
   856   qed
   857 
   858 lemma nonzero_inverse_mult_distrib: 
   859       assumes anz: "a \<noteq> 0"
   860           and bnz: "b \<noteq> 0"
   861       shows "inverse(a*b) = inverse(b) * inverse(a::'a::field)"
   862   proof -
   863   have "inverse(a*b) * (a * b) * inverse(b) = inverse(b)" 
   864     by (simp add: field_mult_eq_0_iff anz bnz)
   865   hence "inverse(a*b) * a = inverse(b)" 
   866     by (simp add: mult_assoc bnz)
   867   hence "inverse(a*b) * a * inverse(a) = inverse(b) * inverse(a)" 
   868     by simp
   869   thus ?thesis
   870     by (simp add: mult_assoc anz)
   871   qed
   872 
   873 text{*This version builds in division by zero while also re-orienting
   874       the right-hand side.*}
   875 lemma inverse_mult_distrib [simp]:
   876      "inverse(a*b) = inverse(a) * inverse(b::'a::{field,division_by_zero})"
   877   proof cases
   878     assume "a \<noteq> 0 & b \<noteq> 0" 
   879     thus ?thesis  by (simp add: nonzero_inverse_mult_distrib mult_commute)
   880   next
   881     assume "~ (a \<noteq> 0 & b \<noteq> 0)" 
   882     thus ?thesis  by force
   883   qed
   884 
   885 text{*There is no slick version using division by zero.*}
   886 lemma inverse_add:
   887      "[|a \<noteq> 0;  b \<noteq> 0|]
   888       ==> inverse a + inverse b = (a+b) * inverse a * inverse (b::'a::field)"
   889 apply (simp add: left_distrib mult_assoc)
   890 apply (simp add: mult_commute [of "inverse a"]) 
   891 apply (simp add: mult_assoc [symmetric] add_commute)
   892 done
   893 
   894 lemma nonzero_mult_divide_cancel_left:
   895   assumes [simp]: "b\<noteq>0" and [simp]: "c\<noteq>0" 
   896     shows "(c*a)/(c*b) = a/(b::'a::field)"
   897 proof -
   898   have "(c*a)/(c*b) = c * a * (inverse b * inverse c)"
   899     by (simp add: field_mult_eq_0_iff divide_inverse 
   900                   nonzero_inverse_mult_distrib)
   901   also have "... =  a * inverse b * (inverse c * c)"
   902     by (simp only: mult_ac)
   903   also have "... =  a * inverse b"
   904     by simp
   905     finally show ?thesis 
   906     by (simp add: divide_inverse)
   907 qed
   908 
   909 lemma mult_divide_cancel_left:
   910      "c\<noteq>0 ==> (c*a) / (c*b) = a / (b::'a::{field,division_by_zero})"
   911 apply (case_tac "b = 0")
   912 apply (simp_all add: nonzero_mult_divide_cancel_left)
   913 done
   914 
   915 lemma nonzero_mult_divide_cancel_right:
   916      "[|b\<noteq>0; c\<noteq>0|] ==> (a*c) / (b*c) = a/(b::'a::field)"
   917 by (simp add: mult_commute [of _ c] nonzero_mult_divide_cancel_left) 
   918 
   919 lemma mult_divide_cancel_right:
   920      "c\<noteq>0 ==> (a*c) / (b*c) = a / (b::'a::{field,division_by_zero})"
   921 apply (case_tac "b = 0")
   922 apply (simp_all add: nonzero_mult_divide_cancel_right)
   923 done
   924 
   925 (*For ExtractCommonTerm*)
   926 lemma mult_divide_cancel_eq_if:
   927      "(c*a) / (c*b) = 
   928       (if c=0 then 0 else a / (b::'a::{field,division_by_zero}))"
   929   by (simp add: mult_divide_cancel_left)
   930 
   931 lemma divide_1 [simp]: "a/1 = (a::'a::field)"
   932   by (simp add: divide_inverse [OF not_sym])
   933 
   934 lemma times_divide_eq_right [simp]:
   935      "a * (b/c) = (a*b) / (c::'a::{field,division_by_zero})"
   936 by (simp add: divide_inverse_zero mult_assoc)
   937 
   938 lemma times_divide_eq_left [simp]:
   939      "(b/c) * a = (b*a) / (c::'a::{field,division_by_zero})"
   940 by (simp add: divide_inverse_zero mult_ac)
   941 
   942 lemma divide_divide_eq_right [simp]:
   943      "a / (b/c) = (a*c) / (b::'a::{field,division_by_zero})"
   944 by (simp add: divide_inverse_zero mult_ac)
   945 
   946 lemma divide_divide_eq_left [simp]:
   947      "(a / b) / (c::'a::{field,division_by_zero}) = a / (b*c)"
   948 by (simp add: divide_inverse_zero mult_assoc)
   949 
   950 
   951 subsection {* Division and Unary Minus *}
   952 
   953 lemma nonzero_minus_divide_left: "b \<noteq> 0 ==> - (a/b) = (-a) / (b::'a::field)"
   954 by (simp add: divide_inverse minus_mult_left)
   955 
   956 lemma nonzero_minus_divide_right: "b \<noteq> 0 ==> - (a/b) = a / -(b::'a::field)"
   957 by (simp add: divide_inverse nonzero_inverse_minus_eq minus_mult_right)
   958 
   959 lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (-a)/(-b) = a / (b::'a::field)"
   960 by (simp add: divide_inverse nonzero_inverse_minus_eq)
   961 
   962 lemma minus_divide_left: "- (a/b) = (-a) / (b::'a::{field,division_by_zero})"
   963 apply (case_tac "b=0", simp) 
   964 apply (simp add: nonzero_minus_divide_left) 
   965 done
   966 
   967 lemma minus_divide_right: "- (a/b) = a / -(b::'a::{field,division_by_zero})"
   968 apply (case_tac "b=0", simp) 
   969 by (rule nonzero_minus_divide_right) 
   970 
   971 text{*The effect is to extract signs from divisions*}
   972 declare minus_divide_left  [symmetric, simp]
   973 declare minus_divide_right [symmetric, simp]
   974 
   975 lemma minus_divide_divide [simp]:
   976      "(-a)/(-b) = a / (b::'a::{field,division_by_zero})"
   977 apply (case_tac "b=0", simp) 
   978 apply (simp add: nonzero_minus_divide_divide) 
   979 done
   980 
   981 
   982 subsection {* Ordered Fields *}
   983 
   984 lemma positive_imp_inverse_positive: 
   985       assumes a_gt_0: "0 < a"  shows "0 < inverse (a::'a::ordered_field)"
   986   proof -
   987   have "0 < a * inverse a" 
   988     by (simp add: a_gt_0 [THEN order_less_imp_not_eq2] zero_less_one)
   989   thus "0 < inverse a" 
   990     by (simp add: a_gt_0 [THEN order_less_not_sym] zero_less_mult_iff)
   991   qed
   992 
   993 lemma negative_imp_inverse_negative:
   994      "a < 0 ==> inverse a < (0::'a::ordered_field)"
   995   by (insert positive_imp_inverse_positive [of "-a"], 
   996       simp add: nonzero_inverse_minus_eq order_less_imp_not_eq) 
   997 
   998 lemma inverse_le_imp_le:
   999       assumes invle: "inverse a \<le> inverse b"
  1000 	  and apos:  "0 < a"
  1001 	 shows "b \<le> (a::'a::ordered_field)"
  1002   proof (rule classical)
  1003   assume "~ b \<le> a"
  1004   hence "a < b"
  1005     by (simp add: linorder_not_le)
  1006   hence bpos: "0 < b"
  1007     by (blast intro: apos order_less_trans)
  1008   hence "a * inverse a \<le> a * inverse b"
  1009     by (simp add: apos invle order_less_imp_le mult_left_mono)
  1010   hence "(a * inverse a) * b \<le> (a * inverse b) * b"
  1011     by (simp add: bpos order_less_imp_le mult_right_mono)
  1012   thus "b \<le> a"
  1013     by (simp add: mult_assoc apos bpos order_less_imp_not_eq2)
  1014   qed
  1015 
  1016 lemma inverse_positive_imp_positive:
  1017       assumes inv_gt_0: "0 < inverse a"
  1018           and [simp]:   "a \<noteq> 0"
  1019         shows "0 < (a::'a::ordered_field)"
  1020   proof -
  1021   have "0 < inverse (inverse a)"
  1022     by (rule positive_imp_inverse_positive)
  1023   thus "0 < a"
  1024     by (simp add: nonzero_inverse_inverse_eq)
  1025   qed
  1026 
  1027 lemma inverse_positive_iff_positive [simp]:
  1028       "(0 < inverse a) = (0 < (a::'a::{ordered_field,division_by_zero}))"
  1029 apply (case_tac "a = 0", simp)
  1030 apply (blast intro: inverse_positive_imp_positive positive_imp_inverse_positive)
  1031 done
  1032 
  1033 lemma inverse_negative_imp_negative:
  1034       assumes inv_less_0: "inverse a < 0"
  1035           and [simp]:   "a \<noteq> 0"
  1036         shows "a < (0::'a::ordered_field)"
  1037   proof -
  1038   have "inverse (inverse a) < 0"
  1039     by (rule negative_imp_inverse_negative)
  1040   thus "a < 0"
  1041     by (simp add: nonzero_inverse_inverse_eq)
  1042   qed
  1043 
  1044 lemma inverse_negative_iff_negative [simp]:
  1045       "(inverse a < 0) = (a < (0::'a::{ordered_field,division_by_zero}))"
  1046 apply (case_tac "a = 0", simp)
  1047 apply (blast intro: inverse_negative_imp_negative negative_imp_inverse_negative)
  1048 done
  1049 
  1050 lemma inverse_nonnegative_iff_nonnegative [simp]:
  1051       "(0 \<le> inverse a) = (0 \<le> (a::'a::{ordered_field,division_by_zero}))"
  1052 by (simp add: linorder_not_less [symmetric])
  1053 
  1054 lemma inverse_nonpositive_iff_nonpositive [simp]:
  1055       "(inverse a \<le> 0) = (a \<le> (0::'a::{ordered_field,division_by_zero}))"
  1056 by (simp add: linorder_not_less [symmetric])
  1057 
  1058 
  1059 subsection{*Anti-Monotonicity of @{term inverse}*}
  1060 
  1061 lemma less_imp_inverse_less:
  1062       assumes less: "a < b"
  1063 	  and apos:  "0 < a"
  1064 	shows "inverse b < inverse (a::'a::ordered_field)"
  1065   proof (rule ccontr)
  1066   assume "~ inverse b < inverse a"
  1067   hence "inverse a \<le> inverse b"
  1068     by (simp add: linorder_not_less)
  1069   hence "~ (a < b)"
  1070     by (simp add: linorder_not_less inverse_le_imp_le [OF _ apos])
  1071   thus False
  1072     by (rule notE [OF _ less])
  1073   qed
  1074 
  1075 lemma inverse_less_imp_less:
  1076    "[|inverse a < inverse b; 0 < a|] ==> b < (a::'a::ordered_field)"
  1077 apply (simp add: order_less_le [of "inverse a"] order_less_le [of "b"])
  1078 apply (force dest!: inverse_le_imp_le nonzero_inverse_eq_imp_eq) 
  1079 done
  1080 
  1081 text{*Both premises are essential. Consider -1 and 1.*}
  1082 lemma inverse_less_iff_less [simp]:
  1083      "[|0 < a; 0 < b|] 
  1084       ==> (inverse a < inverse b) = (b < (a::'a::ordered_field))"
  1085 by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less) 
  1086 
  1087 lemma le_imp_inverse_le:
  1088    "[|a \<le> b; 0 < a|] ==> inverse b \<le> inverse (a::'a::ordered_field)"
  1089   by (force simp add: order_le_less less_imp_inverse_less)
  1090 
  1091 lemma inverse_le_iff_le [simp]:
  1092      "[|0 < a; 0 < b|] 
  1093       ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::ordered_field))"
  1094 by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le) 
  1095 
  1096 
  1097 text{*These results refer to both operands being negative.  The opposite-sign
  1098 case is trivial, since inverse preserves signs.*}
  1099 lemma inverse_le_imp_le_neg:
  1100    "[|inverse a \<le> inverse b; b < 0|] ==> b \<le> (a::'a::ordered_field)"
  1101   apply (rule classical) 
  1102   apply (subgoal_tac "a < 0") 
  1103    prefer 2 apply (force simp add: linorder_not_le intro: order_less_trans) 
  1104   apply (insert inverse_le_imp_le [of "-b" "-a"])
  1105   apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
  1106   done
  1107 
  1108 lemma less_imp_inverse_less_neg:
  1109    "[|a < b; b < 0|] ==> inverse b < inverse (a::'a::ordered_field)"
  1110   apply (subgoal_tac "a < 0") 
  1111    prefer 2 apply (blast intro: order_less_trans) 
  1112   apply (insert less_imp_inverse_less [of "-b" "-a"])
  1113   apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
  1114   done
  1115 
  1116 lemma inverse_less_imp_less_neg:
  1117    "[|inverse a < inverse b; b < 0|] ==> b < (a::'a::ordered_field)"
  1118   apply (rule classical) 
  1119   apply (subgoal_tac "a < 0") 
  1120    prefer 2
  1121    apply (force simp add: linorder_not_less intro: order_le_less_trans) 
  1122   apply (insert inverse_less_imp_less [of "-b" "-a"])
  1123   apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
  1124   done
  1125 
  1126 lemma inverse_less_iff_less_neg [simp]:
  1127      "[|a < 0; b < 0|] 
  1128       ==> (inverse a < inverse b) = (b < (a::'a::ordered_field))"
  1129   apply (insert inverse_less_iff_less [of "-b" "-a"])
  1130   apply (simp del: inverse_less_iff_less 
  1131 	      add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
  1132   done
  1133 
  1134 lemma le_imp_inverse_le_neg:
  1135    "[|a \<le> b; b < 0|] ==> inverse b \<le> inverse (a::'a::ordered_field)"
  1136   by (force simp add: order_le_less less_imp_inverse_less_neg)
  1137 
  1138 lemma inverse_le_iff_le_neg [simp]:
  1139      "[|a < 0; b < 0|] 
  1140       ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::ordered_field))"
  1141 by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg) 
  1142 
  1143 
  1144 subsection{*Division and Signs*}
  1145 
  1146 lemma zero_less_divide_iff:
  1147      "((0::'a::{ordered_field,division_by_zero}) < a/b) = (0 < a & 0 < b | a < 0 & b < 0)"
  1148 by (simp add: divide_inverse_zero zero_less_mult_iff)
  1149 
  1150 lemma divide_less_0_iff:
  1151      "(a/b < (0::'a::{ordered_field,division_by_zero})) = 
  1152       (0 < a & b < 0 | a < 0 & 0 < b)"
  1153 by (simp add: divide_inverse_zero mult_less_0_iff)
  1154 
  1155 lemma zero_le_divide_iff:
  1156      "((0::'a::{ordered_field,division_by_zero}) \<le> a/b) =
  1157       (0 \<le> a & 0 \<le> b | a \<le> 0 & b \<le> 0)"
  1158 by (simp add: divide_inverse_zero zero_le_mult_iff)
  1159 
  1160 lemma divide_le_0_iff:
  1161      "(a/b \<le> (0::'a::{ordered_field,division_by_zero})) =
  1162       (0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> b)"
  1163 by (simp add: divide_inverse_zero mult_le_0_iff)
  1164 
  1165 lemma divide_eq_0_iff [simp]:
  1166      "(a/b = 0) = (a=0 | b=(0::'a::{field,division_by_zero}))"
  1167 by (simp add: divide_inverse_zero field_mult_eq_0_iff)
  1168 
  1169 
  1170 subsection{*Simplification of Inequalities Involving Literal Divisors*}
  1171 
  1172 lemma pos_le_divide_eq: "0 < (c::'a::ordered_field) ==> (a \<le> b/c) = (a*c \<le> b)"
  1173 proof -
  1174   assume less: "0<c"
  1175   hence "(a \<le> b/c) = (a*c \<le> (b/c)*c)"
  1176     by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
  1177   also have "... = (a*c \<le> b)"
  1178     by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc) 
  1179   finally show ?thesis .
  1180 qed
  1181 
  1182 
  1183 lemma neg_le_divide_eq: "c < (0::'a::ordered_field) ==> (a \<le> b/c) = (b \<le> a*c)"
  1184 proof -
  1185   assume less: "c<0"
  1186   hence "(a \<le> b/c) = ((b/c)*c \<le> a*c)"
  1187     by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
  1188   also have "... = (b \<le> a*c)"
  1189     by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc) 
  1190   finally show ?thesis .
  1191 qed
  1192 
  1193 lemma le_divide_eq:
  1194   "(a \<le> b/c) = 
  1195    (if 0 < c then a*c \<le> b
  1196              else if c < 0 then b \<le> a*c
  1197              else  a \<le> (0::'a::{ordered_field,division_by_zero}))"
  1198 apply (case_tac "c=0", simp) 
  1199 apply (force simp add: pos_le_divide_eq neg_le_divide_eq linorder_neq_iff) 
  1200 done
  1201 
  1202 lemma pos_divide_le_eq: "0 < (c::'a::ordered_field) ==> (b/c \<le> a) = (b \<le> a*c)"
  1203 proof -
  1204   assume less: "0<c"
  1205   hence "(b/c \<le> a) = ((b/c)*c \<le> a*c)"
  1206     by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
  1207   also have "... = (b \<le> a*c)"
  1208     by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc) 
  1209   finally show ?thesis .
  1210 qed
  1211 
  1212 lemma neg_divide_le_eq: "c < (0::'a::ordered_field) ==> (b/c \<le> a) = (a*c \<le> b)"
  1213 proof -
  1214   assume less: "c<0"
  1215   hence "(b/c \<le> a) = (a*c \<le> (b/c)*c)"
  1216     by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
  1217   also have "... = (a*c \<le> b)"
  1218     by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc) 
  1219   finally show ?thesis .
  1220 qed
  1221 
  1222 lemma divide_le_eq:
  1223   "(b/c \<le> a) = 
  1224    (if 0 < c then b \<le> a*c
  1225              else if c < 0 then a*c \<le> b
  1226              else 0 \<le> (a::'a::{ordered_field,division_by_zero}))"
  1227 apply (case_tac "c=0", simp) 
  1228 apply (force simp add: pos_divide_le_eq neg_divide_le_eq linorder_neq_iff) 
  1229 done
  1230 
  1231 
  1232 lemma pos_less_divide_eq:
  1233      "0 < (c::'a::ordered_field) ==> (a < b/c) = (a*c < b)"
  1234 proof -
  1235   assume less: "0<c"
  1236   hence "(a < b/c) = (a*c < (b/c)*c)"
  1237     by (simp add: mult_less_cancel_right order_less_not_sym [OF less])
  1238   also have "... = (a*c < b)"
  1239     by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc) 
  1240   finally show ?thesis .
  1241 qed
  1242 
  1243 lemma neg_less_divide_eq:
  1244  "c < (0::'a::ordered_field) ==> (a < b/c) = (b < a*c)"
  1245 proof -
  1246   assume less: "c<0"
  1247   hence "(a < b/c) = ((b/c)*c < a*c)"
  1248     by (simp add: mult_less_cancel_right order_less_not_sym [OF less])
  1249   also have "... = (b < a*c)"
  1250     by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc) 
  1251   finally show ?thesis .
  1252 qed
  1253 
  1254 lemma less_divide_eq:
  1255   "(a < b/c) = 
  1256    (if 0 < c then a*c < b
  1257              else if c < 0 then b < a*c
  1258              else  a < (0::'a::{ordered_field,division_by_zero}))"
  1259 apply (case_tac "c=0", simp) 
  1260 apply (force simp add: pos_less_divide_eq neg_less_divide_eq linorder_neq_iff) 
  1261 done
  1262 
  1263 lemma pos_divide_less_eq:
  1264      "0 < (c::'a::ordered_field) ==> (b/c < a) = (b < a*c)"
  1265 proof -
  1266   assume less: "0<c"
  1267   hence "(b/c < a) = ((b/c)*c < a*c)"
  1268     by (simp add: mult_less_cancel_right order_less_not_sym [OF less])
  1269   also have "... = (b < a*c)"
  1270     by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc) 
  1271   finally show ?thesis .
  1272 qed
  1273 
  1274 lemma neg_divide_less_eq:
  1275  "c < (0::'a::ordered_field) ==> (b/c < a) = (a*c < b)"
  1276 proof -
  1277   assume less: "c<0"
  1278   hence "(b/c < a) = (a*c < (b/c)*c)"
  1279     by (simp add: mult_less_cancel_right order_less_not_sym [OF less])
  1280   also have "... = (a*c < b)"
  1281     by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc) 
  1282   finally show ?thesis .
  1283 qed
  1284 
  1285 lemma divide_less_eq:
  1286   "(b/c < a) = 
  1287    (if 0 < c then b < a*c
  1288              else if c < 0 then a*c < b
  1289              else 0 < (a::'a::{ordered_field,division_by_zero}))"
  1290 apply (case_tac "c=0", simp) 
  1291 apply (force simp add: pos_divide_less_eq neg_divide_less_eq linorder_neq_iff) 
  1292 done
  1293 
  1294 lemma nonzero_eq_divide_eq: "c\<noteq>0 ==> ((a::'a::field) = b/c) = (a*c = b)"
  1295 proof -
  1296   assume [simp]: "c\<noteq>0"
  1297   have "(a = b/c) = (a*c = (b/c)*c)"
  1298     by (simp add: field_mult_cancel_right)
  1299   also have "... = (a*c = b)"
  1300     by (simp add: divide_inverse mult_assoc) 
  1301   finally show ?thesis .
  1302 qed
  1303 
  1304 lemma eq_divide_eq:
  1305   "((a::'a::{field,division_by_zero}) = b/c) = (if c\<noteq>0 then a*c = b else a=0)"
  1306 by (simp add: nonzero_eq_divide_eq) 
  1307 
  1308 lemma nonzero_divide_eq_eq: "c\<noteq>0 ==> (b/c = (a::'a::field)) = (b = a*c)"
  1309 proof -
  1310   assume [simp]: "c\<noteq>0"
  1311   have "(b/c = a) = ((b/c)*c = a*c)"
  1312     by (simp add: field_mult_cancel_right)
  1313   also have "... = (b = a*c)"
  1314     by (simp add: divide_inverse mult_assoc) 
  1315   finally show ?thesis .
  1316 qed
  1317 
  1318 lemma divide_eq_eq:
  1319   "(b/c = (a::'a::{field,division_by_zero})) = (if c\<noteq>0 then b = a*c else a=0)"
  1320 by (force simp add: nonzero_divide_eq_eq) 
  1321 
  1322 subsection{*Cancellation Laws for Division*}
  1323 
  1324 lemma divide_cancel_right [simp]:
  1325      "(a/c = b/c) = (c = 0 | a = (b::'a::{field,division_by_zero}))"
  1326 apply (case_tac "c=0", simp) 
  1327 apply (simp add: divide_inverse_zero field_mult_cancel_right) 
  1328 done
  1329 
  1330 lemma divide_cancel_left [simp]:
  1331      "(c/a = c/b) = (c = 0 | a = (b::'a::{field,division_by_zero}))" 
  1332 apply (case_tac "c=0", simp) 
  1333 apply (simp add: divide_inverse_zero field_mult_cancel_left) 
  1334 done
  1335 
  1336 
  1337 subsection {* Ordering Rules for Division *}
  1338 
  1339 lemma divide_strict_right_mono:
  1340      "[|a < b; 0 < c|] ==> a / c < b / (c::'a::ordered_field)"
  1341 by (simp add: order_less_imp_not_eq2 divide_inverse mult_strict_right_mono 
  1342               positive_imp_inverse_positive) 
  1343 
  1344 lemma divide_right_mono:
  1345      "[|a \<le> b; 0 \<le> c|] ==> a/c \<le> b/(c::'a::{ordered_field,division_by_zero})"
  1346   by (force simp add: divide_strict_right_mono order_le_less) 
  1347 
  1348 
  1349 text{*The last premise ensures that @{term a} and @{term b} 
  1350       have the same sign*}
  1351 lemma divide_strict_left_mono:
  1352        "[|b < a; 0 < c; 0 < a*b|] ==> c / a < c / (b::'a::ordered_field)"
  1353 by (force simp add: zero_less_mult_iff divide_inverse mult_strict_left_mono 
  1354       order_less_imp_not_eq order_less_imp_not_eq2  
  1355       less_imp_inverse_less less_imp_inverse_less_neg) 
  1356 
  1357 lemma divide_left_mono:
  1358      "[|b \<le> a; 0 \<le> c; 0 < a*b|] ==> c / a \<le> c / (b::'a::ordered_field)"
  1359   apply (subgoal_tac "a \<noteq> 0 & b \<noteq> 0") 
  1360    prefer 2 
  1361    apply (force simp add: zero_less_mult_iff order_less_imp_not_eq) 
  1362   apply (case_tac "c=0", simp add: divide_inverse)
  1363   apply (force simp add: divide_strict_left_mono order_le_less) 
  1364   done
  1365 
  1366 lemma divide_strict_left_mono_neg:
  1367      "[|a < b; c < 0; 0 < a*b|] ==> c / a < c / (b::'a::ordered_field)"
  1368   apply (subgoal_tac "a \<noteq> 0 & b \<noteq> 0") 
  1369    prefer 2 
  1370    apply (force simp add: zero_less_mult_iff order_less_imp_not_eq) 
  1371   apply (drule divide_strict_left_mono [of _ _ "-c"]) 
  1372    apply (simp_all add: mult_commute nonzero_minus_divide_left [symmetric]) 
  1373   done
  1374 
  1375 lemma divide_strict_right_mono_neg:
  1376      "[|b < a; c < 0|] ==> a / c < b / (c::'a::ordered_field)"
  1377 apply (drule divide_strict_right_mono [of _ _ "-c"], simp) 
  1378 apply (simp add: order_less_imp_not_eq nonzero_minus_divide_right [symmetric]) 
  1379 done
  1380 
  1381 
  1382 subsection {* Ordered Fields are Dense *}
  1383 
  1384 lemma zero_less_two: "0 < (1+1::'a::ordered_field)"
  1385 proof -
  1386   have "0 + 0 <  (1+1::'a::ordered_field)"
  1387     by (blast intro: zero_less_one add_strict_mono) 
  1388   thus ?thesis by simp
  1389 qed
  1390 
  1391 lemma less_half_sum: "a < b ==> a < (a+b) / (1+1::'a::ordered_field)"
  1392 by (simp add: zero_less_two pos_less_divide_eq right_distrib) 
  1393 
  1394 lemma gt_half_sum: "a < b ==> (a+b)/(1+1::'a::ordered_field) < b"
  1395 by (simp add: zero_less_two pos_divide_less_eq right_distrib) 
  1396 
  1397 lemma dense: "a < b ==> \<exists>r::'a::ordered_field. a < r & r < b"
  1398 by (blast intro!: less_half_sum gt_half_sum)
  1399 
  1400 
  1401 subsection {* Absolute Value *}
  1402 
  1403 lemma abs_zero [simp]: "abs 0 = (0::'a::ordered_ring)"
  1404 by (simp add: abs_if)
  1405 
  1406 lemma abs_one [simp]: "abs 1 = (1::'a::ordered_ring)"
  1407   by (simp add: abs_if zero_less_one [THEN order_less_not_sym]) 
  1408 
  1409 lemma abs_mult: "abs (a * b) = abs a * abs (b::'a::ordered_ring)" 
  1410 apply (case_tac "a=0 | b=0", force) 
  1411 apply (auto elim: order_less_asym
  1412             simp add: abs_if mult_less_0_iff linorder_neq_iff
  1413                   minus_mult_left [symmetric] minus_mult_right [symmetric])  
  1414 done
  1415 
  1416 
  1417 lemma abs_mult_self: "abs a * abs a = a * (a::'a::ordered_ring)"
  1418 by (simp add: abs_if) 
  1419 
  1420 lemma abs_eq_0 [simp]: "(abs a = 0) = (a = (0::'a::ordered_ring))"
  1421 by (simp add: abs_if)
  1422 
  1423 lemma zero_less_abs_iff [simp]: "(0 < abs a) = (a \<noteq> (0::'a::ordered_ring))"
  1424 by (simp add: abs_if linorder_neq_iff)
  1425 
  1426 lemma abs_not_less_zero [simp]: "~ abs a < (0::'a::ordered_ring)"
  1427 by (simp add: abs_if  order_less_not_sym [of a 0])
  1428 
  1429 lemma abs_le_zero_iff [simp]: "(abs a \<le> (0::'a::ordered_ring)) = (a = 0)" 
  1430 by (simp add: order_le_less) 
  1431 
  1432 lemma abs_minus_cancel [simp]: "abs (-a) = abs(a::'a::ordered_ring)"
  1433 apply (auto simp add: abs_if linorder_not_less order_less_not_sym [of 0 a])  
  1434 apply (drule order_antisym, assumption, simp) 
  1435 done
  1436 
  1437 lemma abs_ge_zero [simp]: "(0::'a::ordered_ring) \<le> abs a"
  1438 apply (simp add: abs_if order_less_imp_le)
  1439 apply (simp add: linorder_not_less) 
  1440 done
  1441 
  1442 lemma abs_idempotent [simp]: "abs (abs a) = abs (a::'a::ordered_ring)"
  1443   by (force elim: order_less_asym simp add: abs_if)
  1444 
  1445 lemma abs_zero_iff [simp]: "(abs a = 0) = (a = (0::'a::ordered_ring))"
  1446 by (simp add: abs_if)
  1447 
  1448 lemma abs_ge_self: "a \<le> abs (a::'a::ordered_ring)"
  1449 apply (simp add: abs_if)
  1450 apply (simp add: order_less_imp_le order_trans [of _ 0])
  1451 done
  1452 
  1453 lemma abs_ge_minus_self: "-a \<le> abs (a::'a::ordered_ring)"
  1454 by (insert abs_ge_self [of "-a"], simp)
  1455 
  1456 lemma nonzero_abs_inverse:
  1457      "a \<noteq> 0 ==> abs (inverse (a::'a::ordered_field)) = inverse (abs a)"
  1458 apply (auto simp add: linorder_neq_iff abs_if nonzero_inverse_minus_eq 
  1459                       negative_imp_inverse_negative)
  1460 apply (blast intro: positive_imp_inverse_positive elim: order_less_asym) 
  1461 done
  1462 
  1463 lemma abs_inverse [simp]:
  1464      "abs (inverse (a::'a::{ordered_field,division_by_zero})) = 
  1465       inverse (abs a)"
  1466 apply (case_tac "a=0", simp) 
  1467 apply (simp add: nonzero_abs_inverse) 
  1468 done
  1469 
  1470 lemma nonzero_abs_divide:
  1471      "b \<noteq> 0 ==> abs (a / (b::'a::ordered_field)) = abs a / abs b"
  1472 by (simp add: divide_inverse abs_mult nonzero_abs_inverse) 
  1473 
  1474 lemma abs_divide:
  1475      "abs (a / (b::'a::{ordered_field,division_by_zero})) = abs a / abs b"
  1476 apply (case_tac "b=0", simp) 
  1477 apply (simp add: nonzero_abs_divide) 
  1478 done
  1479 
  1480 lemma abs_leI: "[|a \<le> b; -a \<le> b|] ==> abs a \<le> (b::'a::ordered_ring)"
  1481 by (simp add: abs_if)
  1482 
  1483 lemma le_minus_self_iff: "(a \<le> -a) = (a \<le> (0::'a::ordered_ring))"
  1484 proof 
  1485   assume ale: "a \<le> -a"
  1486   show "a\<le>0"
  1487     apply (rule classical) 
  1488     apply (simp add: linorder_not_le) 
  1489     apply (blast intro: ale order_trans order_less_imp_le
  1490                         neg_0_le_iff_le [THEN iffD1]) 
  1491     done
  1492 next
  1493   assume "a\<le>0"
  1494   hence "0 \<le> -a" by (simp only: neg_0_le_iff_le)
  1495   thus "a \<le> -a"  by (blast intro: prems order_trans) 
  1496 qed
  1497 
  1498 lemma minus_le_self_iff: "(-a \<le> a) = (0 \<le> (a::'a::ordered_ring))"
  1499 by (insert le_minus_self_iff [of "-a"], simp)
  1500 
  1501 lemma eq_minus_self_iff: "(a = -a) = (a = (0::'a::ordered_ring))"
  1502 by (force simp add: order_eq_iff le_minus_self_iff minus_le_self_iff)
  1503 
  1504 lemma less_minus_self_iff: "(a < -a) = (a < (0::'a::ordered_ring))"
  1505 by (simp add: order_less_le le_minus_self_iff eq_minus_self_iff)
  1506 
  1507 lemma abs_le_D1: "abs a \<le> b ==> a \<le> (b::'a::ordered_ring)"
  1508 apply (simp add: abs_if split: split_if_asm)
  1509 apply (rule order_trans [of _ "-a"]) 
  1510  apply (simp add: less_minus_self_iff order_less_imp_le, assumption)
  1511 done
  1512 
  1513 lemma abs_le_D2: "abs a \<le> b ==> -a \<le> (b::'a::ordered_ring)"
  1514 by (insert abs_le_D1 [of "-a"], simp)
  1515 
  1516 lemma abs_le_iff: "(abs a \<le> b) = (a \<le> b & -a \<le> (b::'a::ordered_ring))"
  1517 by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2)
  1518 
  1519 lemma abs_less_iff: "(abs a < b) = (a < b & -a < (b::'a::ordered_ring))" 
  1520 apply (simp add: order_less_le abs_le_iff)  
  1521 apply (auto simp add: abs_if minus_le_self_iff eq_minus_self_iff) 
  1522  apply (simp add:  linorder_not_less [symmetric]) 
  1523 apply (simp add: le_minus_self_iff linorder_neq_iff) 
  1524 apply (simp add:  linorder_not_less [symmetric]) 
  1525 done
  1526 
  1527 lemma abs_triangle_ineq: "abs (a+b) \<le> abs a + abs (b::'a::ordered_ring)"
  1528 by (force simp add: abs_le_iff abs_ge_self abs_ge_minus_self add_mono)
  1529 
  1530 lemma abs_mult_less:
  1531      "[| abs a < c; abs b < d |] ==> abs a * abs b < c*(d::'a::ordered_ring)"
  1532 proof -
  1533   assume ac: "abs a < c"
  1534   hence cpos: "0<c" by (blast intro: order_le_less_trans abs_ge_zero)
  1535   assume "abs b < d"
  1536   thus ?thesis by (simp add: ac cpos mult_strict_mono) 
  1537 qed
  1538 
  1539 ML
  1540 {*
  1541 val add_assoc = thm"add_assoc";
  1542 val add_commute = thm"add_commute";
  1543 val mult_assoc = thm"mult_assoc";
  1544 val mult_commute = thm"mult_commute";
  1545 val zero_neq_one = thm"zero_neq_one";
  1546 val diff_minus = thm"diff_minus";
  1547 val abs_if = thm"abs_if";
  1548 val divide_inverse = thm"divide_inverse";
  1549 val inverse_zero = thm"inverse_zero";
  1550 val divide_zero = thm"divide_zero";
  1551 val add_0 = thm"add_0";
  1552 val add_0_right = thm"add_0_right";
  1553 val add_left_commute = thm"add_left_commute";
  1554 val left_minus = thm"left_minus";
  1555 val right_minus = thm"right_minus";
  1556 val right_minus_eq = thm"right_minus_eq";
  1557 val add_left_cancel = thm"add_left_cancel";
  1558 val add_right_cancel = thm"add_right_cancel";
  1559 val minus_minus = thm"minus_minus";
  1560 val equals_zero_I = thm"equals_zero_I";
  1561 val minus_zero = thm"minus_zero";
  1562 val diff_self = thm"diff_self";
  1563 val diff_0 = thm"diff_0";
  1564 val diff_0_right = thm"diff_0_right";
  1565 val diff_minus_eq_add = thm"diff_minus_eq_add";
  1566 val neg_equal_iff_equal = thm"neg_equal_iff_equal";
  1567 val neg_equal_0_iff_equal = thm"neg_equal_0_iff_equal";
  1568 val neg_0_equal_iff_equal = thm"neg_0_equal_iff_equal";
  1569 val equation_minus_iff = thm"equation_minus_iff";
  1570 val minus_equation_iff = thm"minus_equation_iff";
  1571 val mult_1 = thm"mult_1";
  1572 val mult_1_right = thm"mult_1_right";
  1573 val mult_left_commute = thm"mult_left_commute";
  1574 val mult_left_zero = thm"mult_left_zero";
  1575 val mult_right_zero = thm"mult_right_zero";
  1576 val left_distrib = thm "left_distrib";
  1577 val right_distrib = thm"right_distrib";
  1578 val combine_common_factor = thm"combine_common_factor";
  1579 val minus_add_distrib = thm"minus_add_distrib";
  1580 val minus_mult_left = thm"minus_mult_left";
  1581 val minus_mult_right = thm"minus_mult_right";
  1582 val minus_mult_minus = thm"minus_mult_minus";
  1583 val right_diff_distrib = thm"right_diff_distrib";
  1584 val left_diff_distrib = thm"left_diff_distrib";
  1585 val minus_diff_eq = thm"minus_diff_eq";
  1586 val add_left_mono = thm"add_left_mono";
  1587 val add_right_mono = thm"add_right_mono";
  1588 val add_mono = thm"add_mono";
  1589 val add_strict_left_mono = thm"add_strict_left_mono";
  1590 val add_strict_right_mono = thm"add_strict_right_mono";
  1591 val add_strict_mono = thm"add_strict_mono";
  1592 val add_less_le_mono = thm"add_less_le_mono";
  1593 val add_le_less_mono = thm"add_le_less_mono";
  1594 val add_less_imp_less_left = thm"add_less_imp_less_left";
  1595 val add_less_imp_less_right = thm"add_less_imp_less_right";
  1596 val add_less_cancel_left = thm"add_less_cancel_left";
  1597 val add_less_cancel_right = thm"add_less_cancel_right";
  1598 val add_le_cancel_left = thm"add_le_cancel_left";
  1599 val add_le_cancel_right = thm"add_le_cancel_right";
  1600 val add_le_imp_le_left = thm"add_le_imp_le_left";
  1601 val add_le_imp_le_right = thm"add_le_imp_le_right";
  1602 val le_imp_neg_le = thm"le_imp_neg_le";
  1603 val neg_le_iff_le = thm"neg_le_iff_le";
  1604 val neg_le_0_iff_le = thm"neg_le_0_iff_le";
  1605 val neg_0_le_iff_le = thm"neg_0_le_iff_le";
  1606 val neg_less_iff_less = thm"neg_less_iff_less";
  1607 val neg_less_0_iff_less = thm"neg_less_0_iff_less";
  1608 val neg_0_less_iff_less = thm"neg_0_less_iff_less";
  1609 val less_minus_iff = thm"less_minus_iff";
  1610 val minus_less_iff = thm"minus_less_iff";
  1611 val le_minus_iff = thm"le_minus_iff";
  1612 val minus_le_iff = thm"minus_le_iff";
  1613 val add_diff_eq = thm"add_diff_eq";
  1614 val diff_add_eq = thm"diff_add_eq";
  1615 val diff_eq_eq = thm"diff_eq_eq";
  1616 val eq_diff_eq = thm"eq_diff_eq";
  1617 val diff_diff_eq = thm"diff_diff_eq";
  1618 val diff_diff_eq2 = thm"diff_diff_eq2";
  1619 val less_iff_diff_less_0 = thm"less_iff_diff_less_0";
  1620 val diff_less_eq = thm"diff_less_eq";
  1621 val less_diff_eq = thm"less_diff_eq";
  1622 val diff_le_eq = thm"diff_le_eq";
  1623 val le_diff_eq = thm"le_diff_eq";
  1624 val eq_iff_diff_eq_0 = thm"eq_iff_diff_eq_0";
  1625 val le_iff_diff_le_0 = thm"le_iff_diff_le_0";
  1626 val eq_add_iff1 = thm"eq_add_iff1";
  1627 val eq_add_iff2 = thm"eq_add_iff2";
  1628 val less_add_iff1 = thm"less_add_iff1";
  1629 val less_add_iff2 = thm"less_add_iff2";
  1630 val le_add_iff1 = thm"le_add_iff1";
  1631 val le_add_iff2 = thm"le_add_iff2";
  1632 val mult_strict_left_mono = thm"mult_strict_left_mono";
  1633 val mult_strict_right_mono = thm"mult_strict_right_mono";
  1634 val mult_left_mono = thm"mult_left_mono";
  1635 val mult_right_mono = thm"mult_right_mono";
  1636 val mult_left_le_imp_le = thm"mult_left_le_imp_le";
  1637 val mult_right_le_imp_le = thm"mult_right_le_imp_le";
  1638 val mult_left_less_imp_less = thm"mult_left_less_imp_less";
  1639 val mult_right_less_imp_less = thm"mult_right_less_imp_less";
  1640 val mult_strict_left_mono_neg = thm"mult_strict_left_mono_neg";
  1641 val mult_strict_right_mono_neg = thm"mult_strict_right_mono_neg";
  1642 val mult_pos = thm"mult_pos";
  1643 val mult_pos_neg = thm"mult_pos_neg";
  1644 val mult_neg = thm"mult_neg";
  1645 val zero_less_mult_pos = thm"zero_less_mult_pos";
  1646 val zero_less_mult_iff = thm"zero_less_mult_iff";
  1647 val mult_eq_0_iff = thm"mult_eq_0_iff";
  1648 val zero_le_mult_iff = thm"zero_le_mult_iff";
  1649 val mult_less_0_iff = thm"mult_less_0_iff";
  1650 val mult_le_0_iff = thm"mult_le_0_iff";
  1651 val zero_le_square = thm"zero_le_square";
  1652 val zero_less_one = thm"zero_less_one";
  1653 val zero_le_one = thm"zero_le_one";
  1654 val mult_left_mono_neg = thm"mult_left_mono_neg";
  1655 val mult_right_mono_neg = thm"mult_right_mono_neg";
  1656 val mult_strict_mono = thm"mult_strict_mono";
  1657 val mult_strict_mono' = thm"mult_strict_mono'";
  1658 val mult_mono = thm"mult_mono";
  1659 val mult_less_cancel_right = thm"mult_less_cancel_right";
  1660 val mult_less_cancel_left = thm"mult_less_cancel_left";
  1661 val mult_le_cancel_right = thm"mult_le_cancel_right";
  1662 val mult_le_cancel_left = thm"mult_le_cancel_left";
  1663 val mult_less_imp_less_left = thm"mult_less_imp_less_left";
  1664 val mult_less_imp_less_right = thm"mult_less_imp_less_right";
  1665 val mult_cancel_right = thm"mult_cancel_right";
  1666 val mult_cancel_left = thm"mult_cancel_left";
  1667 val left_inverse = thm "left_inverse";
  1668 val right_inverse = thm"right_inverse";
  1669 val right_inverse_eq = thm"right_inverse_eq";
  1670 val nonzero_inverse_eq_divide = thm"nonzero_inverse_eq_divide";
  1671 val divide_self = thm"divide_self";
  1672 val divide_inverse_zero = thm"divide_inverse_zero";
  1673 val divide_zero_left = thm"divide_zero_left";
  1674 val inverse_eq_divide = thm"inverse_eq_divide";
  1675 val nonzero_add_divide_distrib = thm"nonzero_add_divide_distrib";
  1676 val add_divide_distrib = thm"add_divide_distrib";
  1677 val field_mult_eq_0_iff = thm"field_mult_eq_0_iff";
  1678 val field_mult_cancel_right = thm"field_mult_cancel_right";
  1679 val field_mult_cancel_left = thm"field_mult_cancel_left";
  1680 val nonzero_imp_inverse_nonzero = thm"nonzero_imp_inverse_nonzero";
  1681 val inverse_zero_imp_zero = thm"inverse_zero_imp_zero";
  1682 val inverse_nonzero_imp_nonzero = thm"inverse_nonzero_imp_nonzero";
  1683 val inverse_nonzero_iff_nonzero = thm"inverse_nonzero_iff_nonzero";
  1684 val nonzero_inverse_minus_eq = thm"nonzero_inverse_minus_eq";
  1685 val inverse_minus_eq = thm"inverse_minus_eq";
  1686 val nonzero_inverse_eq_imp_eq = thm"nonzero_inverse_eq_imp_eq";
  1687 val inverse_eq_imp_eq = thm"inverse_eq_imp_eq";
  1688 val inverse_eq_iff_eq = thm"inverse_eq_iff_eq";
  1689 val nonzero_inverse_inverse_eq = thm"nonzero_inverse_inverse_eq";
  1690 val inverse_inverse_eq = thm"inverse_inverse_eq";
  1691 val inverse_1 = thm"inverse_1";
  1692 val nonzero_inverse_mult_distrib = thm"nonzero_inverse_mult_distrib";
  1693 val inverse_mult_distrib = thm"inverse_mult_distrib";
  1694 val inverse_add = thm"inverse_add";
  1695 val nonzero_mult_divide_cancel_left = thm"nonzero_mult_divide_cancel_left";
  1696 val mult_divide_cancel_left = thm"mult_divide_cancel_left";
  1697 val nonzero_mult_divide_cancel_right = thm"nonzero_mult_divide_cancel_right";
  1698 val mult_divide_cancel_right = thm"mult_divide_cancel_right";
  1699 val mult_divide_cancel_eq_if = thm"mult_divide_cancel_eq_if";
  1700 val divide_1 = thm"divide_1";
  1701 val times_divide_eq_right = thm"times_divide_eq_right";
  1702 val times_divide_eq_left = thm"times_divide_eq_left";
  1703 val divide_divide_eq_right = thm"divide_divide_eq_right";
  1704 val divide_divide_eq_left = thm"divide_divide_eq_left";
  1705 val nonzero_minus_divide_left = thm"nonzero_minus_divide_left";
  1706 val nonzero_minus_divide_right = thm"nonzero_minus_divide_right";
  1707 val nonzero_minus_divide_divide = thm"nonzero_minus_divide_divide";
  1708 val minus_divide_left = thm"minus_divide_left";
  1709 val minus_divide_right = thm"minus_divide_right";
  1710 val minus_divide_divide = thm"minus_divide_divide";
  1711 val positive_imp_inverse_positive = thm"positive_imp_inverse_positive";
  1712 val negative_imp_inverse_negative = thm"negative_imp_inverse_negative";
  1713 val inverse_le_imp_le = thm"inverse_le_imp_le";
  1714 val inverse_positive_imp_positive = thm"inverse_positive_imp_positive";
  1715 val inverse_positive_iff_positive = thm"inverse_positive_iff_positive";
  1716 val inverse_negative_imp_negative = thm"inverse_negative_imp_negative";
  1717 val inverse_negative_iff_negative = thm"inverse_negative_iff_negative";
  1718 val inverse_nonnegative_iff_nonnegative = thm"inverse_nonnegative_iff_nonnegative";
  1719 val inverse_nonpositive_iff_nonpositive = thm"inverse_nonpositive_iff_nonpositive";
  1720 val less_imp_inverse_less = thm"less_imp_inverse_less";
  1721 val inverse_less_imp_less = thm"inverse_less_imp_less";
  1722 val inverse_less_iff_less = thm"inverse_less_iff_less";
  1723 val le_imp_inverse_le = thm"le_imp_inverse_le";
  1724 val inverse_le_iff_le = thm"inverse_le_iff_le";
  1725 val inverse_le_imp_le_neg = thm"inverse_le_imp_le_neg";
  1726 val less_imp_inverse_less_neg = thm"less_imp_inverse_less_neg";
  1727 val inverse_less_imp_less_neg = thm"inverse_less_imp_less_neg";
  1728 val inverse_less_iff_less_neg = thm"inverse_less_iff_less_neg";
  1729 val le_imp_inverse_le_neg = thm"le_imp_inverse_le_neg";
  1730 val inverse_le_iff_le_neg = thm"inverse_le_iff_le_neg";
  1731 val zero_less_divide_iff = thm"zero_less_divide_iff";
  1732 val divide_less_0_iff = thm"divide_less_0_iff";
  1733 val zero_le_divide_iff = thm"zero_le_divide_iff";
  1734 val divide_le_0_iff = thm"divide_le_0_iff";
  1735 val divide_eq_0_iff = thm"divide_eq_0_iff";
  1736 val pos_le_divide_eq = thm"pos_le_divide_eq";
  1737 val neg_le_divide_eq = thm"neg_le_divide_eq";
  1738 val le_divide_eq = thm"le_divide_eq";
  1739 val pos_divide_le_eq = thm"pos_divide_le_eq";
  1740 val neg_divide_le_eq = thm"neg_divide_le_eq";
  1741 val divide_le_eq = thm"divide_le_eq";
  1742 val pos_less_divide_eq = thm"pos_less_divide_eq";
  1743 val neg_less_divide_eq = thm"neg_less_divide_eq";
  1744 val less_divide_eq = thm"less_divide_eq";
  1745 val pos_divide_less_eq = thm"pos_divide_less_eq";
  1746 val neg_divide_less_eq = thm"neg_divide_less_eq";
  1747 val divide_less_eq = thm"divide_less_eq";
  1748 val nonzero_eq_divide_eq = thm"nonzero_eq_divide_eq";
  1749 val eq_divide_eq = thm"eq_divide_eq";
  1750 val nonzero_divide_eq_eq = thm"nonzero_divide_eq_eq";
  1751 val divide_eq_eq = thm"divide_eq_eq";
  1752 val divide_cancel_right = thm"divide_cancel_right";
  1753 val divide_cancel_left = thm"divide_cancel_left";
  1754 val divide_strict_right_mono = thm"divide_strict_right_mono";
  1755 val divide_right_mono = thm"divide_right_mono";
  1756 val divide_strict_left_mono = thm"divide_strict_left_mono";
  1757 val divide_left_mono = thm"divide_left_mono";
  1758 val divide_strict_left_mono_neg = thm"divide_strict_left_mono_neg";
  1759 val divide_strict_right_mono_neg = thm"divide_strict_right_mono_neg";
  1760 val zero_less_two = thm"zero_less_two";
  1761 val less_half_sum = thm"less_half_sum";
  1762 val gt_half_sum = thm"gt_half_sum";
  1763 val dense = thm"dense";
  1764 val abs_zero = thm"abs_zero";
  1765 val abs_one = thm"abs_one";
  1766 val abs_mult = thm"abs_mult";
  1767 val abs_mult_self = thm"abs_mult_self";
  1768 val abs_eq_0 = thm"abs_eq_0";
  1769 val zero_less_abs_iff = thm"zero_less_abs_iff";
  1770 val abs_not_less_zero = thm"abs_not_less_zero";
  1771 val abs_le_zero_iff = thm"abs_le_zero_iff";
  1772 val abs_minus_cancel = thm"abs_minus_cancel";
  1773 val abs_ge_zero = thm"abs_ge_zero";
  1774 val abs_idempotent = thm"abs_idempotent";
  1775 val abs_zero_iff = thm"abs_zero_iff";
  1776 val abs_ge_self = thm"abs_ge_self";
  1777 val abs_ge_minus_self = thm"abs_ge_minus_self";
  1778 val nonzero_abs_inverse = thm"nonzero_abs_inverse";
  1779 val abs_inverse = thm"abs_inverse";
  1780 val nonzero_abs_divide = thm"nonzero_abs_divide";
  1781 val abs_divide = thm"abs_divide";
  1782 val abs_leI = thm"abs_leI";
  1783 val le_minus_self_iff = thm"le_minus_self_iff";
  1784 val minus_le_self_iff = thm"minus_le_self_iff";
  1785 val eq_minus_self_iff = thm"eq_minus_self_iff";
  1786 val less_minus_self_iff = thm"less_minus_self_iff";
  1787 val abs_le_D1 = thm"abs_le_D1";
  1788 val abs_le_D2 = thm"abs_le_D2";
  1789 val abs_le_iff = thm"abs_le_iff";
  1790 val abs_less_iff = thm"abs_less_iff";
  1791 val abs_triangle_ineq = thm"abs_triangle_ineq";
  1792 val abs_mult_less = thm"abs_mult_less";
  1793 
  1794 val compare_rls = thms"compare_rls";
  1795 *}
  1796 
  1797 
  1798 end