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
```