src/HOL/Ring_and_Field.thy
 author nipkow Fri Mar 06 17:38:47 2009 +0100 (2009-03-06) changeset 30313 b2441b0c8d38 parent 30242 aea5d7fa7ef5 child 30630 4fbe1401bac2 child 30649 57753e0ec1d4 permissions -rw-r--r--
     1 (*  Title:   HOL/Ring_and_Field.thy

     2     Author:  Gertrud Bauer, Steven Obua, Tobias Nipkow, Lawrence C Paulson, and Markus Wenzel,

     3              with contributions by Jeremy Avigad

     4 *)

     5

     6 header {* (Ordered) Rings and Fields *}

     7

     8 theory Ring_and_Field

     9 imports OrderedGroup

    10 begin

    11

    12 text {*

    13   The theory of partially ordered rings is taken from the books:

    14   \begin{itemize}

    15   \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979

    16   \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963

    17   \end{itemize}

    18   Most of the used notions can also be looked up in

    19   \begin{itemize}

    20   \item \url{http://www.mathworld.com} by Eric Weisstein et. al.

    21   \item \emph{Algebra I} by van der Waerden, Springer.

    22   \end{itemize}

    23 *}

    24

    25 class semiring = ab_semigroup_add + semigroup_mult +

    26   assumes left_distrib[algebra_simps]: "(a + b) * c = a * c + b * c"

    27   assumes right_distrib[algebra_simps]: "a * (b + c) = a * b + a * c"

    28 begin

    29

    30 text{*For the @{text combine_numerals} simproc*}

    31 lemma combine_common_factor:

    32   "a * e + (b * e + c) = (a + b) * e + c"

    33 by (simp add: left_distrib add_ac)

    34

    35 end

    36

    37 class mult_zero = times + zero +

    38   assumes mult_zero_left [simp]: "0 * a = 0"

    39   assumes mult_zero_right [simp]: "a * 0 = 0"

    40

    41 class semiring_0 = semiring + comm_monoid_add + mult_zero

    42

    43 class semiring_0_cancel = semiring + cancel_comm_monoid_add

    44 begin

    45

    46 subclass semiring_0

    47 proof

    48   fix a :: 'a

    49   have "0 * a + 0 * a = 0 * a + 0" by (simp add: left_distrib [symmetric])

    50   thus "0 * a = 0" by (simp only: add_left_cancel)

    51 next

    52   fix a :: 'a

    53   have "a * 0 + a * 0 = a * 0 + 0" by (simp add: right_distrib [symmetric])

    54   thus "a * 0 = 0" by (simp only: add_left_cancel)

    55 qed

    56

    57 end

    58

    59 class comm_semiring = ab_semigroup_add + ab_semigroup_mult +

    60   assumes distrib: "(a + b) * c = a * c + b * c"

    61 begin

    62

    63 subclass semiring

    64 proof

    65   fix a b c :: 'a

    66   show "(a + b) * c = a * c + b * c" by (simp add: distrib)

    67   have "a * (b + c) = (b + c) * a" by (simp add: mult_ac)

    68   also have "... = b * a + c * a" by (simp only: distrib)

    69   also have "... = a * b + a * c" by (simp add: mult_ac)

    70   finally show "a * (b + c) = a * b + a * c" by blast

    71 qed

    72

    73 end

    74

    75 class comm_semiring_0 = comm_semiring + comm_monoid_add + mult_zero

    76 begin

    77

    78 subclass semiring_0 ..

    79

    80 end

    81

    82 class comm_semiring_0_cancel = comm_semiring + cancel_comm_monoid_add

    83 begin

    84

    85 subclass semiring_0_cancel ..

    86

    87 subclass comm_semiring_0 ..

    88

    89 end

    90

    91 class zero_neq_one = zero + one +

    92   assumes zero_neq_one [simp]: "0 \<noteq> 1"

    93 begin

    94

    95 lemma one_neq_zero [simp]: "1 \<noteq> 0"

    96 by (rule not_sym) (rule zero_neq_one)

    97

    98 end

    99

   100 class semiring_1 = zero_neq_one + semiring_0 + monoid_mult

   101

   102 text {* Abstract divisibility *}

   103

   104 class dvd = times

   105 begin

   106

   107 definition dvd :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "dvd" 50) where

   108   [code del]: "b dvd a \<longleftrightarrow> (\<exists>k. a = b * k)"

   109

   110 lemma dvdI [intro?]: "a = b * k \<Longrightarrow> b dvd a"

   111   unfolding dvd_def ..

   112

   113 lemma dvdE [elim?]: "b dvd a \<Longrightarrow> (\<And>k. a = b * k \<Longrightarrow> P) \<Longrightarrow> P"

   114   unfolding dvd_def by blast

   115

   116 end

   117

   118 class comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult + dvd

   119   (*previously almost_semiring*)

   120 begin

   121

   122 subclass semiring_1 ..

   123

   124 lemma dvd_refl[simp]: "a dvd a"

   125 proof

   126   show "a = a * 1" by simp

   127 qed

   128

   129 lemma dvd_trans:

   130   assumes "a dvd b" and "b dvd c"

   131   shows "a dvd c"

   132 proof -

   133   from assms obtain v where "b = a * v" by (auto elim!: dvdE)

   134   moreover from assms obtain w where "c = b * w" by (auto elim!: dvdE)

   135   ultimately have "c = a * (v * w)" by (simp add: mult_assoc)

   136   then show ?thesis ..

   137 qed

   138

   139 lemma dvd_0_left_iff [noatp, simp]: "0 dvd a \<longleftrightarrow> a = 0"

   140 by (auto intro: dvd_refl elim!: dvdE)

   141

   142 lemma dvd_0_right [iff]: "a dvd 0"

   143 proof

   144   show "0 = a * 0" by simp

   145 qed

   146

   147 lemma one_dvd [simp]: "1 dvd a"

   148 by (auto intro!: dvdI)

   149

   150 lemma dvd_mult[simp]: "a dvd c \<Longrightarrow> a dvd (b * c)"

   151 by (auto intro!: mult_left_commute dvdI elim!: dvdE)

   152

   153 lemma dvd_mult2[simp]: "a dvd b \<Longrightarrow> a dvd (b * c)"

   154   apply (subst mult_commute)

   155   apply (erule dvd_mult)

   156   done

   157

   158 lemma dvd_triv_right [simp]: "a dvd b * a"

   159 by (rule dvd_mult) (rule dvd_refl)

   160

   161 lemma dvd_triv_left [simp]: "a dvd a * b"

   162 by (rule dvd_mult2) (rule dvd_refl)

   163

   164 lemma mult_dvd_mono:

   165   assumes "a dvd b"

   166     and "c dvd d"

   167   shows "a * c dvd b * d"

   168 proof -

   169   from a dvd b obtain b' where "b = a * b'" ..

   170   moreover from c dvd d obtain d' where "d = c * d'" ..

   171   ultimately have "b * d = (a * c) * (b' * d')" by (simp add: mult_ac)

   172   then show ?thesis ..

   173 qed

   174

   175 lemma dvd_mult_left: "a * b dvd c \<Longrightarrow> a dvd c"

   176 by (simp add: dvd_def mult_assoc, blast)

   177

   178 lemma dvd_mult_right: "a * b dvd c \<Longrightarrow> b dvd c"

   179   unfolding mult_ac [of a] by (rule dvd_mult_left)

   180

   181 lemma dvd_0_left: "0 dvd a \<Longrightarrow> a = 0"

   182 by simp

   183

   184 lemma dvd_add[simp]:

   185   assumes "a dvd b" and "a dvd c" shows "a dvd (b + c)"

   186 proof -

   187   from a dvd b obtain b' where "b = a * b'" ..

   188   moreover from a dvd c obtain c' where "c = a * c'" ..

   189   ultimately have "b + c = a * (b' + c')" by (simp add: right_distrib)

   190   then show ?thesis ..

   191 qed

   192

   193 end

   194

   195

   196 class no_zero_divisors = zero + times +

   197   assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"

   198

   199 class semiring_1_cancel = semiring + cancel_comm_monoid_add

   200   + zero_neq_one + monoid_mult

   201 begin

   202

   203 subclass semiring_0_cancel ..

   204

   205 subclass semiring_1 ..

   206

   207 end

   208

   209 class comm_semiring_1_cancel = comm_semiring + cancel_comm_monoid_add

   210   + zero_neq_one + comm_monoid_mult

   211 begin

   212

   213 subclass semiring_1_cancel ..

   214 subclass comm_semiring_0_cancel ..

   215 subclass comm_semiring_1 ..

   216

   217 end

   218

   219 class ring = semiring + ab_group_add

   220 begin

   221

   222 subclass semiring_0_cancel ..

   223

   224 text {* Distribution rules *}

   225

   226 lemma minus_mult_left: "- (a * b) = - a * b"

   227 by (rule equals_zero_I) (simp add: left_distrib [symmetric])

   228

   229 lemma minus_mult_right: "- (a * b) = a * - b"

   230 by (rule equals_zero_I) (simp add: right_distrib [symmetric])

   231

   232 text{*Extract signs from products*}

   233 lemmas mult_minus_left [simp, noatp] = minus_mult_left [symmetric]

   234 lemmas mult_minus_right [simp,noatp] = minus_mult_right [symmetric]

   235

   236 lemma minus_mult_minus [simp]: "- a * - b = a * b"

   237 by simp

   238

   239 lemma minus_mult_commute: "- a * b = a * - b"

   240 by simp

   241

   242 lemma right_diff_distrib[algebra_simps]: "a * (b - c) = a * b - a * c"

   243 by (simp add: right_distrib diff_minus)

   244

   245 lemma left_diff_distrib[algebra_simps]: "(a - b) * c = a * c - b * c"

   246 by (simp add: left_distrib diff_minus)

   247

   248 lemmas ring_distribs[noatp] =

   249   right_distrib left_distrib left_diff_distrib right_diff_distrib

   250

   251 text{*Legacy - use @{text algebra_simps} *}

   252 lemmas ring_simps[noatp] = algebra_simps

   253

   254 lemma eq_add_iff1:

   255   "a * e + c = b * e + d \<longleftrightarrow> (a - b) * e + c = d"

   256 by (simp add: algebra_simps)

   257

   258 lemma eq_add_iff2:

   259   "a * e + c = b * e + d \<longleftrightarrow> c = (b - a) * e + d"

   260 by (simp add: algebra_simps)

   261

   262 end

   263

   264 lemmas ring_distribs[noatp] =

   265   right_distrib left_distrib left_diff_distrib right_diff_distrib

   266

   267 class comm_ring = comm_semiring + ab_group_add

   268 begin

   269

   270 subclass ring ..

   271 subclass comm_semiring_0_cancel ..

   272

   273 end

   274

   275 class ring_1 = ring + zero_neq_one + monoid_mult

   276 begin

   277

   278 subclass semiring_1_cancel ..

   279

   280 end

   281

   282 class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult

   283   (*previously ring*)

   284 begin

   285

   286 subclass ring_1 ..

   287 subclass comm_semiring_1_cancel ..

   288

   289 lemma dvd_minus_iff [simp]: "x dvd - y \<longleftrightarrow> x dvd y"

   290 proof

   291   assume "x dvd - y"

   292   then have "x dvd - 1 * - y" by (rule dvd_mult)

   293   then show "x dvd y" by simp

   294 next

   295   assume "x dvd y"

   296   then have "x dvd - 1 * y" by (rule dvd_mult)

   297   then show "x dvd - y" by simp

   298 qed

   299

   300 lemma minus_dvd_iff [simp]: "- x dvd y \<longleftrightarrow> x dvd y"

   301 proof

   302   assume "- x dvd y"

   303   then obtain k where "y = - x * k" ..

   304   then have "y = x * - k" by simp

   305   then show "x dvd y" ..

   306 next

   307   assume "x dvd y"

   308   then obtain k where "y = x * k" ..

   309   then have "y = - x * - k" by simp

   310   then show "- x dvd y" ..

   311 qed

   312

   313 lemma dvd_diff[simp]: "x dvd y \<Longrightarrow> x dvd z \<Longrightarrow> x dvd (y - z)"

   314 by (simp add: diff_minus dvd_minus_iff)

   315

   316 end

   317

   318 class ring_no_zero_divisors = ring + no_zero_divisors

   319 begin

   320

   321 lemma mult_eq_0_iff [simp]:

   322   shows "a * b = 0 \<longleftrightarrow> (a = 0 \<or> b = 0)"

   323 proof (cases "a = 0 \<or> b = 0")

   324   case False then have "a \<noteq> 0" and "b \<noteq> 0" by auto

   325     then show ?thesis using no_zero_divisors by simp

   326 next

   327   case True then show ?thesis by auto

   328 qed

   329

   330 text{*Cancellation of equalities with a common factor*}

   331 lemma mult_cancel_right [simp, noatp]:

   332   "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b"

   333 proof -

   334   have "(a * c = b * c) = ((a - b) * c = 0)"

   335     by (simp add: algebra_simps right_minus_eq)

   336   thus ?thesis by (simp add: disj_commute right_minus_eq)

   337 qed

   338

   339 lemma mult_cancel_left [simp, noatp]:

   340   "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b"

   341 proof -

   342   have "(c * a = c * b) = (c * (a - b) = 0)"

   343     by (simp add: algebra_simps right_minus_eq)

   344   thus ?thesis by (simp add: right_minus_eq)

   345 qed

   346

   347 end

   348

   349 class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors

   350 begin

   351

   352 lemma mult_cancel_right1 [simp]:

   353   "c = b * c \<longleftrightarrow> c = 0 \<or> b = 1"

   354 by (insert mult_cancel_right [of 1 c b], force)

   355

   356 lemma mult_cancel_right2 [simp]:

   357   "a * c = c \<longleftrightarrow> c = 0 \<or> a = 1"

   358 by (insert mult_cancel_right [of a c 1], simp)

   359

   360 lemma mult_cancel_left1 [simp]:

   361   "c = c * b \<longleftrightarrow> c = 0 \<or> b = 1"

   362 by (insert mult_cancel_left [of c 1 b], force)

   363

   364 lemma mult_cancel_left2 [simp]:

   365   "c * a = c \<longleftrightarrow> c = 0 \<or> a = 1"

   366 by (insert mult_cancel_left [of c a 1], simp)

   367

   368 end

   369

   370 class idom = comm_ring_1 + no_zero_divisors

   371 begin

   372

   373 subclass ring_1_no_zero_divisors ..

   374

   375 lemma square_eq_iff: "a * a = b * b \<longleftrightarrow> (a = b \<or> a = - b)"

   376 proof

   377   assume "a * a = b * b"

   378   then have "(a - b) * (a + b) = 0"

   379     by (simp add: algebra_simps)

   380   then show "a = b \<or> a = - b"

   381     by (simp add: right_minus_eq eq_neg_iff_add_eq_0)

   382 next

   383   assume "a = b \<or> a = - b"

   384   then show "a * a = b * b" by auto

   385 qed

   386

   387 lemma dvd_mult_cancel_right [simp]:

   388   "a * c dvd b * c \<longleftrightarrow> c = 0 \<or> a dvd b"

   389 proof -

   390   have "a * c dvd b * c \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)"

   391     unfolding dvd_def by (simp add: mult_ac)

   392   also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b"

   393     unfolding dvd_def by simp

   394   finally show ?thesis .

   395 qed

   396

   397 lemma dvd_mult_cancel_left [simp]:

   398   "c * a dvd c * b \<longleftrightarrow> c = 0 \<or> a dvd b"

   399 proof -

   400   have "c * a dvd c * b \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)"

   401     unfolding dvd_def by (simp add: mult_ac)

   402   also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b"

   403     unfolding dvd_def by simp

   404   finally show ?thesis .

   405 qed

   406

   407 end

   408

   409 class division_ring = ring_1 + inverse +

   410   assumes left_inverse [simp]:  "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"

   411   assumes right_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> a * inverse a = 1"

   412 begin

   413

   414 subclass ring_1_no_zero_divisors

   415 proof

   416   fix a b :: 'a

   417   assume a: "a \<noteq> 0" and b: "b \<noteq> 0"

   418   show "a * b \<noteq> 0"

   419   proof

   420     assume ab: "a * b = 0"

   421     hence "0 = inverse a * (a * b) * inverse b" by simp

   422     also have "\<dots> = (inverse a * a) * (b * inverse b)"

   423       by (simp only: mult_assoc)

   424     also have "\<dots> = 1" using a b by simp

   425     finally show False by simp

   426   qed

   427 qed

   428

   429 lemma nonzero_imp_inverse_nonzero:

   430   "a \<noteq> 0 \<Longrightarrow> inverse a \<noteq> 0"

   431 proof

   432   assume ianz: "inverse a = 0"

   433   assume "a \<noteq> 0"

   434   hence "1 = a * inverse a" by simp

   435   also have "... = 0" by (simp add: ianz)

   436   finally have "1 = 0" .

   437   thus False by (simp add: eq_commute)

   438 qed

   439

   440 lemma inverse_zero_imp_zero:

   441   "inverse a = 0 \<Longrightarrow> a = 0"

   442 apply (rule classical)

   443 apply (drule nonzero_imp_inverse_nonzero)

   444 apply auto

   445 done

   446

   447 lemma inverse_unique:

   448   assumes ab: "a * b = 1"

   449   shows "inverse a = b"

   450 proof -

   451   have "a \<noteq> 0" using ab by (cases "a = 0") simp_all

   452   moreover have "inverse a * (a * b) = inverse a" by (simp add: ab)

   453   ultimately show ?thesis by (simp add: mult_assoc [symmetric])

   454 qed

   455

   456 lemma nonzero_inverse_minus_eq:

   457   "a \<noteq> 0 \<Longrightarrow> inverse (- a) = - inverse a"

   458 by (rule inverse_unique) simp

   459

   460 lemma nonzero_inverse_inverse_eq:

   461   "a \<noteq> 0 \<Longrightarrow> inverse (inverse a) = a"

   462 by (rule inverse_unique) simp

   463

   464 lemma nonzero_inverse_eq_imp_eq:

   465   assumes "inverse a = inverse b" and "a \<noteq> 0" and "b \<noteq> 0"

   466   shows "a = b"

   467 proof -

   468   from inverse a = inverse b

   469   have "inverse (inverse a) = inverse (inverse b)" by (rule arg_cong)

   470   with a \<noteq> 0 and b \<noteq> 0 show "a = b"

   471     by (simp add: nonzero_inverse_inverse_eq)

   472 qed

   473

   474 lemma inverse_1 [simp]: "inverse 1 = 1"

   475 by (rule inverse_unique) simp

   476

   477 lemma nonzero_inverse_mult_distrib:

   478   assumes "a \<noteq> 0" and "b \<noteq> 0"

   479   shows "inverse (a * b) = inverse b * inverse a"

   480 proof -

   481   have "a * (b * inverse b) * inverse a = 1" using assms by simp

   482   hence "a * b * (inverse b * inverse a) = 1" by (simp only: mult_assoc)

   483   thus ?thesis by (rule inverse_unique)

   484 qed

   485

   486 lemma division_ring_inverse_add:

   487   "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a + inverse b = inverse a * (a + b) * inverse b"

   488 by (simp add: algebra_simps)

   489

   490 lemma division_ring_inverse_diff:

   491   "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a - inverse b = inverse a * (b - a) * inverse b"

   492 by (simp add: algebra_simps)

   493

   494 end

   495

   496 class field = comm_ring_1 + inverse +

   497   assumes field_inverse:  "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"

   498   assumes divide_inverse: "a / b = a * inverse b"

   499 begin

   500

   501 subclass division_ring

   502 proof

   503   fix a :: 'a

   504   assume "a \<noteq> 0"

   505   thus "inverse a * a = 1" by (rule field_inverse)

   506   thus "a * inverse a = 1" by (simp only: mult_commute)

   507 qed

   508

   509 subclass idom ..

   510

   511 lemma right_inverse_eq: "b \<noteq> 0 \<Longrightarrow> a / b = 1 \<longleftrightarrow> a = b"

   512 proof

   513   assume neq: "b \<noteq> 0"

   514   {

   515     hence "a = (a / b) * b" by (simp add: divide_inverse mult_ac)

   516     also assume "a / b = 1"

   517     finally show "a = b" by simp

   518   next

   519     assume "a = b"

   520     with neq show "a / b = 1" by (simp add: divide_inverse)

   521   }

   522 qed

   523

   524 lemma nonzero_inverse_eq_divide: "a \<noteq> 0 \<Longrightarrow> inverse a = 1 / a"

   525 by (simp add: divide_inverse)

   526

   527 lemma divide_self [simp]: "a \<noteq> 0 \<Longrightarrow> a / a = 1"

   528 by (simp add: divide_inverse)

   529

   530 lemma divide_zero_left [simp]: "0 / a = 0"

   531 by (simp add: divide_inverse)

   532

   533 lemma inverse_eq_divide: "inverse a = 1 / a"

   534 by (simp add: divide_inverse)

   535

   536 lemma add_divide_distrib: "(a+b) / c = a/c + b/c"

   537 by (simp add: divide_inverse algebra_simps)

   538

   539 end

   540

   541 class division_by_zero = zero + inverse +

   542   assumes inverse_zero [simp]: "inverse 0 = 0"

   543

   544 lemma divide_zero [simp]:

   545   "a / 0 = (0::'a::{field,division_by_zero})"

   546 by (simp add: divide_inverse)

   547

   548 lemma divide_self_if [simp]:

   549   "a / (a::'a::{field,division_by_zero}) = (if a=0 then 0 else 1)"

   550 by simp

   551

   552 class mult_mono = times + zero + ord +

   553   assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"

   554   assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"

   555

   556 class pordered_semiring = mult_mono + semiring_0 + pordered_ab_semigroup_add

   557 begin

   558

   559 lemma mult_mono:

   560   "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> c

   561      \<Longrightarrow> a * c \<le> b * d"

   562 apply (erule mult_right_mono [THEN order_trans], assumption)

   563 apply (erule mult_left_mono, assumption)

   564 done

   565

   566 lemma mult_mono':

   567   "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> c

   568      \<Longrightarrow> a * c \<le> b * d"

   569 apply (rule mult_mono)

   570 apply (fast intro: order_trans)+

   571 done

   572

   573 end

   574

   575 class pordered_cancel_semiring = mult_mono + pordered_ab_semigroup_add

   576   + semiring + cancel_comm_monoid_add

   577 begin

   578

   579 subclass semiring_0_cancel ..

   580 subclass pordered_semiring ..

   581

   582 lemma mult_nonneg_nonneg: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b"

   583 by (drule mult_left_mono [of zero b], auto)

   584

   585 lemma mult_nonneg_nonpos: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> a * b \<le> 0"

   586 by (drule mult_left_mono [of b zero], auto)

   587

   588 lemma mult_nonneg_nonpos2: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> b * a \<le> 0"

   589 by (drule mult_right_mono [of b zero], auto)

   590

   591 lemma split_mult_neg_le: "(0 \<le> a & b \<le> 0) | (a \<le> 0 & 0 \<le> b) \<Longrightarrow> a * b \<le> 0"

   592 by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)

   593

   594 end

   595

   596 class ordered_semiring = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add + mult_mono

   597 begin

   598

   599 subclass pordered_cancel_semiring ..

   600

   601 subclass pordered_comm_monoid_add ..

   602

   603 lemma mult_left_less_imp_less:

   604   "c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"

   605 by (force simp add: mult_left_mono not_le [symmetric])

   606

   607 lemma mult_right_less_imp_less:

   608   "a * c < b * c \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"

   609 by (force simp add: mult_right_mono not_le [symmetric])

   610

   611 end

   612

   613 class ordered_semiring_strict = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add +

   614   assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"

   615   assumes mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c"

   616 begin

   617

   618 subclass semiring_0_cancel ..

   619

   620 subclass ordered_semiring

   621 proof

   622   fix a b c :: 'a

   623   assume A: "a \<le> b" "0 \<le> c"

   624   from A show "c * a \<le> c * b"

   625     unfolding le_less

   626     using mult_strict_left_mono by (cases "c = 0") auto

   627   from A show "a * c \<le> b * c"

   628     unfolding le_less

   629     using mult_strict_right_mono by (cases "c = 0") auto

   630 qed

   631

   632 lemma mult_left_le_imp_le:

   633   "c * a \<le> c * b \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"

   634 by (force simp add: mult_strict_left_mono _not_less [symmetric])

   635

   636 lemma mult_right_le_imp_le:

   637   "a * c \<le> b * c \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"

   638 by (force simp add: mult_strict_right_mono not_less [symmetric])

   639

   640 lemma mult_pos_pos:

   641   "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a * b"

   642 by (drule mult_strict_left_mono [of zero b], auto)

   643

   644 lemma mult_pos_neg:

   645   "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> a * b < 0"

   646 by (drule mult_strict_left_mono [of b zero], auto)

   647

   648 lemma mult_pos_neg2:

   649   "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> b * a < 0"

   650 by (drule mult_strict_right_mono [of b zero], auto)

   651

   652 lemma zero_less_mult_pos:

   653   "0 < a * b \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"

   654 apply (cases "b\<le>0")

   655  apply (auto simp add: le_less not_less)

   656 apply (drule_tac mult_pos_neg [of a b])

   657  apply (auto dest: less_not_sym)

   658 done

   659

   660 lemma zero_less_mult_pos2:

   661   "0 < b * a \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"

   662 apply (cases "b\<le>0")

   663  apply (auto simp add: le_less not_less)

   664 apply (drule_tac mult_pos_neg2 [of a b])

   665  apply (auto dest: less_not_sym)

   666 done

   667

   668 text{*Strict monotonicity in both arguments*}

   669 lemma mult_strict_mono:

   670   assumes "a < b" and "c < d" and "0 < b" and "0 \<le> c"

   671   shows "a * c < b * d"

   672   using assms apply (cases "c=0")

   673   apply (simp add: mult_pos_pos)

   674   apply (erule mult_strict_right_mono [THEN less_trans])

   675   apply (force simp add: le_less)

   676   apply (erule mult_strict_left_mono, assumption)

   677   done

   678

   679 text{*This weaker variant has more natural premises*}

   680 lemma mult_strict_mono':

   681   assumes "a < b" and "c < d" and "0 \<le> a" and "0 \<le> c"

   682   shows "a * c < b * d"

   683 by (rule mult_strict_mono) (insert assms, auto)

   684

   685 lemma mult_less_le_imp_less:

   686   assumes "a < b" and "c \<le> d" and "0 \<le> a" and "0 < c"

   687   shows "a * c < b * d"

   688   using assms apply (subgoal_tac "a * c < b * c")

   689   apply (erule less_le_trans)

   690   apply (erule mult_left_mono)

   691   apply simp

   692   apply (erule mult_strict_right_mono)

   693   apply assumption

   694   done

   695

   696 lemma mult_le_less_imp_less:

   697   assumes "a \<le> b" and "c < d" and "0 < a" and "0 \<le> c"

   698   shows "a * c < b * d"

   699   using assms apply (subgoal_tac "a * c \<le> b * c")

   700   apply (erule le_less_trans)

   701   apply (erule mult_strict_left_mono)

   702   apply simp

   703   apply (erule mult_right_mono)

   704   apply simp

   705   done

   706

   707 lemma mult_less_imp_less_left:

   708   assumes less: "c * a < c * b" and nonneg: "0 \<le> c"

   709   shows "a < b"

   710 proof (rule ccontr)

   711   assume "\<not>  a < b"

   712   hence "b \<le> a" by (simp add: linorder_not_less)

   713   hence "c * b \<le> c * a" using nonneg by (rule mult_left_mono)

   714   with this and less show False by (simp add: not_less [symmetric])

   715 qed

   716

   717 lemma mult_less_imp_less_right:

   718   assumes less: "a * c < b * c" and nonneg: "0 \<le> c"

   719   shows "a < b"

   720 proof (rule ccontr)

   721   assume "\<not> a < b"

   722   hence "b \<le> a" by (simp add: linorder_not_less)

   723   hence "b * c \<le> a * c" using nonneg by (rule mult_right_mono)

   724   with this and less show False by (simp add: not_less [symmetric])

   725 qed

   726

   727 end

   728

   729 class mult_mono1 = times + zero + ord +

   730   assumes mult_mono1: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"

   731

   732 class pordered_comm_semiring = comm_semiring_0

   733   + pordered_ab_semigroup_add + mult_mono1

   734 begin

   735

   736 subclass pordered_semiring

   737 proof

   738   fix a b c :: 'a

   739   assume "a \<le> b" "0 \<le> c"

   740   thus "c * a \<le> c * b" by (rule mult_mono1)

   741   thus "a * c \<le> b * c" by (simp only: mult_commute)

   742 qed

   743

   744 end

   745

   746 class pordered_cancel_comm_semiring = comm_semiring_0_cancel

   747   + pordered_ab_semigroup_add + mult_mono1

   748 begin

   749

   750 subclass pordered_comm_semiring ..

   751 subclass pordered_cancel_semiring ..

   752

   753 end

   754

   755 class ordered_comm_semiring_strict = comm_semiring_0 + ordered_cancel_ab_semigroup_add +

   756   assumes mult_strict_left_mono_comm: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"

   757 begin

   758

   759 subclass ordered_semiring_strict

   760 proof

   761   fix a b c :: 'a

   762   assume "a < b" "0 < c"

   763   thus "c * a < c * b" by (rule mult_strict_left_mono_comm)

   764   thus "a * c < b * c" by (simp only: mult_commute)

   765 qed

   766

   767 subclass pordered_cancel_comm_semiring

   768 proof

   769   fix a b c :: 'a

   770   assume "a \<le> b" "0 \<le> c"

   771   thus "c * a \<le> c * b"

   772     unfolding le_less

   773     using mult_strict_left_mono by (cases "c = 0") auto

   774 qed

   775

   776 end

   777

   778 class pordered_ring = ring + pordered_cancel_semiring

   779 begin

   780

   781 subclass pordered_ab_group_add ..

   782

   783 text{*Legacy - use @{text algebra_simps} *}

   784 lemmas ring_simps[noatp] = algebra_simps

   785

   786 lemma less_add_iff1:

   787   "a * e + c < b * e + d \<longleftrightarrow> (a - b) * e + c < d"

   788 by (simp add: algebra_simps)

   789

   790 lemma less_add_iff2:

   791   "a * e + c < b * e + d \<longleftrightarrow> c < (b - a) * e + d"

   792 by (simp add: algebra_simps)

   793

   794 lemma le_add_iff1:

   795   "a * e + c \<le> b * e + d \<longleftrightarrow> (a - b) * e + c \<le> d"

   796 by (simp add: algebra_simps)

   797

   798 lemma le_add_iff2:

   799   "a * e + c \<le> b * e + d \<longleftrightarrow> c \<le> (b - a) * e + d"

   800 by (simp add: algebra_simps)

   801

   802 lemma mult_left_mono_neg:

   803   "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> c * a \<le> c * b"

   804   apply (drule mult_left_mono [of _ _ "uminus c"])

   805   apply (simp_all add: minus_mult_left [symmetric])

   806   done

   807

   808 lemma mult_right_mono_neg:

   809   "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> a * c \<le> b * c"

   810   apply (drule mult_right_mono [of _ _ "uminus c"])

   811   apply (simp_all add: minus_mult_right [symmetric])

   812   done

   813

   814 lemma mult_nonpos_nonpos:

   815   "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> 0 \<le> a * b"

   816 by (drule mult_right_mono_neg [of a zero b]) auto

   817

   818 lemma split_mult_pos_le:

   819   "(0 \<le> a \<and> 0 \<le> b) \<or> (a \<le> 0 \<and> b \<le> 0) \<Longrightarrow> 0 \<le> a * b"

   820 by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)

   821

   822 end

   823

   824 class abs_if = minus + uminus + ord + zero + abs +

   825   assumes abs_if: "\<bar>a\<bar> = (if a < 0 then - a else a)"

   826

   827 class sgn_if = minus + uminus + zero + one + ord + sgn +

   828   assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"

   829

   830 lemma (in sgn_if) sgn0[simp]: "sgn 0 = 0"

   831 by(simp add:sgn_if)

   832

   833 class ordered_ring = ring + ordered_semiring

   834   + ordered_ab_group_add + abs_if

   835 begin

   836

   837 subclass pordered_ring ..

   838

   839 subclass pordered_ab_group_add_abs

   840 proof

   841   fix a b

   842   show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"

   843 by (auto simp add: abs_if not_less neg_less_eq_nonneg less_eq_neg_nonpos)

   844    (auto simp del: minus_add_distrib simp add: minus_add_distrib [symmetric]

   845      neg_less_eq_nonneg less_eq_neg_nonpos, auto intro: add_nonneg_nonneg,

   846       auto intro!: less_imp_le add_neg_neg)

   847 qed (auto simp add: abs_if less_eq_neg_nonpos neg_equal_zero)

   848

   849 end

   850

   851 (* The "strict" suffix can be seen as describing the combination of ordered_ring and no_zero_divisors.

   852    Basically, ordered_ring + no_zero_divisors = ordered_ring_strict.

   853  *)

   854 class ordered_ring_strict = ring + ordered_semiring_strict

   855   + ordered_ab_group_add + abs_if

   856 begin

   857

   858 subclass ordered_ring ..

   859

   860 lemma mult_strict_left_mono_neg:

   861   "b < a \<Longrightarrow> c < 0 \<Longrightarrow> c * a < c * b"

   862   apply (drule mult_strict_left_mono [of _ _ "uminus c"])

   863   apply (simp_all add: minus_mult_left [symmetric])

   864   done

   865

   866 lemma mult_strict_right_mono_neg:

   867   "b < a \<Longrightarrow> c < 0 \<Longrightarrow> a * c < b * c"

   868   apply (drule mult_strict_right_mono [of _ _ "uminus c"])

   869   apply (simp_all add: minus_mult_right [symmetric])

   870   done

   871

   872 lemma mult_neg_neg:

   873   "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> 0 < a * b"

   874 by (drule mult_strict_right_mono_neg, auto)

   875

   876 subclass ring_no_zero_divisors

   877 proof

   878   fix a b

   879   assume "a \<noteq> 0" then have A: "a < 0 \<or> 0 < a" by (simp add: neq_iff)

   880   assume "b \<noteq> 0" then have B: "b < 0 \<or> 0 < b" by (simp add: neq_iff)

   881   have "a * b < 0 \<or> 0 < a * b"

   882   proof (cases "a < 0")

   883     case True note A' = this

   884     show ?thesis proof (cases "b < 0")

   885       case True with A'

   886       show ?thesis by (auto dest: mult_neg_neg)

   887     next

   888       case False with B have "0 < b" by auto

   889       with A' show ?thesis by (auto dest: mult_strict_right_mono)

   890     qed

   891   next

   892     case False with A have A': "0 < a" by auto

   893     show ?thesis proof (cases "b < 0")

   894       case True with A'

   895       show ?thesis by (auto dest: mult_strict_right_mono_neg)

   896     next

   897       case False with B have "0 < b" by auto

   898       with A' show ?thesis by (auto dest: mult_pos_pos)

   899     qed

   900   qed

   901   then show "a * b \<noteq> 0" by (simp add: neq_iff)

   902 qed

   903

   904 lemma zero_less_mult_iff:

   905   "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0"

   906   apply (auto simp add: mult_pos_pos mult_neg_neg)

   907   apply (simp_all add: not_less le_less)

   908   apply (erule disjE) apply assumption defer

   909   apply (erule disjE) defer apply (drule sym) apply simp

   910   apply (erule disjE) defer apply (drule sym) apply simp

   911   apply (erule disjE) apply assumption apply (drule sym) apply simp

   912   apply (drule sym) apply simp

   913   apply (blast dest: zero_less_mult_pos)

   914   apply (blast dest: zero_less_mult_pos2)

   915   done

   916

   917 lemma zero_le_mult_iff:

   918   "0 \<le> a * b \<longleftrightarrow> 0 \<le> a \<and> 0 \<le> b \<or> a \<le> 0 \<and> b \<le> 0"

   919 by (auto simp add: eq_commute [of 0] le_less not_less zero_less_mult_iff)

   920

   921 lemma mult_less_0_iff:

   922   "a * b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b"

   923   apply (insert zero_less_mult_iff [of "-a" b])

   924   apply (force simp add: minus_mult_left[symmetric])

   925   done

   926

   927 lemma mult_le_0_iff:

   928   "a * b \<le> 0 \<longleftrightarrow> 0 \<le> a \<and> b \<le> 0 \<or> a \<le> 0 \<and> 0 \<le> b"

   929   apply (insert zero_le_mult_iff [of "-a" b])

   930   apply (force simp add: minus_mult_left[symmetric])

   931   done

   932

   933 lemma zero_le_square [simp]: "0 \<le> a * a"

   934 by (simp add: zero_le_mult_iff linear)

   935

   936 lemma not_square_less_zero [simp]: "\<not> (a * a < 0)"

   937 by (simp add: not_less)

   938

   939 text{*Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"},

   940    also with the relations @{text "\<le>"} and equality.*}

   941

   942 text{*These disjunction'' versions produce two cases when the comparison is

   943  an assumption, but effectively four when the comparison is a goal.*}

   944

   945 lemma mult_less_cancel_right_disj:

   946   "a * c < b * c \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"

   947   apply (cases "c = 0")

   948   apply (auto simp add: neq_iff mult_strict_right_mono

   949                       mult_strict_right_mono_neg)

   950   apply (auto simp add: not_less

   951                       not_le [symmetric, of "a*c"]

   952                       not_le [symmetric, of a])

   953   apply (erule_tac [!] notE)

   954   apply (auto simp add: less_imp_le mult_right_mono

   955                       mult_right_mono_neg)

   956   done

   957

   958 lemma mult_less_cancel_left_disj:

   959   "c * a < c * b \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"

   960   apply (cases "c = 0")

   961   apply (auto simp add: neq_iff mult_strict_left_mono

   962                       mult_strict_left_mono_neg)

   963   apply (auto simp add: not_less

   964                       not_le [symmetric, of "c*a"]

   965                       not_le [symmetric, of a])

   966   apply (erule_tac [!] notE)

   967   apply (auto simp add: less_imp_le mult_left_mono

   968                       mult_left_mono_neg)

   969   done

   970

   971 text{*The conjunction of implication'' lemmas produce two cases when the

   972 comparison is a goal, but give four when the comparison is an assumption.*}

   973

   974 lemma mult_less_cancel_right:

   975   "a * c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)"

   976   using mult_less_cancel_right_disj [of a c b] by auto

   977

   978 lemma mult_less_cancel_left:

   979   "c * a < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)"

   980   using mult_less_cancel_left_disj [of c a b] by auto

   981

   982 lemma mult_le_cancel_right:

   983    "a * c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"

   984 by (simp add: not_less [symmetric] mult_less_cancel_right_disj)

   985

   986 lemma mult_le_cancel_left:

   987   "c * a \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"

   988 by (simp add: not_less [symmetric] mult_less_cancel_left_disj)

   989

   990 end

   991

   992 text{*Legacy - use @{text algebra_simps} *}

   993 lemmas ring_simps[noatp] = algebra_simps

   994

   995

   996 class pordered_comm_ring = comm_ring + pordered_comm_semiring

   997 begin

   998

   999 subclass pordered_ring ..

  1000 subclass pordered_cancel_comm_semiring ..

  1001

  1002 end

  1003

  1004 class ordered_semidom = comm_semiring_1_cancel + ordered_comm_semiring_strict +

  1005   (*previously ordered_semiring*)

  1006   assumes zero_less_one [simp]: "0 < 1"

  1007 begin

  1008

  1009 lemma pos_add_strict:

  1010   shows "0 < a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"

  1011   using add_strict_mono [of zero a b c] by simp

  1012

  1013 lemma zero_le_one [simp]: "0 \<le> 1"

  1014 by (rule zero_less_one [THEN less_imp_le])

  1015

  1016 lemma not_one_le_zero [simp]: "\<not> 1 \<le> 0"

  1017 by (simp add: not_le)

  1018

  1019 lemma not_one_less_zero [simp]: "\<not> 1 < 0"

  1020 by (simp add: not_less)

  1021

  1022 lemma less_1_mult:

  1023   assumes "1 < m" and "1 < n"

  1024   shows "1 < m * n"

  1025   using assms mult_strict_mono [of 1 m 1 n]

  1026     by (simp add:  less_trans [OF zero_less_one])

  1027

  1028 end

  1029

  1030 class ordered_idom = comm_ring_1 +

  1031   ordered_comm_semiring_strict + ordered_ab_group_add +

  1032   abs_if + sgn_if

  1033   (*previously ordered_ring*)

  1034 begin

  1035

  1036 subclass ordered_ring_strict ..

  1037 subclass pordered_comm_ring ..

  1038 subclass idom ..

  1039

  1040 subclass ordered_semidom

  1041 proof

  1042   have "0 \<le> 1 * 1" by (rule zero_le_square)

  1043   thus "0 < 1" by (simp add: le_less)

  1044 qed

  1045

  1046 lemma linorder_neqE_ordered_idom:

  1047   assumes "x \<noteq> y" obtains "x < y" | "y < x"

  1048   using assms by (rule neqE)

  1049

  1050 text {* These cancellation simprules also produce two cases when the comparison is a goal. *}

  1051

  1052 lemma mult_le_cancel_right1:

  1053   "c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)"

  1054 by (insert mult_le_cancel_right [of 1 c b], simp)

  1055

  1056 lemma mult_le_cancel_right2:

  1057   "a * c \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)"

  1058 by (insert mult_le_cancel_right [of a c 1], simp)

  1059

  1060 lemma mult_le_cancel_left1:

  1061   "c \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)"

  1062 by (insert mult_le_cancel_left [of c 1 b], simp)

  1063

  1064 lemma mult_le_cancel_left2:

  1065   "c * a \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)"

  1066 by (insert mult_le_cancel_left [of c a 1], simp)

  1067

  1068 lemma mult_less_cancel_right1:

  1069   "c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)"

  1070 by (insert mult_less_cancel_right [of 1 c b], simp)

  1071

  1072 lemma mult_less_cancel_right2:

  1073   "a * c < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"

  1074 by (insert mult_less_cancel_right [of a c 1], simp)

  1075

  1076 lemma mult_less_cancel_left1:

  1077   "c < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)"

  1078 by (insert mult_less_cancel_left [of c 1 b], simp)

  1079

  1080 lemma mult_less_cancel_left2:

  1081   "c * a < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"

  1082 by (insert mult_less_cancel_left [of c a 1], simp)

  1083

  1084 lemma sgn_sgn [simp]:

  1085   "sgn (sgn a) = sgn a"

  1086 unfolding sgn_if by simp

  1087

  1088 lemma sgn_0_0:

  1089   "sgn a = 0 \<longleftrightarrow> a = 0"

  1090 unfolding sgn_if by simp

  1091

  1092 lemma sgn_1_pos:

  1093   "sgn a = 1 \<longleftrightarrow> a > 0"

  1094 unfolding sgn_if by (simp add: neg_equal_zero)

  1095

  1096 lemma sgn_1_neg:

  1097   "sgn a = - 1 \<longleftrightarrow> a < 0"

  1098 unfolding sgn_if by (auto simp add: equal_neg_zero)

  1099

  1100 lemma sgn_pos [simp]:

  1101   "0 < a \<Longrightarrow> sgn a = 1"

  1102 unfolding sgn_1_pos .

  1103

  1104 lemma sgn_neg [simp]:

  1105   "a < 0 \<Longrightarrow> sgn a = - 1"

  1106 unfolding sgn_1_neg .

  1107

  1108 lemma sgn_times:

  1109   "sgn (a * b) = sgn a * sgn b"

  1110 by (auto simp add: sgn_if zero_less_mult_iff)

  1111

  1112 lemma abs_sgn: "abs k = k * sgn k"

  1113 unfolding sgn_if abs_if by auto

  1114

  1115 lemma sgn_greater [simp]:

  1116   "0 < sgn a \<longleftrightarrow> 0 < a"

  1117   unfolding sgn_if by auto

  1118

  1119 lemma sgn_less [simp]:

  1120   "sgn a < 0 \<longleftrightarrow> a < 0"

  1121   unfolding sgn_if by auto

  1122

  1123 lemma abs_dvd_iff [simp]: "(abs m) dvd k \<longleftrightarrow> m dvd k"

  1124   by (simp add: abs_if)

  1125

  1126 lemma dvd_abs_iff [simp]: "m dvd (abs k) \<longleftrightarrow> m dvd k"

  1127   by (simp add: abs_if)

  1128

  1129 end

  1130

  1131 class ordered_field = field + ordered_idom

  1132

  1133 text {* Simprules for comparisons where common factors can be cancelled. *}

  1134

  1135 lemmas mult_compare_simps[noatp] =

  1136     mult_le_cancel_right mult_le_cancel_left

  1137     mult_le_cancel_right1 mult_le_cancel_right2

  1138     mult_le_cancel_left1 mult_le_cancel_left2

  1139     mult_less_cancel_right mult_less_cancel_left

  1140     mult_less_cancel_right1 mult_less_cancel_right2

  1141     mult_less_cancel_left1 mult_less_cancel_left2

  1142     mult_cancel_right mult_cancel_left

  1143     mult_cancel_right1 mult_cancel_right2

  1144     mult_cancel_left1 mult_cancel_left2

  1145

  1146 -- {* FIXME continue localization here *}

  1147

  1148 lemma inverse_nonzero_iff_nonzero [simp]:

  1149    "(inverse a = 0) = (a = (0::'a::{division_ring,division_by_zero}))"

  1150 by (force dest: inverse_zero_imp_zero)

  1151

  1152 lemma inverse_minus_eq [simp]:

  1153    "inverse(-a) = -inverse(a::'a::{division_ring,division_by_zero})"

  1154 proof cases

  1155   assume "a=0" thus ?thesis by (simp add: inverse_zero)

  1156 next

  1157   assume "a\<noteq>0"

  1158   thus ?thesis by (simp add: nonzero_inverse_minus_eq)

  1159 qed

  1160

  1161 lemma inverse_eq_imp_eq:

  1162   "inverse a = inverse b ==> a = (b::'a::{division_ring,division_by_zero})"

  1163 apply (cases "a=0 | b=0")

  1164  apply (force dest!: inverse_zero_imp_zero

  1165               simp add: eq_commute [of "0::'a"])

  1166 apply (force dest!: nonzero_inverse_eq_imp_eq)

  1167 done

  1168

  1169 lemma inverse_eq_iff_eq [simp]:

  1170   "(inverse a = inverse b) = (a = (b::'a::{division_ring,division_by_zero}))"

  1171 by (force dest!: inverse_eq_imp_eq)

  1172

  1173 lemma inverse_inverse_eq [simp]:

  1174      "inverse(inverse (a::'a::{division_ring,division_by_zero})) = a"

  1175   proof cases

  1176     assume "a=0" thus ?thesis by simp

  1177   next

  1178     assume "a\<noteq>0"

  1179     thus ?thesis by (simp add: nonzero_inverse_inverse_eq)

  1180   qed

  1181

  1182 text{*This version builds in division by zero while also re-orienting

  1183       the right-hand side.*}

  1184 lemma inverse_mult_distrib [simp]:

  1185      "inverse(a*b) = inverse(a) * inverse(b::'a::{field,division_by_zero})"

  1186   proof cases

  1187     assume "a \<noteq> 0 & b \<noteq> 0"

  1188     thus ?thesis by (simp add: nonzero_inverse_mult_distrib mult_commute)

  1189   next

  1190     assume "~ (a \<noteq> 0 & b \<noteq> 0)"

  1191     thus ?thesis by force

  1192   qed

  1193

  1194 text{*There is no slick version using division by zero.*}

  1195 lemma inverse_add:

  1196   "[|a \<noteq> 0;  b \<noteq> 0|]

  1197    ==> inverse a + inverse b = (a+b) * inverse a * inverse (b::'a::field)"

  1198 by (simp add: division_ring_inverse_add mult_ac)

  1199

  1200 lemma inverse_divide [simp]:

  1201   "inverse (a/b) = b / (a::'a::{field,division_by_zero})"

  1202 by (simp add: divide_inverse mult_commute)

  1203

  1204

  1205 subsection {* Calculations with fractions *}

  1206

  1207 text{* There is a whole bunch of simp-rules just for class @{text

  1208 field} but none for class @{text field} and @{text nonzero_divides}

  1209 because the latter are covered by a simproc. *}

  1210

  1211 lemma nonzero_mult_divide_mult_cancel_left[simp,noatp]:

  1212 assumes [simp]: "b\<noteq>0" and [simp]: "c\<noteq>0" shows "(c*a)/(c*b) = a/(b::'a::field)"

  1213 proof -

  1214   have "(c*a)/(c*b) = c * a * (inverse b * inverse c)"

  1215     by (simp add: divide_inverse nonzero_inverse_mult_distrib)

  1216   also have "... =  a * inverse b * (inverse c * c)"

  1217     by (simp only: mult_ac)

  1218   also have "... =  a * inverse b" by simp

  1219     finally show ?thesis by (simp add: divide_inverse)

  1220 qed

  1221

  1222 lemma mult_divide_mult_cancel_left:

  1223   "c\<noteq>0 ==> (c*a) / (c*b) = a / (b::'a::{field,division_by_zero})"

  1224 apply (cases "b = 0")

  1225 apply (simp_all add: nonzero_mult_divide_mult_cancel_left)

  1226 done

  1227

  1228 lemma nonzero_mult_divide_mult_cancel_right [noatp]:

  1229   "[|b\<noteq>0; c\<noteq>0|] ==> (a*c) / (b*c) = a/(b::'a::field)"

  1230 by (simp add: mult_commute [of _ c] nonzero_mult_divide_mult_cancel_left)

  1231

  1232 lemma mult_divide_mult_cancel_right:

  1233   "c\<noteq>0 ==> (a*c) / (b*c) = a / (b::'a::{field,division_by_zero})"

  1234 apply (cases "b = 0")

  1235 apply (simp_all add: nonzero_mult_divide_mult_cancel_right)

  1236 done

  1237

  1238 lemma divide_1 [simp]: "a/1 = (a::'a::field)"

  1239 by (simp add: divide_inverse)

  1240

  1241 lemma times_divide_eq_right: "a * (b/c) = (a*b) / (c::'a::field)"

  1242 by (simp add: divide_inverse mult_assoc)

  1243

  1244 lemma times_divide_eq_left: "(b/c) * a = (b*a) / (c::'a::field)"

  1245 by (simp add: divide_inverse mult_ac)

  1246

  1247 lemmas times_divide_eq[noatp] = times_divide_eq_right times_divide_eq_left

  1248

  1249 lemma divide_divide_eq_right [simp,noatp]:

  1250   "a / (b/c) = (a*c) / (b::'a::{field,division_by_zero})"

  1251 by (simp add: divide_inverse mult_ac)

  1252

  1253 lemma divide_divide_eq_left [simp,noatp]:

  1254   "(a / b) / (c::'a::{field,division_by_zero}) = a / (b*c)"

  1255 by (simp add: divide_inverse mult_assoc)

  1256

  1257 lemma add_frac_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==>

  1258     x / y + w / z = (x * z + w * y) / (y * z)"

  1259 apply (subgoal_tac "x / y = (x * z) / (y * z)")

  1260 apply (erule ssubst)

  1261 apply (subgoal_tac "w / z = (w * y) / (y * z)")

  1262 apply (erule ssubst)

  1263 apply (rule add_divide_distrib [THEN sym])

  1264 apply (subst mult_commute)

  1265 apply (erule nonzero_mult_divide_mult_cancel_left [THEN sym])

  1266 apply assumption

  1267 apply (erule nonzero_mult_divide_mult_cancel_right [THEN sym])

  1268 apply assumption

  1269 done

  1270

  1271

  1272 subsubsection{*Special Cancellation Simprules for Division*}

  1273

  1274 lemma mult_divide_mult_cancel_left_if[simp,noatp]:

  1275 fixes c :: "'a :: {field,division_by_zero}"

  1276 shows "(c*a) / (c*b) = (if c=0 then 0 else a/b)"

  1277 by (simp add: mult_divide_mult_cancel_left)

  1278

  1279 lemma nonzero_mult_divide_cancel_right[simp,noatp]:

  1280   "b \<noteq> 0 \<Longrightarrow> a * b / b = (a::'a::field)"

  1281 using nonzero_mult_divide_mult_cancel_right[of 1 b a] by simp

  1282

  1283 lemma nonzero_mult_divide_cancel_left[simp,noatp]:

  1284   "a \<noteq> 0 \<Longrightarrow> a * b / a = (b::'a::field)"

  1285 using nonzero_mult_divide_mult_cancel_left[of 1 a b] by simp

  1286

  1287

  1288 lemma nonzero_divide_mult_cancel_right[simp,noatp]:

  1289   "\<lbrakk> a\<noteq>0; b\<noteq>0 \<rbrakk> \<Longrightarrow> b / (a * b) = 1/(a::'a::field)"

  1290 using nonzero_mult_divide_mult_cancel_right[of a b 1] by simp

  1291

  1292 lemma nonzero_divide_mult_cancel_left[simp,noatp]:

  1293   "\<lbrakk> a\<noteq>0; b\<noteq>0 \<rbrakk> \<Longrightarrow> a / (a * b) = 1/(b::'a::field)"

  1294 using nonzero_mult_divide_mult_cancel_left[of b a 1] by simp

  1295

  1296

  1297 lemma nonzero_mult_divide_mult_cancel_left2[simp,noatp]:

  1298   "[|b\<noteq>0; c\<noteq>0|] ==> (c*a) / (b*c) = a/(b::'a::field)"

  1299 using nonzero_mult_divide_mult_cancel_left[of b c a] by(simp add:mult_ac)

  1300

  1301 lemma nonzero_mult_divide_mult_cancel_right2[simp,noatp]:

  1302   "[|b\<noteq>0; c\<noteq>0|] ==> (a*c) / (c*b) = a/(b::'a::field)"

  1303 using nonzero_mult_divide_mult_cancel_right[of b c a] by(simp add:mult_ac)

  1304

  1305

  1306 subsection {* Division and Unary Minus *}

  1307

  1308 lemma nonzero_minus_divide_left: "b \<noteq> 0 ==> - (a/b) = (-a) / (b::'a::field)"

  1309 by (simp add: divide_inverse)

  1310

  1311 lemma nonzero_minus_divide_right: "b \<noteq> 0 ==> - (a/b) = a / -(b::'a::field)"

  1312 by (simp add: divide_inverse nonzero_inverse_minus_eq)

  1313

  1314 lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (-a)/(-b) = a / (b::'a::field)"

  1315 by (simp add: divide_inverse nonzero_inverse_minus_eq)

  1316

  1317 lemma minus_divide_left: "- (a/b) = (-a) / (b::'a::field)"

  1318 by (simp add: divide_inverse)

  1319

  1320 lemma minus_divide_right: "- (a/b) = a / -(b::'a::{field,division_by_zero})"

  1321 by (simp add: divide_inverse)

  1322

  1323

  1324 text{*The effect is to extract signs from divisions*}

  1325 lemmas divide_minus_left[noatp] = minus_divide_left [symmetric]

  1326 lemmas divide_minus_right[noatp] = minus_divide_right [symmetric]

  1327 declare divide_minus_left [simp]   divide_minus_right [simp]

  1328

  1329 lemma minus_divide_divide [simp]:

  1330   "(-a)/(-b) = a / (b::'a::{field,division_by_zero})"

  1331 apply (cases "b=0", simp)

  1332 apply (simp add: nonzero_minus_divide_divide)

  1333 done

  1334

  1335 lemma diff_divide_distrib: "(a-b)/(c::'a::field) = a/c - b/c"

  1336 by (simp add: diff_minus add_divide_distrib)

  1337

  1338 lemma add_divide_eq_iff:

  1339   "(z::'a::field) \<noteq> 0 \<Longrightarrow> x + y/z = (z*x + y)/z"

  1340 by(simp add:add_divide_distrib nonzero_mult_divide_cancel_left)

  1341

  1342 lemma divide_add_eq_iff:

  1343   "(z::'a::field) \<noteq> 0 \<Longrightarrow> x/z + y = (x + z*y)/z"

  1344 by(simp add:add_divide_distrib nonzero_mult_divide_cancel_left)

  1345

  1346 lemma diff_divide_eq_iff:

  1347   "(z::'a::field) \<noteq> 0 \<Longrightarrow> x - y/z = (z*x - y)/z"

  1348 by(simp add:diff_divide_distrib nonzero_mult_divide_cancel_left)

  1349

  1350 lemma divide_diff_eq_iff:

  1351   "(z::'a::field) \<noteq> 0 \<Longrightarrow> x/z - y = (x - z*y)/z"

  1352 by(simp add:diff_divide_distrib nonzero_mult_divide_cancel_left)

  1353

  1354 lemma nonzero_eq_divide_eq: "c\<noteq>0 ==> ((a::'a::field) = b/c) = (a*c = b)"

  1355 proof -

  1356   assume [simp]: "c\<noteq>0"

  1357   have "(a = b/c) = (a*c = (b/c)*c)" by simp

  1358   also have "... = (a*c = b)" by (simp add: divide_inverse mult_assoc)

  1359   finally show ?thesis .

  1360 qed

  1361

  1362 lemma nonzero_divide_eq_eq: "c\<noteq>0 ==> (b/c = (a::'a::field)) = (b = a*c)"

  1363 proof -

  1364   assume [simp]: "c\<noteq>0"

  1365   have "(b/c = a) = ((b/c)*c = a*c)"  by simp

  1366   also have "... = (b = a*c)"  by (simp add: divide_inverse mult_assoc)

  1367   finally show ?thesis .

  1368 qed

  1369

  1370 lemma eq_divide_eq:

  1371   "((a::'a::{field,division_by_zero}) = b/c) = (if c\<noteq>0 then a*c = b else a=0)"

  1372 by (simp add: nonzero_eq_divide_eq)

  1373

  1374 lemma divide_eq_eq:

  1375   "(b/c = (a::'a::{field,division_by_zero})) = (if c\<noteq>0 then b = a*c else a=0)"

  1376 by (force simp add: nonzero_divide_eq_eq)

  1377

  1378 lemma divide_eq_imp: "(c::'a::{division_by_zero,field}) ~= 0 ==>

  1379     b = a * c ==> b / c = a"

  1380 by (subst divide_eq_eq, simp)

  1381

  1382 lemma eq_divide_imp: "(c::'a::{division_by_zero,field}) ~= 0 ==>

  1383     a * c = b ==> a = b / c"

  1384 by (subst eq_divide_eq, simp)

  1385

  1386

  1387 lemmas field_eq_simps[noatp] = algebra_simps

  1388   (* pull / out*)

  1389   add_divide_eq_iff divide_add_eq_iff

  1390   diff_divide_eq_iff divide_diff_eq_iff

  1391   (* multiply eqn *)

  1392   nonzero_eq_divide_eq nonzero_divide_eq_eq

  1393 (* is added later:

  1394   times_divide_eq_left times_divide_eq_right

  1395 *)

  1396

  1397 text{*An example:*}

  1398 lemma fixes a b c d e f :: "'a::field"

  1399 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"

  1400 apply(subgoal_tac "(c-d)*(e-f)*(a-b) \<noteq> 0")

  1401  apply(simp add:field_eq_simps)

  1402 apply(simp)

  1403 done

  1404

  1405

  1406 lemma diff_frac_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==>

  1407     x / y - w / z = (x * z - w * y) / (y * z)"

  1408 by (simp add:field_eq_simps times_divide_eq)

  1409

  1410 lemma frac_eq_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==>

  1411     (x / y = w / z) = (x * z = w * y)"

  1412 by (simp add:field_eq_simps times_divide_eq)

  1413

  1414

  1415 subsection {* Ordered Fields *}

  1416

  1417 lemma positive_imp_inverse_positive:

  1418 assumes a_gt_0: "0 < a"  shows "0 < inverse (a::'a::ordered_field)"

  1419 proof -

  1420   have "0 < a * inverse a"

  1421     by (simp add: a_gt_0 [THEN order_less_imp_not_eq2] zero_less_one)

  1422   thus "0 < inverse a"

  1423     by (simp add: a_gt_0 [THEN order_less_not_sym] zero_less_mult_iff)

  1424 qed

  1425

  1426 lemma negative_imp_inverse_negative:

  1427   "a < 0 ==> inverse a < (0::'a::ordered_field)"

  1428 by (insert positive_imp_inverse_positive [of "-a"],

  1429     simp add: nonzero_inverse_minus_eq order_less_imp_not_eq)

  1430

  1431 lemma inverse_le_imp_le:

  1432 assumes invle: "inverse a \<le> inverse b" and apos:  "0 < a"

  1433 shows "b \<le> (a::'a::ordered_field)"

  1434 proof (rule classical)

  1435   assume "~ b \<le> a"

  1436   hence "a < b"  by (simp add: linorder_not_le)

  1437   hence bpos: "0 < b"  by (blast intro: apos order_less_trans)

  1438   hence "a * inverse a \<le> a * inverse b"

  1439     by (simp add: apos invle order_less_imp_le mult_left_mono)

  1440   hence "(a * inverse a) * b \<le> (a * inverse b) * b"

  1441     by (simp add: bpos order_less_imp_le mult_right_mono)

  1442   thus "b \<le> a"  by (simp add: mult_assoc apos bpos order_less_imp_not_eq2)

  1443 qed

  1444

  1445 lemma inverse_positive_imp_positive:

  1446 assumes inv_gt_0: "0 < inverse a" and nz: "a \<noteq> 0"

  1447 shows "0 < (a::'a::ordered_field)"

  1448 proof -

  1449   have "0 < inverse (inverse a)"

  1450     using inv_gt_0 by (rule positive_imp_inverse_positive)

  1451   thus "0 < a"

  1452     using nz by (simp add: nonzero_inverse_inverse_eq)

  1453 qed

  1454

  1455 lemma inverse_positive_iff_positive [simp]:

  1456   "(0 < inverse a) = (0 < (a::'a::{ordered_field,division_by_zero}))"

  1457 apply (cases "a = 0", simp)

  1458 apply (blast intro: inverse_positive_imp_positive positive_imp_inverse_positive)

  1459 done

  1460

  1461 lemma inverse_negative_imp_negative:

  1462 assumes inv_less_0: "inverse a < 0" and nz:  "a \<noteq> 0"

  1463 shows "a < (0::'a::ordered_field)"

  1464 proof -

  1465   have "inverse (inverse a) < 0"

  1466     using inv_less_0 by (rule negative_imp_inverse_negative)

  1467   thus "a < 0" using nz by (simp add: nonzero_inverse_inverse_eq)

  1468 qed

  1469

  1470 lemma inverse_negative_iff_negative [simp]:

  1471   "(inverse a < 0) = (a < (0::'a::{ordered_field,division_by_zero}))"

  1472 apply (cases "a = 0", simp)

  1473 apply (blast intro: inverse_negative_imp_negative negative_imp_inverse_negative)

  1474 done

  1475

  1476 lemma inverse_nonnegative_iff_nonnegative [simp]:

  1477   "(0 \<le> inverse a) = (0 \<le> (a::'a::{ordered_field,division_by_zero}))"

  1478 by (simp add: linorder_not_less [symmetric])

  1479

  1480 lemma inverse_nonpositive_iff_nonpositive [simp]:

  1481   "(inverse a \<le> 0) = (a \<le> (0::'a::{ordered_field,division_by_zero}))"

  1482 by (simp add: linorder_not_less [symmetric])

  1483

  1484 lemma ordered_field_no_lb: "\<forall> x. \<exists>y. y < (x::'a::ordered_field)"

  1485 proof

  1486   fix x::'a

  1487   have m1: "- (1::'a) < 0" by simp

  1488   from add_strict_right_mono[OF m1, where c=x]

  1489   have "(- 1) + x < x" by simp

  1490   thus "\<exists>y. y < x" by blast

  1491 qed

  1492

  1493 lemma ordered_field_no_ub: "\<forall> x. \<exists>y. y > (x::'a::ordered_field)"

  1494 proof

  1495   fix x::'a

  1496   have m1: " (1::'a) > 0" by simp

  1497   from add_strict_right_mono[OF m1, where c=x]

  1498   have "1 + x > x" by simp

  1499   thus "\<exists>y. y > x" by blast

  1500 qed

  1501

  1502 subsection{*Anti-Monotonicity of @{term inverse}*}

  1503

  1504 lemma less_imp_inverse_less:

  1505 assumes less: "a < b" and apos:  "0 < a"

  1506 shows "inverse b < inverse (a::'a::ordered_field)"

  1507 proof (rule ccontr)

  1508   assume "~ inverse b < inverse a"

  1509   hence "inverse a \<le> inverse b" by (simp add: linorder_not_less)

  1510   hence "~ (a < b)"

  1511     by (simp add: linorder_not_less inverse_le_imp_le [OF _ apos])

  1512   thus False by (rule notE [OF _ less])

  1513 qed

  1514

  1515 lemma inverse_less_imp_less:

  1516   "[|inverse a < inverse b; 0 < a|] ==> b < (a::'a::ordered_field)"

  1517 apply (simp add: order_less_le [of "inverse a"] order_less_le [of "b"])

  1518 apply (force dest!: inverse_le_imp_le nonzero_inverse_eq_imp_eq)

  1519 done

  1520

  1521 text{*Both premises are essential. Consider -1 and 1.*}

  1522 lemma inverse_less_iff_less [simp,noatp]:

  1523   "[|0 < a; 0 < b|] ==> (inverse a < inverse b) = (b < (a::'a::ordered_field))"

  1524 by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less)

  1525

  1526 lemma le_imp_inverse_le:

  1527   "[|a \<le> b; 0 < a|] ==> inverse b \<le> inverse (a::'a::ordered_field)"

  1528 by (force simp add: order_le_less less_imp_inverse_less)

  1529

  1530 lemma inverse_le_iff_le [simp,noatp]:

  1531  "[|0 < a; 0 < b|] ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::ordered_field))"

  1532 by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le)

  1533

  1534

  1535 text{*These results refer to both operands being negative.  The opposite-sign

  1536 case is trivial, since inverse preserves signs.*}

  1537 lemma inverse_le_imp_le_neg:

  1538   "[|inverse a \<le> inverse b; b < 0|] ==> b \<le> (a::'a::ordered_field)"

  1539 apply (rule classical)

  1540 apply (subgoal_tac "a < 0")

  1541  prefer 2 apply (force simp add: linorder_not_le intro: order_less_trans)

  1542 apply (insert inverse_le_imp_le [of "-b" "-a"])

  1543 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)

  1544 done

  1545

  1546 lemma less_imp_inverse_less_neg:

  1547    "[|a < b; b < 0|] ==> inverse b < inverse (a::'a::ordered_field)"

  1548 apply (subgoal_tac "a < 0")

  1549  prefer 2 apply (blast intro: order_less_trans)

  1550 apply (insert less_imp_inverse_less [of "-b" "-a"])

  1551 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)

  1552 done

  1553

  1554 lemma inverse_less_imp_less_neg:

  1555    "[|inverse a < inverse b; b < 0|] ==> b < (a::'a::ordered_field)"

  1556 apply (rule classical)

  1557 apply (subgoal_tac "a < 0")

  1558  prefer 2

  1559  apply (force simp add: linorder_not_less intro: order_le_less_trans)

  1560 apply (insert inverse_less_imp_less [of "-b" "-a"])

  1561 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)

  1562 done

  1563

  1564 lemma inverse_less_iff_less_neg [simp,noatp]:

  1565   "[|a < 0; b < 0|] ==> (inverse a < inverse b) = (b < (a::'a::ordered_field))"

  1566 apply (insert inverse_less_iff_less [of "-b" "-a"])

  1567 apply (simp del: inverse_less_iff_less

  1568             add: order_less_imp_not_eq nonzero_inverse_minus_eq)

  1569 done

  1570

  1571 lemma le_imp_inverse_le_neg:

  1572   "[|a \<le> b; b < 0|] ==> inverse b \<le> inverse (a::'a::ordered_field)"

  1573 by (force simp add: order_le_less less_imp_inverse_less_neg)

  1574

  1575 lemma inverse_le_iff_le_neg [simp,noatp]:

  1576  "[|a < 0; b < 0|] ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::ordered_field))"

  1577 by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg)

  1578

  1579

  1580 subsection{*Inverses and the Number One*}

  1581

  1582 lemma one_less_inverse_iff:

  1583   "(1 < inverse x) = (0 < x & x < (1::'a::{ordered_field,division_by_zero}))"

  1584 proof cases

  1585   assume "0 < x"

  1586     with inverse_less_iff_less [OF zero_less_one, of x]

  1587     show ?thesis by simp

  1588 next

  1589   assume notless: "~ (0 < x)"

  1590   have "~ (1 < inverse x)"

  1591   proof

  1592     assume "1 < inverse x"

  1593     also with notless have "... \<le> 0" by (simp add: linorder_not_less)

  1594     also have "... < 1" by (rule zero_less_one)

  1595     finally show False by auto

  1596   qed

  1597   with notless show ?thesis by simp

  1598 qed

  1599

  1600 lemma inverse_eq_1_iff [simp]:

  1601   "(inverse x = 1) = (x = (1::'a::{field,division_by_zero}))"

  1602 by (insert inverse_eq_iff_eq [of x 1], simp)

  1603

  1604 lemma one_le_inverse_iff:

  1605   "(1 \<le> inverse x) = (0 < x & x \<le> (1::'a::{ordered_field,division_by_zero}))"

  1606 by (force simp add: order_le_less one_less_inverse_iff zero_less_one

  1607                     eq_commute [of 1])

  1608

  1609 lemma inverse_less_1_iff:

  1610   "(inverse x < 1) = (x \<le> 0 | 1 < (x::'a::{ordered_field,division_by_zero}))"

  1611 by (simp add: linorder_not_le [symmetric] one_le_inverse_iff)

  1612

  1613 lemma inverse_le_1_iff:

  1614   "(inverse x \<le> 1) = (x \<le> 0 | 1 \<le> (x::'a::{ordered_field,division_by_zero}))"

  1615 by (simp add: linorder_not_less [symmetric] one_less_inverse_iff)

  1616

  1617

  1618 subsection{*Simplification of Inequalities Involving Literal Divisors*}

  1619

  1620 lemma pos_le_divide_eq: "0 < (c::'a::ordered_field) ==> (a \<le> b/c) = (a*c \<le> b)"

  1621 proof -

  1622   assume less: "0<c"

  1623   hence "(a \<le> b/c) = (a*c \<le> (b/c)*c)"

  1624     by (simp add: mult_le_cancel_right order_less_not_sym [OF less])

  1625   also have "... = (a*c \<le> b)"

  1626     by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc)

  1627   finally show ?thesis .

  1628 qed

  1629

  1630 lemma neg_le_divide_eq: "c < (0::'a::ordered_field) ==> (a \<le> b/c) = (b \<le> a*c)"

  1631 proof -

  1632   assume less: "c<0"

  1633   hence "(a \<le> b/c) = ((b/c)*c \<le> a*c)"

  1634     by (simp add: mult_le_cancel_right order_less_not_sym [OF less])

  1635   also have "... = (b \<le> a*c)"

  1636     by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc)

  1637   finally show ?thesis .

  1638 qed

  1639

  1640 lemma le_divide_eq:

  1641   "(a \<le> b/c) =

  1642    (if 0 < c then a*c \<le> b

  1643              else if c < 0 then b \<le> a*c

  1644              else  a \<le> (0::'a::{ordered_field,division_by_zero}))"

  1645 apply (cases "c=0", simp)

  1646 apply (force simp add: pos_le_divide_eq neg_le_divide_eq linorder_neq_iff)

  1647 done

  1648

  1649 lemma pos_divide_le_eq: "0 < (c::'a::ordered_field) ==> (b/c \<le> a) = (b \<le> a*c)"

  1650 proof -

  1651   assume less: "0<c"

  1652   hence "(b/c \<le> a) = ((b/c)*c \<le> a*c)"

  1653     by (simp add: mult_le_cancel_right order_less_not_sym [OF less])

  1654   also have "... = (b \<le> a*c)"

  1655     by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc)

  1656   finally show ?thesis .

  1657 qed

  1658

  1659 lemma neg_divide_le_eq: "c < (0::'a::ordered_field) ==> (b/c \<le> a) = (a*c \<le> b)"

  1660 proof -

  1661   assume less: "c<0"

  1662   hence "(b/c \<le> a) = (a*c \<le> (b/c)*c)"

  1663     by (simp add: mult_le_cancel_right order_less_not_sym [OF less])

  1664   also have "... = (a*c \<le> b)"

  1665     by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc)

  1666   finally show ?thesis .

  1667 qed

  1668

  1669 lemma divide_le_eq:

  1670   "(b/c \<le> a) =

  1671    (if 0 < c then b \<le> a*c

  1672              else if c < 0 then a*c \<le> b

  1673              else 0 \<le> (a::'a::{ordered_field,division_by_zero}))"

  1674 apply (cases "c=0", simp)

  1675 apply (force simp add: pos_divide_le_eq neg_divide_le_eq linorder_neq_iff)

  1676 done

  1677

  1678 lemma pos_less_divide_eq:

  1679      "0 < (c::'a::ordered_field) ==> (a < b/c) = (a*c < b)"

  1680 proof -

  1681   assume less: "0<c"

  1682   hence "(a < b/c) = (a*c < (b/c)*c)"

  1683     by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])

  1684   also have "... = (a*c < b)"

  1685     by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc)

  1686   finally show ?thesis .

  1687 qed

  1688

  1689 lemma neg_less_divide_eq:

  1690  "c < (0::'a::ordered_field) ==> (a < b/c) = (b < a*c)"

  1691 proof -

  1692   assume less: "c<0"

  1693   hence "(a < b/c) = ((b/c)*c < a*c)"

  1694     by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])

  1695   also have "... = (b < a*c)"

  1696     by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc)

  1697   finally show ?thesis .

  1698 qed

  1699

  1700 lemma less_divide_eq:

  1701   "(a < b/c) =

  1702    (if 0 < c then a*c < b

  1703              else if c < 0 then b < a*c

  1704              else  a < (0::'a::{ordered_field,division_by_zero}))"

  1705 apply (cases "c=0", simp)

  1706 apply (force simp add: pos_less_divide_eq neg_less_divide_eq linorder_neq_iff)

  1707 done

  1708

  1709 lemma pos_divide_less_eq:

  1710      "0 < (c::'a::ordered_field) ==> (b/c < a) = (b < a*c)"

  1711 proof -

  1712   assume less: "0<c"

  1713   hence "(b/c < a) = ((b/c)*c < a*c)"

  1714     by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])

  1715   also have "... = (b < a*c)"

  1716     by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc)

  1717   finally show ?thesis .

  1718 qed

  1719

  1720 lemma neg_divide_less_eq:

  1721  "c < (0::'a::ordered_field) ==> (b/c < a) = (a*c < b)"

  1722 proof -

  1723   assume less: "c<0"

  1724   hence "(b/c < a) = (a*c < (b/c)*c)"

  1725     by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])

  1726   also have "... = (a*c < b)"

  1727     by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc)

  1728   finally show ?thesis .

  1729 qed

  1730

  1731 lemma divide_less_eq:

  1732   "(b/c < a) =

  1733    (if 0 < c then b < a*c

  1734              else if c < 0 then a*c < b

  1735              else 0 < (a::'a::{ordered_field,division_by_zero}))"

  1736 apply (cases "c=0", simp)

  1737 apply (force simp add: pos_divide_less_eq neg_divide_less_eq linorder_neq_iff)

  1738 done

  1739

  1740

  1741 subsection{*Field simplification*}

  1742

  1743 text{* Lemmas @{text field_simps} multiply with denominators in in(equations)

  1744 if they can be proved to be non-zero (for equations) or positive/negative

  1745 (for inequations). Can be too aggressive and is therefore separate from the

  1746 more benign @{text algebra_simps}. *}

  1747

  1748 lemmas field_simps[noatp] = field_eq_simps

  1749   (* multiply ineqn *)

  1750   pos_divide_less_eq neg_divide_less_eq

  1751   pos_less_divide_eq neg_less_divide_eq

  1752   pos_divide_le_eq neg_divide_le_eq

  1753   pos_le_divide_eq neg_le_divide_eq

  1754

  1755 text{* Lemmas @{text sign_simps} is a first attempt to automate proofs

  1756 of positivity/negativity needed for @{text field_simps}. Have not added @{text

  1757 sign_simps} to @{text field_simps} because the former can lead to case

  1758 explosions. *}

  1759

  1760 lemmas sign_simps[noatp] = group_simps

  1761   zero_less_mult_iff  mult_less_0_iff

  1762

  1763 (* Only works once linear arithmetic is installed:

  1764 text{*An example:*}

  1765 lemma fixes a b c d e f :: "'a::ordered_field"

  1766 shows "\<lbrakk>a>b; c<d; e<f; 0 < u \<rbrakk> \<Longrightarrow>

  1767  ((a-b)*(c-d)*(e-f))/((c-d)*(e-f)*(a-b)) <

  1768  ((e-f)*(a-b)*(c-d))/((e-f)*(a-b)*(c-d)) + u"

  1769 apply(subgoal_tac "(c-d)*(e-f)*(a-b) > 0")

  1770  prefer 2 apply(simp add:sign_simps)

  1771 apply(subgoal_tac "(c-d)*(e-f)*(a-b)*u > 0")

  1772  prefer 2 apply(simp add:sign_simps)

  1773 apply(simp add:field_simps)

  1774 done

  1775 *)

  1776

  1777

  1778 subsection{*Division and Signs*}

  1779

  1780 lemma zero_less_divide_iff:

  1781      "((0::'a::{ordered_field,division_by_zero}) < a/b) = (0 < a & 0 < b | a < 0 & b < 0)"

  1782 by (simp add: divide_inverse zero_less_mult_iff)

  1783

  1784 lemma divide_less_0_iff:

  1785      "(a/b < (0::'a::{ordered_field,division_by_zero})) =

  1786       (0 < a & b < 0 | a < 0 & 0 < b)"

  1787 by (simp add: divide_inverse mult_less_0_iff)

  1788

  1789 lemma zero_le_divide_iff:

  1790      "((0::'a::{ordered_field,division_by_zero}) \<le> a/b) =

  1791       (0 \<le> a & 0 \<le> b | a \<le> 0 & b \<le> 0)"

  1792 by (simp add: divide_inverse zero_le_mult_iff)

  1793

  1794 lemma divide_le_0_iff:

  1795      "(a/b \<le> (0::'a::{ordered_field,division_by_zero})) =

  1796       (0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> b)"

  1797 by (simp add: divide_inverse mult_le_0_iff)

  1798

  1799 lemma divide_eq_0_iff [simp,noatp]:

  1800      "(a/b = 0) = (a=0 | b=(0::'a::{field,division_by_zero}))"

  1801 by (simp add: divide_inverse)

  1802

  1803 lemma divide_pos_pos:

  1804   "0 < (x::'a::ordered_field) ==> 0 < y ==> 0 < x / y"

  1805 by(simp add:field_simps)

  1806

  1807

  1808 lemma divide_nonneg_pos:

  1809   "0 <= (x::'a::ordered_field) ==> 0 < y ==> 0 <= x / y"

  1810 by(simp add:field_simps)

  1811

  1812 lemma divide_neg_pos:

  1813   "(x::'a::ordered_field) < 0 ==> 0 < y ==> x / y < 0"

  1814 by(simp add:field_simps)

  1815

  1816 lemma divide_nonpos_pos:

  1817   "(x::'a::ordered_field) <= 0 ==> 0 < y ==> x / y <= 0"

  1818 by(simp add:field_simps)

  1819

  1820 lemma divide_pos_neg:

  1821   "0 < (x::'a::ordered_field) ==> y < 0 ==> x / y < 0"

  1822 by(simp add:field_simps)

  1823

  1824 lemma divide_nonneg_neg:

  1825   "0 <= (x::'a::ordered_field) ==> y < 0 ==> x / y <= 0"

  1826 by(simp add:field_simps)

  1827

  1828 lemma divide_neg_neg:

  1829   "(x::'a::ordered_field) < 0 ==> y < 0 ==> 0 < x / y"

  1830 by(simp add:field_simps)

  1831

  1832 lemma divide_nonpos_neg:

  1833   "(x::'a::ordered_field) <= 0 ==> y < 0 ==> 0 <= x / y"

  1834 by(simp add:field_simps)

  1835

  1836

  1837 subsection{*Cancellation Laws for Division*}

  1838

  1839 lemma divide_cancel_right [simp,noatp]:

  1840      "(a/c = b/c) = (c = 0 | a = (b::'a::{field,division_by_zero}))"

  1841 apply (cases "c=0", simp)

  1842 apply (simp add: divide_inverse)

  1843 done

  1844

  1845 lemma divide_cancel_left [simp,noatp]:

  1846      "(c/a = c/b) = (c = 0 | a = (b::'a::{field,division_by_zero}))"

  1847 apply (cases "c=0", simp)

  1848 apply (simp add: divide_inverse)

  1849 done

  1850

  1851

  1852 subsection {* Division and the Number One *}

  1853

  1854 text{*Simplify expressions equated with 1*}

  1855 lemma divide_eq_1_iff [simp,noatp]:

  1856      "(a/b = 1) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"

  1857 apply (cases "b=0", simp)

  1858 apply (simp add: right_inverse_eq)

  1859 done

  1860

  1861 lemma one_eq_divide_iff [simp,noatp]:

  1862      "(1 = a/b) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"

  1863 by (simp add: eq_commute [of 1])

  1864

  1865 lemma zero_eq_1_divide_iff [simp,noatp]:

  1866      "((0::'a::{ordered_field,division_by_zero}) = 1/a) = (a = 0)"

  1867 apply (cases "a=0", simp)

  1868 apply (auto simp add: nonzero_eq_divide_eq)

  1869 done

  1870

  1871 lemma one_divide_eq_0_iff [simp,noatp]:

  1872      "(1/a = (0::'a::{ordered_field,division_by_zero})) = (a = 0)"

  1873 apply (cases "a=0", simp)

  1874 apply (insert zero_neq_one [THEN not_sym])

  1875 apply (auto simp add: nonzero_divide_eq_eq)

  1876 done

  1877

  1878 text{*Simplify expressions such as @{text "0 < 1/x"} to @{text "0 < x"}*}

  1879 lemmas zero_less_divide_1_iff = zero_less_divide_iff [of 1, simplified]

  1880 lemmas divide_less_0_1_iff = divide_less_0_iff [of 1, simplified]

  1881 lemmas zero_le_divide_1_iff = zero_le_divide_iff [of 1, simplified]

  1882 lemmas divide_le_0_1_iff = divide_le_0_iff [of 1, simplified]

  1883

  1884 declare zero_less_divide_1_iff [simp,noatp]

  1885 declare divide_less_0_1_iff [simp,noatp]

  1886 declare zero_le_divide_1_iff [simp,noatp]

  1887 declare divide_le_0_1_iff [simp,noatp]

  1888

  1889

  1890 subsection {* Ordering Rules for Division *}

  1891

  1892 lemma divide_strict_right_mono:

  1893      "[|a < b; 0 < c|] ==> a / c < b / (c::'a::ordered_field)"

  1894 by (simp add: order_less_imp_not_eq2 divide_inverse mult_strict_right_mono

  1895               positive_imp_inverse_positive)

  1896

  1897 lemma divide_right_mono:

  1898      "[|a \<le> b; 0 \<le> c|] ==> a/c \<le> b/(c::'a::{ordered_field,division_by_zero})"

  1899 by (force simp add: divide_strict_right_mono order_le_less)

  1900

  1901 lemma divide_right_mono_neg: "(a::'a::{division_by_zero,ordered_field}) <= b

  1902     ==> c <= 0 ==> b / c <= a / c"

  1903 apply (drule divide_right_mono [of _ _ "- c"])

  1904 apply auto

  1905 done

  1906

  1907 lemma divide_strict_right_mono_neg:

  1908      "[|b < a; c < 0|] ==> a / c < b / (c::'a::ordered_field)"

  1909 apply (drule divide_strict_right_mono [of _ _ "-c"], simp)

  1910 apply (simp add: order_less_imp_not_eq nonzero_minus_divide_right [symmetric])

  1911 done

  1912

  1913 text{*The last premise ensures that @{term a} and @{term b}

  1914       have the same sign*}

  1915 lemma divide_strict_left_mono:

  1916   "[|b < a; 0 < c; 0 < a*b|] ==> c / a < c / (b::'a::ordered_field)"

  1917 by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono)

  1918

  1919 lemma divide_left_mono:

  1920   "[|b \<le> a; 0 \<le> c; 0 < a*b|] ==> c / a \<le> c / (b::'a::ordered_field)"

  1921 by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_right_mono)

  1922

  1923 lemma divide_left_mono_neg: "(a::'a::{division_by_zero,ordered_field}) <= b

  1924     ==> c <= 0 ==> 0 < a * b ==> c / a <= c / b"

  1925   apply (drule divide_left_mono [of _ _ "- c"])

  1926   apply (auto simp add: mult_commute)

  1927 done

  1928

  1929 lemma divide_strict_left_mono_neg:

  1930   "[|a < b; c < 0; 0 < a*b|] ==> c / a < c / (b::'a::ordered_field)"

  1931 by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono_neg)

  1932

  1933

  1934 text{*Simplify quotients that are compared with the value 1.*}

  1935

  1936 lemma le_divide_eq_1 [noatp]:

  1937   fixes a :: "'a :: {ordered_field,division_by_zero}"

  1938   shows "(1 \<le> b / a) = ((0 < a & a \<le> b) | (a < 0 & b \<le> a))"

  1939 by (auto simp add: le_divide_eq)

  1940

  1941 lemma divide_le_eq_1 [noatp]:

  1942   fixes a :: "'a :: {ordered_field,division_by_zero}"

  1943   shows "(b / a \<le> 1) = ((0 < a & b \<le> a) | (a < 0 & a \<le> b) | a=0)"

  1944 by (auto simp add: divide_le_eq)

  1945

  1946 lemma less_divide_eq_1 [noatp]:

  1947   fixes a :: "'a :: {ordered_field,division_by_zero}"

  1948   shows "(1 < b / a) = ((0 < a & a < b) | (a < 0 & b < a))"

  1949 by (auto simp add: less_divide_eq)

  1950

  1951 lemma divide_less_eq_1 [noatp]:

  1952   fixes a :: "'a :: {ordered_field,division_by_zero}"

  1953   shows "(b / a < 1) = ((0 < a & b < a) | (a < 0 & a < b) | a=0)"

  1954 by (auto simp add: divide_less_eq)

  1955

  1956

  1957 subsection{*Conditional Simplification Rules: No Case Splits*}

  1958

  1959 lemma le_divide_eq_1_pos [simp,noatp]:

  1960   fixes a :: "'a :: {ordered_field,division_by_zero}"

  1961   shows "0 < a \<Longrightarrow> (1 \<le> b/a) = (a \<le> b)"

  1962 by (auto simp add: le_divide_eq)

  1963

  1964 lemma le_divide_eq_1_neg [simp,noatp]:

  1965   fixes a :: "'a :: {ordered_field,division_by_zero}"

  1966   shows "a < 0 \<Longrightarrow> (1 \<le> b/a) = (b \<le> a)"

  1967 by (auto simp add: le_divide_eq)

  1968

  1969 lemma divide_le_eq_1_pos [simp,noatp]:

  1970   fixes a :: "'a :: {ordered_field,division_by_zero}"

  1971   shows "0 < a \<Longrightarrow> (b/a \<le> 1) = (b \<le> a)"

  1972 by (auto simp add: divide_le_eq)

  1973

  1974 lemma divide_le_eq_1_neg [simp,noatp]:

  1975   fixes a :: "'a :: {ordered_field,division_by_zero}"

  1976   shows "a < 0 \<Longrightarrow> (b/a \<le> 1) = (a \<le> b)"

  1977 by (auto simp add: divide_le_eq)

  1978

  1979 lemma less_divide_eq_1_pos [simp,noatp]:

  1980   fixes a :: "'a :: {ordered_field,division_by_zero}"

  1981   shows "0 < a \<Longrightarrow> (1 < b/a) = (a < b)"

  1982 by (auto simp add: less_divide_eq)

  1983

  1984 lemma less_divide_eq_1_neg [simp,noatp]:

  1985   fixes a :: "'a :: {ordered_field,division_by_zero}"

  1986   shows "a < 0 \<Longrightarrow> (1 < b/a) = (b < a)"

  1987 by (auto simp add: less_divide_eq)

  1988

  1989 lemma divide_less_eq_1_pos [simp,noatp]:

  1990   fixes a :: "'a :: {ordered_field,division_by_zero}"

  1991   shows "0 < a \<Longrightarrow> (b/a < 1) = (b < a)"

  1992 by (auto simp add: divide_less_eq)

  1993

  1994 lemma divide_less_eq_1_neg [simp,noatp]:

  1995   fixes a :: "'a :: {ordered_field,division_by_zero}"

  1996   shows "a < 0 \<Longrightarrow> b/a < 1 <-> a < b"

  1997 by (auto simp add: divide_less_eq)

  1998

  1999 lemma eq_divide_eq_1 [simp,noatp]:

  2000   fixes a :: "'a :: {ordered_field,division_by_zero}"

  2001   shows "(1 = b/a) = ((a \<noteq> 0 & a = b))"

  2002 by (auto simp add: eq_divide_eq)

  2003

  2004 lemma divide_eq_eq_1 [simp,noatp]:

  2005   fixes a :: "'a :: {ordered_field,division_by_zero}"

  2006   shows "(b/a = 1) = ((a \<noteq> 0 & a = b))"

  2007 by (auto simp add: divide_eq_eq)

  2008

  2009

  2010 subsection {* Reasoning about inequalities with division *}

  2011

  2012 lemma mult_right_le_one_le: "0 <= (x::'a::ordered_idom) ==> 0 <= y ==> y <= 1

  2013     ==> x * y <= x"

  2014 by (auto simp add: mult_compare_simps);

  2015

  2016 lemma mult_left_le_one_le: "0 <= (x::'a::ordered_idom) ==> 0 <= y ==> y <= 1

  2017     ==> y * x <= x"

  2018 by (auto simp add: mult_compare_simps);

  2019

  2020 lemma mult_imp_div_pos_le: "0 < (y::'a::ordered_field) ==> x <= z * y ==>

  2021     x / y <= z";

  2022 by (subst pos_divide_le_eq, assumption+);

  2023

  2024 lemma mult_imp_le_div_pos: "0 < (y::'a::ordered_field) ==> z * y <= x ==>

  2025     z <= x / y"

  2026 by(simp add:field_simps)

  2027

  2028 lemma mult_imp_div_pos_less: "0 < (y::'a::ordered_field) ==> x < z * y ==>

  2029     x / y < z"

  2030 by(simp add:field_simps)

  2031

  2032 lemma mult_imp_less_div_pos: "0 < (y::'a::ordered_field) ==> z * y < x ==>

  2033     z < x / y"

  2034 by(simp add:field_simps)

  2035

  2036 lemma frac_le: "(0::'a::ordered_field) <= x ==>

  2037     x <= y ==> 0 < w ==> w <= z  ==> x / z <= y / w"

  2038   apply (rule mult_imp_div_pos_le)

  2039   apply simp

  2040   apply (subst times_divide_eq_left)

  2041   apply (rule mult_imp_le_div_pos, assumption)

  2042   apply (rule mult_mono)

  2043   apply simp_all

  2044 done

  2045

  2046 lemma frac_less: "(0::'a::ordered_field) <= x ==>

  2047     x < y ==> 0 < w ==> w <= z  ==> x / z < y / w"

  2048   apply (rule mult_imp_div_pos_less)

  2049   apply simp;

  2050   apply (subst times_divide_eq_left);

  2051   apply (rule mult_imp_less_div_pos, assumption)

  2052   apply (erule mult_less_le_imp_less)

  2053   apply simp_all

  2054 done

  2055

  2056 lemma frac_less2: "(0::'a::ordered_field) < x ==>

  2057     x <= y ==> 0 < w ==> w < z  ==> x / z < y / w"

  2058   apply (rule mult_imp_div_pos_less)

  2059   apply simp_all

  2060   apply (subst times_divide_eq_left);

  2061   apply (rule mult_imp_less_div_pos, assumption)

  2062   apply (erule mult_le_less_imp_less)

  2063   apply simp_all

  2064 done

  2065

  2066 text{*It's not obvious whether these should be simprules or not.

  2067   Their effect is to gather terms into one big fraction, like

  2068   a*b*c / x*y*z. The rationale for that is unclear, but many proofs

  2069   seem to need them.*}

  2070

  2071 declare times_divide_eq [simp]

  2072

  2073

  2074 subsection {* Ordered Fields are Dense *}

  2075

  2076 context ordered_semidom

  2077 begin

  2078

  2079 lemma less_add_one: "a < a + 1"

  2080 proof -

  2081   have "a + 0 < a + 1"

  2082     by (blast intro: zero_less_one add_strict_left_mono)

  2083   thus ?thesis by simp

  2084 qed

  2085

  2086 lemma zero_less_two: "0 < 1 + 1"

  2087 by (blast intro: less_trans zero_less_one less_add_one)

  2088

  2089 end

  2090

  2091 lemma less_half_sum: "a < b ==> a < (a+b) / (1+1::'a::ordered_field)"

  2092 by (simp add: field_simps zero_less_two)

  2093

  2094 lemma gt_half_sum: "a < b ==> (a+b)/(1+1::'a::ordered_field) < b"

  2095 by (simp add: field_simps zero_less_two)

  2096

  2097 instance ordered_field < dense_linear_order

  2098 proof

  2099   fix x y :: 'a

  2100   have "x < x + 1" by simp

  2101   then show "\<exists>y. x < y" ..

  2102   have "x - 1 < x" by simp

  2103   then show "\<exists>y. y < x" ..

  2104   show "x < y \<Longrightarrow> \<exists>z>x. z < y" by (blast intro!: less_half_sum gt_half_sum)

  2105 qed

  2106

  2107

  2108 subsection {* Absolute Value *}

  2109

  2110 context ordered_idom

  2111 begin

  2112

  2113 lemma mult_sgn_abs: "sgn x * abs x = x"

  2114   unfolding abs_if sgn_if by auto

  2115

  2116 end

  2117

  2118 lemma abs_one [simp]: "abs 1 = (1::'a::ordered_idom)"

  2119 by (simp add: abs_if zero_less_one [THEN order_less_not_sym])

  2120

  2121 class pordered_ring_abs = pordered_ring + pordered_ab_group_add_abs +

  2122   assumes abs_eq_mult:

  2123     "(0 \<le> a \<or> a \<le> 0) \<and> (0 \<le> b \<or> b \<le> 0) \<Longrightarrow> \<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>"

  2124

  2125

  2126 class lordered_ring = pordered_ring + lordered_ab_group_add_abs

  2127 begin

  2128

  2129 subclass lordered_ab_group_add_meet ..

  2130 subclass lordered_ab_group_add_join ..

  2131

  2132 end

  2133

  2134 lemma abs_le_mult: "abs (a * b) \<le> (abs a) * (abs (b::'a::lordered_ring))"

  2135 proof -

  2136   let ?x = "pprt a * pprt b - pprt a * nprt b - nprt a * pprt b + nprt a * nprt b"

  2137   let ?y = "pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b"

  2138   have a: "(abs a) * (abs b) = ?x"

  2139     by (simp only: abs_prts[of a] abs_prts[of b] algebra_simps)

  2140   {

  2141     fix u v :: 'a

  2142     have bh: "\<lbrakk>u = a; v = b\<rbrakk> \<Longrightarrow>

  2143               u * v = pprt a * pprt b + pprt a * nprt b +

  2144                       nprt a * pprt b + nprt a * nprt b"

  2145       apply (subst prts[of u], subst prts[of v])

  2146       apply (simp add: algebra_simps)

  2147       done

  2148   }

  2149   note b = this[OF refl[of a] refl[of b]]

  2150   note addm = add_mono[of "0::'a" _ "0::'a", simplified]

  2151   note addm2 = add_mono[of _ "0::'a" _ "0::'a", simplified]

  2152   have xy: "- ?x <= ?y"

  2153     apply (simp)

  2154     apply (rule_tac y="0::'a" in order_trans)

  2155     apply (rule addm2)

  2156     apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)

  2157     apply (rule addm)

  2158     apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)

  2159     done

  2160   have yx: "?y <= ?x"

  2161     apply (simp add:diff_def)

  2162     apply (rule_tac y=0 in order_trans)

  2163     apply (rule addm2, (simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)+)

  2164     apply (rule addm, (simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)+)

  2165     done

  2166   have i1: "a*b <= abs a * abs b" by (simp only: a b yx)

  2167   have i2: "- (abs a * abs b) <= a*b" by (simp only: a b xy)

  2168   show ?thesis

  2169     apply (rule abs_leI)

  2170     apply (simp add: i1)

  2171     apply (simp add: i2[simplified minus_le_iff])

  2172     done

  2173 qed

  2174

  2175 instance lordered_ring \<subseteq> pordered_ring_abs

  2176 proof

  2177   fix a b :: "'a\<Colon> lordered_ring"

  2178   assume "(0 \<le> a \<or> a \<le> 0) \<and> (0 \<le> b \<or> b \<le> 0)"

  2179   show "abs (a*b) = abs a * abs b"

  2180 proof -

  2181   have s: "(0 <= a*b) | (a*b <= 0)"

  2182     apply (auto)

  2183     apply (rule_tac split_mult_pos_le)

  2184     apply (rule_tac contrapos_np[of "a*b <= 0"])

  2185     apply (simp)

  2186     apply (rule_tac split_mult_neg_le)

  2187     apply (insert prems)

  2188     apply (blast)

  2189     done

  2190   have mulprts: "a * b = (pprt a + nprt a) * (pprt b + nprt b)"

  2191     by (simp add: prts[symmetric])

  2192   show ?thesis

  2193   proof cases

  2194     assume "0 <= a * b"

  2195     then show ?thesis

  2196       apply (simp_all add: mulprts abs_prts)

  2197       apply (insert prems)

  2198       apply (auto simp add:

  2199 	algebra_simps

  2200 	iffD1[OF zero_le_iff_zero_nprt] iffD1[OF le_zero_iff_zero_pprt]

  2201 	iffD1[OF le_zero_iff_pprt_id] iffD1[OF zero_le_iff_nprt_id])

  2202 	apply(drule (1) mult_nonneg_nonpos[of a b], simp)

  2203 	apply(drule (1) mult_nonneg_nonpos2[of b a], simp)

  2204       done

  2205   next

  2206     assume "~(0 <= a*b)"

  2207     with s have "a*b <= 0" by simp

  2208     then show ?thesis

  2209       apply (simp_all add: mulprts abs_prts)

  2210       apply (insert prems)

  2211       apply (auto simp add: algebra_simps)

  2212       apply(drule (1) mult_nonneg_nonneg[of a b],simp)

  2213       apply(drule (1) mult_nonpos_nonpos[of a b],simp)

  2214       done

  2215   qed

  2216 qed

  2217 qed

  2218

  2219 instance ordered_idom \<subseteq> pordered_ring_abs

  2220 by default (auto simp add: abs_if not_less

  2221   equal_neg_zero neg_equal_zero mult_less_0_iff)

  2222

  2223 lemma abs_mult: "abs (a * b) = abs a * abs (b::'a::ordered_idom)"

  2224 by (simp add: abs_eq_mult linorder_linear)

  2225

  2226 lemma abs_mult_self: "abs a * abs a = a * (a::'a::ordered_idom)"

  2227 by (simp add: abs_if)

  2228

  2229 lemma nonzero_abs_inverse:

  2230      "a \<noteq> 0 ==> abs (inverse (a::'a::ordered_field)) = inverse (abs a)"

  2231 apply (auto simp add: linorder_neq_iff abs_if nonzero_inverse_minus_eq

  2232                       negative_imp_inverse_negative)

  2233 apply (blast intro: positive_imp_inverse_positive elim: order_less_asym)

  2234 done

  2235

  2236 lemma abs_inverse [simp]:

  2237      "abs (inverse (a::'a::{ordered_field,division_by_zero})) =

  2238       inverse (abs a)"

  2239 apply (cases "a=0", simp)

  2240 apply (simp add: nonzero_abs_inverse)

  2241 done

  2242

  2243 lemma nonzero_abs_divide:

  2244      "b \<noteq> 0 ==> abs (a / (b::'a::ordered_field)) = abs a / abs b"

  2245 by (simp add: divide_inverse abs_mult nonzero_abs_inverse)

  2246

  2247 lemma abs_divide [simp]:

  2248      "abs (a / (b::'a::{ordered_field,division_by_zero})) = abs a / abs b"

  2249 apply (cases "b=0", simp)

  2250 apply (simp add: nonzero_abs_divide)

  2251 done

  2252

  2253 lemma abs_mult_less:

  2254      "[| abs a < c; abs b < d |] ==> abs a * abs b < c*(d::'a::ordered_idom)"

  2255 proof -

  2256   assume ac: "abs a < c"

  2257   hence cpos: "0<c" by (blast intro: order_le_less_trans abs_ge_zero)

  2258   assume "abs b < d"

  2259   thus ?thesis by (simp add: ac cpos mult_strict_mono)

  2260 qed

  2261

  2262 lemmas eq_minus_self_iff[noatp] = equal_neg_zero

  2263

  2264 lemma less_minus_self_iff: "(a < -a) = (a < (0::'a::ordered_idom))"

  2265   unfolding order_less_le less_eq_neg_nonpos equal_neg_zero ..

  2266

  2267 lemma abs_less_iff: "(abs a < b) = (a < b & -a < (b::'a::ordered_idom))"

  2268 apply (simp add: order_less_le abs_le_iff)

  2269 apply (auto simp add: abs_if neg_less_eq_nonneg less_eq_neg_nonpos)

  2270 done

  2271

  2272 lemma abs_mult_pos: "(0::'a::ordered_idom) <= x ==>

  2273     (abs y) * x = abs (y * x)"

  2274   apply (subst abs_mult)

  2275   apply simp

  2276 done

  2277

  2278 lemma abs_div_pos: "(0::'a::{division_by_zero,ordered_field}) < y ==>

  2279     abs x / y = abs (x / y)"

  2280   apply (subst abs_divide)

  2281   apply (simp add: order_less_imp_le)

  2282 done

  2283

  2284

  2285 subsection {* Bounds of products via negative and positive Part *}

  2286

  2287 lemma mult_le_prts:

  2288   assumes

  2289   "a1 <= (a::'a::lordered_ring)"

  2290   "a <= a2"

  2291   "b1 <= b"

  2292   "b <= b2"

  2293   shows

  2294   "a * b <= pprt a2 * pprt b2 + pprt a1 * nprt b2 + nprt a2 * pprt b1 + nprt a1 * nprt b1"

  2295 proof -

  2296   have "a * b = (pprt a + nprt a) * (pprt b + nprt b)"

  2297     apply (subst prts[symmetric])+

  2298     apply simp

  2299     done

  2300   then have "a * b = pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b"

  2301     by (simp add: algebra_simps)

  2302   moreover have "pprt a * pprt b <= pprt a2 * pprt b2"

  2303     by (simp_all add: prems mult_mono)

  2304   moreover have "pprt a * nprt b <= pprt a1 * nprt b2"

  2305   proof -

  2306     have "pprt a * nprt b <= pprt a * nprt b2"

  2307       by (simp add: mult_left_mono prems)

  2308     moreover have "pprt a * nprt b2 <= pprt a1 * nprt b2"

  2309       by (simp add: mult_right_mono_neg prems)

  2310     ultimately show ?thesis

  2311       by simp

  2312   qed

  2313   moreover have "nprt a * pprt b <= nprt a2 * pprt b1"

  2314   proof -

  2315     have "nprt a * pprt b <= nprt a2 * pprt b"

  2316       by (simp add: mult_right_mono prems)

  2317     moreover have "nprt a2 * pprt b <= nprt a2 * pprt b1"

  2318       by (simp add: mult_left_mono_neg prems)

  2319     ultimately show ?thesis

  2320       by simp

  2321   qed

  2322   moreover have "nprt a * nprt b <= nprt a1 * nprt b1"

  2323   proof -

  2324     have "nprt a * nprt b <= nprt a * nprt b1"

  2325       by (simp add: mult_left_mono_neg prems)

  2326     moreover have "nprt a * nprt b1 <= nprt a1 * nprt b1"

  2327       by (simp add: mult_right_mono_neg prems)

  2328     ultimately show ?thesis

  2329       by simp

  2330   qed

  2331   ultimately show ?thesis

  2332     by - (rule add_mono | simp)+

  2333 qed

  2334

  2335 lemma mult_ge_prts:

  2336   assumes

  2337   "a1 <= (a::'a::lordered_ring)"

  2338   "a <= a2"

  2339   "b1 <= b"

  2340   "b <= b2"

  2341   shows

  2342   "a * b >= nprt a1 * pprt b2 + nprt a2 * nprt b2 + pprt a1 * pprt b1 + pprt a2 * nprt b1"

  2343 proof -

  2344   from prems have a1:"- a2 <= -a" by auto

  2345   from prems have a2: "-a <= -a1" by auto

  2346   from mult_le_prts[of "-a2" "-a" "-a1" "b1" b "b2", OF a1 a2 prems(3) prems(4), simplified nprt_neg pprt_neg]

  2347   have le: "- (a * b) <= - nprt a1 * pprt b2 + - nprt a2 * nprt b2 + - pprt a1 * pprt b1 + - pprt a2 * nprt b1" by simp

  2348   then have "-(- nprt a1 * pprt b2 + - nprt a2 * nprt b2 + - pprt a1 * pprt b1 + - pprt a2 * nprt b1) <= a * b"

  2349     by (simp only: minus_le_iff)

  2350   then show ?thesis by simp

  2351 qed

  2352

  2353 end