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