src/HOL/Ring_and_Field.thy
 author nipkow Fri Aug 28 18:52:41 2009 +0200 (2009-08-28) changeset 32436 10cd49e0c067 parent 30961 541bfff659af child 32960 69916a850301 permissions -rw-r--r--
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
     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 text{*There is no slick version using division by zero.*}

   540 lemma inverse_add:

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

   542    ==> inverse a + inverse b = (a + b) * inverse a * inverse b"

   543 by (simp add: division_ring_inverse_add mult_ac)

   544

   545 lemma nonzero_mult_divide_mult_cancel_left [simp, noatp]:

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

   547 proof -

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

   549     by (simp add: divide_inverse nonzero_inverse_mult_distrib)

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

   551     by (simp only: mult_ac)

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

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

   554 qed

   555

   556 lemma nonzero_mult_divide_mult_cancel_right [simp, noatp]:

   557   "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (a * c) / (b * c) = a / b"

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

   559

   560 lemma divide_1 [simp]: "a / 1 = a"

   561 by (simp add: divide_inverse)

   562

   563 lemma times_divide_eq_right: "a * (b / c) = (a * b) / c"

   564 by (simp add: divide_inverse mult_assoc)

   565

   566 lemma times_divide_eq_left: "(b / c) * a = (b * a) / c"

   567 by (simp add: divide_inverse mult_ac)

   568

   569 text {* These are later declared as simp rules. *}

   570 lemmas times_divide_eq [noatp] = times_divide_eq_right times_divide_eq_left

   571

   572 lemma add_frac_eq:

   573   assumes "y \<noteq> 0" and "z \<noteq> 0"

   574   shows "x / y + w / z = (x * z + w * y) / (y * z)"

   575 proof -

   576   have "x / y + w / z = (x * z) / (y * z) + (y * w) / (y * z)"

   577     using assms by simp

   578   also have "\<dots> = (x * z + y * w) / (y * z)"

   579     by (simp only: add_divide_distrib)

   580   finally show ?thesis

   581     by (simp only: mult_commute)

   582 qed

   583

   584 text{*Special Cancellation Simprules for Division*}

   585

   586 lemma nonzero_mult_divide_cancel_right [simp, noatp]:

   587   "b \<noteq> 0 \<Longrightarrow> a * b / b = a"

   588 using nonzero_mult_divide_mult_cancel_right [of 1 b a] by simp

   589

   590 lemma nonzero_mult_divide_cancel_left [simp, noatp]:

   591   "a \<noteq> 0 \<Longrightarrow> a * b / a = b"

   592 using nonzero_mult_divide_mult_cancel_left [of 1 a b] by simp

   593

   594 lemma nonzero_divide_mult_cancel_right [simp, noatp]:

   595   "\<lbrakk>a \<noteq> 0; b \<noteq> 0\<rbrakk> \<Longrightarrow> b / (a * b) = 1 / a"

   596 using nonzero_mult_divide_mult_cancel_right [of a b 1] by simp

   597

   598 lemma nonzero_divide_mult_cancel_left [simp, noatp]:

   599   "\<lbrakk>a \<noteq> 0; b \<noteq> 0\<rbrakk> \<Longrightarrow> a / (a * b) = 1 / b"

   600 using nonzero_mult_divide_mult_cancel_left [of b a 1] by simp

   601

   602 lemma nonzero_mult_divide_mult_cancel_left2 [simp, noatp]:

   603   "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (c * a) / (b * c) = a / b"

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

   605

   606 lemma nonzero_mult_divide_mult_cancel_right2 [simp, noatp]:

   607   "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (a * c) / (c * b) = a / b"

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

   609

   610 lemma minus_divide_left: "- (a / b) = (-a) / b"

   611 by (simp add: divide_inverse)

   612

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

   614 by (simp add: divide_inverse nonzero_inverse_minus_eq)

   615

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

   617 by (simp add: divide_inverse nonzero_inverse_minus_eq)

   618

   619 lemma divide_minus_left [simp, noatp]: "(-a) / b = - (a / b)"

   620 by (simp add: divide_inverse)

   621

   622 lemma diff_divide_distrib: "(a - b) / c = a / c - b / c"

   623 by (simp add: diff_minus add_divide_distrib)

   624

   625 lemma add_divide_eq_iff:

   626   "z \<noteq> 0 \<Longrightarrow> x + y / z = (z * x + y) / z"

   627 by (simp add: add_divide_distrib)

   628

   629 lemma divide_add_eq_iff:

   630   "z \<noteq> 0 \<Longrightarrow> x / z + y = (x + z * y) / z"

   631 by (simp add: add_divide_distrib)

   632

   633 lemma diff_divide_eq_iff:

   634   "z \<noteq> 0 \<Longrightarrow> x - y / z = (z * x - y) / z"

   635 by (simp add: diff_divide_distrib)

   636

   637 lemma divide_diff_eq_iff:

   638   "z \<noteq> 0 \<Longrightarrow> x / z - y = (x - z * y) / z"

   639 by (simp add: diff_divide_distrib)

   640

   641 lemma nonzero_eq_divide_eq: "c \<noteq> 0 \<Longrightarrow> a = b / c \<longleftrightarrow> a * c = b"

   642 proof -

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

   644   have "a = b / c \<longleftrightarrow> a * c = (b / c) * c" by simp

   645   also have "... \<longleftrightarrow> a * c = b" by (simp add: divide_inverse mult_assoc)

   646   finally show ?thesis .

   647 qed

   648

   649 lemma nonzero_divide_eq_eq: "c \<noteq> 0 \<Longrightarrow> b / c = a \<longleftrightarrow> b = a * c"

   650 proof -

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

   652   have "b / c = a \<longleftrightarrow> (b / c) * c = a * c" by simp

   653   also have "... \<longleftrightarrow> b = a * c" by (simp add: divide_inverse mult_assoc)

   654   finally show ?thesis .

   655 qed

   656

   657 lemma divide_eq_imp: "c \<noteq> 0 \<Longrightarrow> b = a * c \<Longrightarrow> b / c = a"

   658 by simp

   659

   660 lemma eq_divide_imp: "c \<noteq> 0 \<Longrightarrow> a * c = b \<Longrightarrow> a = b / c"

   661 by (erule subst, simp)

   662

   663 lemmas field_eq_simps[noatp] = algebra_simps

   664   (* pull / out*)

   665   add_divide_eq_iff divide_add_eq_iff

   666   diff_divide_eq_iff divide_diff_eq_iff

   667   (* multiply eqn *)

   668   nonzero_eq_divide_eq nonzero_divide_eq_eq

   669 (* is added later:

   670   times_divide_eq_left times_divide_eq_right

   671 *)

   672

   673 text{*An example:*}

   674 lemma "\<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"

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

   676  apply(simp add:field_eq_simps)

   677 apply(simp)

   678 done

   679

   680 lemma diff_frac_eq:

   681   "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> x / y - w / z = (x * z - w * y) / (y * z)"

   682 by (simp add: field_eq_simps times_divide_eq)

   683

   684 lemma frac_eq_eq:

   685   "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> (x / y = w / z) = (x * z = w * y)"

   686 by (simp add: field_eq_simps times_divide_eq)

   687

   688 end

   689

   690 class division_by_zero = zero + inverse +

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

   692

   693 lemma divide_zero [simp]:

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

   695 by (simp add: divide_inverse)

   696

   697 lemma divide_self_if [simp]:

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

   699 by simp

   700

   701 class mult_mono = times + zero + ord +

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

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

   704

   705 class pordered_semiring = mult_mono + semiring_0 + pordered_ab_semigroup_add

   706 begin

   707

   708 lemma mult_mono:

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

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

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

   712 apply (erule mult_left_mono, assumption)

   713 done

   714

   715 lemma mult_mono':

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

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

   718 apply (rule mult_mono)

   719 apply (fast intro: order_trans)+

   720 done

   721

   722 end

   723

   724 class pordered_cancel_semiring = mult_mono + pordered_ab_semigroup_add

   725   + semiring + cancel_comm_monoid_add

   726 begin

   727

   728 subclass semiring_0_cancel ..

   729 subclass pordered_semiring ..

   730

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

   732 using mult_left_mono [of zero b a] by simp

   733

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

   735 using mult_left_mono [of b zero a] by simp

   736

   737 lemma mult_nonpos_nonneg: "a \<le> 0 \<Longrightarrow> 0 \<le> b \<Longrightarrow> a * b \<le> 0"

   738 using mult_right_mono [of a zero b] by simp

   739

   740 text {* Legacy - use @{text mult_nonpos_nonneg} *}

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

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

   743

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

   745 by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)

   746

   747 end

   748

   749 class ordered_semiring = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add + mult_mono

   750 begin

   751

   752 subclass pordered_cancel_semiring ..

   753

   754 subclass pordered_comm_monoid_add ..

   755

   756 lemma mult_left_less_imp_less:

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

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

   759

   760 lemma mult_right_less_imp_less:

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

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

   763

   764 end

   765

   766 class ordered_semiring_strict = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add +

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

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

   769 begin

   770

   771 subclass semiring_0_cancel ..

   772

   773 subclass ordered_semiring

   774 proof

   775   fix a b c :: 'a

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

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

   778     unfolding le_less

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

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

   781     unfolding le_less

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

   783 qed

   784

   785 lemma mult_left_le_imp_le:

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

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

   788

   789 lemma mult_right_le_imp_le:

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

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

   792

   793 lemma mult_pos_pos: "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a * b"

   794 using mult_strict_left_mono [of zero b a] by simp

   795

   796 lemma mult_pos_neg: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> a * b < 0"

   797 using mult_strict_left_mono [of b zero a] by simp

   798

   799 lemma mult_neg_pos: "a < 0 \<Longrightarrow> 0 < b \<Longrightarrow> a * b < 0"

   800 using mult_strict_right_mono [of a zero b] by simp

   801

   802 text {* Legacy - use @{text mult_neg_pos} *}

   803 lemma mult_pos_neg2: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> b * a < 0"

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

   805

   806 lemma zero_less_mult_pos:

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

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

   809  apply (auto simp add: le_less not_less)

   810 apply (drule_tac mult_pos_neg [of a b])

   811  apply (auto dest: less_not_sym)

   812 done

   813

   814 lemma zero_less_mult_pos2:

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

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

   817  apply (auto simp add: le_less not_less)

   818 apply (drule_tac mult_pos_neg2 [of a b])

   819  apply (auto dest: less_not_sym)

   820 done

   821

   822 text{*Strict monotonicity in both arguments*}

   823 lemma mult_strict_mono:

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

   825   shows "a * c < b * d"

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

   827   apply (simp add: mult_pos_pos)

   828   apply (erule mult_strict_right_mono [THEN less_trans])

   829   apply (force simp add: le_less)

   830   apply (erule mult_strict_left_mono, assumption)

   831   done

   832

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

   834 lemma mult_strict_mono':

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

   836   shows "a * c < b * d"

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

   838

   839 lemma mult_less_le_imp_less:

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

   841   shows "a * c < b * d"

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

   843   apply (erule less_le_trans)

   844   apply (erule mult_left_mono)

   845   apply simp

   846   apply (erule mult_strict_right_mono)

   847   apply assumption

   848   done

   849

   850 lemma mult_le_less_imp_less:

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

   852   shows "a * c < b * d"

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

   854   apply (erule le_less_trans)

   855   apply (erule mult_strict_left_mono)

   856   apply simp

   857   apply (erule mult_right_mono)

   858   apply simp

   859   done

   860

   861 lemma mult_less_imp_less_left:

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

   863   shows "a < b"

   864 proof (rule ccontr)

   865   assume "\<not>  a < b"

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

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

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

   869 qed

   870

   871 lemma mult_less_imp_less_right:

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

   873   shows "a < b"

   874 proof (rule ccontr)

   875   assume "\<not> a < b"

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

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

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

   879 qed

   880

   881 end

   882

   883 class mult_mono1 = times + zero + ord +

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

   885

   886 class pordered_comm_semiring = comm_semiring_0

   887   + pordered_ab_semigroup_add + mult_mono1

   888 begin

   889

   890 subclass pordered_semiring

   891 proof

   892   fix a b c :: 'a

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

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

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

   896 qed

   897

   898 end

   899

   900 class pordered_cancel_comm_semiring = comm_semiring_0_cancel

   901   + pordered_ab_semigroup_add + mult_mono1

   902 begin

   903

   904 subclass pordered_comm_semiring ..

   905 subclass pordered_cancel_semiring ..

   906

   907 end

   908

   909 class ordered_comm_semiring_strict = comm_semiring_0 + ordered_cancel_ab_semigroup_add +

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

   911 begin

   912

   913 subclass ordered_semiring_strict

   914 proof

   915   fix a b c :: 'a

   916   assume "a < b" "0 < c"

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

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

   919 qed

   920

   921 subclass pordered_cancel_comm_semiring

   922 proof

   923   fix a b c :: 'a

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

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

   926     unfolding le_less

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

   928 qed

   929

   930 end

   931

   932 class pordered_ring = ring + pordered_cancel_semiring

   933 begin

   934

   935 subclass pordered_ab_group_add ..

   936

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

   938 lemmas ring_simps[noatp] = algebra_simps

   939

   940 lemma less_add_iff1:

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

   942 by (simp add: algebra_simps)

   943

   944 lemma less_add_iff2:

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

   946 by (simp add: algebra_simps)

   947

   948 lemma le_add_iff1:

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

   950 by (simp add: algebra_simps)

   951

   952 lemma le_add_iff2:

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

   954 by (simp add: algebra_simps)

   955

   956 lemma mult_left_mono_neg:

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

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

   959   apply (simp_all add: minus_mult_left [symmetric])

   960   done

   961

   962 lemma mult_right_mono_neg:

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

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

   965   apply (simp_all add: minus_mult_right [symmetric])

   966   done

   967

   968 lemma mult_nonpos_nonpos: "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> 0 \<le> a * b"

   969 using mult_right_mono_neg [of a zero b] by simp

   970

   971 lemma split_mult_pos_le:

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

   973 by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)

   974

   975 end

   976

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

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

   979

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

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

   982

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

   984 by(simp add:sgn_if)

   985

   986 class ordered_ring = ring + ordered_semiring

   987   + ordered_ab_group_add + abs_if

   988 begin

   989

   990 subclass pordered_ring ..

   991

   992 subclass pordered_ab_group_add_abs

   993 proof

   994   fix a b

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

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

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

   998      neg_less_eq_nonneg less_eq_neg_nonpos, auto intro: add_nonneg_nonneg,

   999       auto intro!: less_imp_le add_neg_neg)

  1000 qed (auto simp add: abs_if less_eq_neg_nonpos neg_equal_zero)

  1001

  1002 end

  1003

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

  1005    Basically, ordered_ring + no_zero_divisors = ordered_ring_strict.

  1006  *)

  1007 class ordered_ring_strict = ring + ordered_semiring_strict

  1008   + ordered_ab_group_add + abs_if

  1009 begin

  1010

  1011 subclass ordered_ring ..

  1012

  1013 lemma mult_strict_left_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> c * a < c * b"

  1014 using mult_strict_left_mono [of b a "- c"] by simp

  1015

  1016 lemma mult_strict_right_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> a * c < b * c"

  1017 using mult_strict_right_mono [of b a "- c"] by simp

  1018

  1019 lemma mult_neg_neg: "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> 0 < a * b"

  1020 using mult_strict_right_mono_neg [of a zero b] by simp

  1021

  1022 subclass ring_no_zero_divisors

  1023 proof

  1024   fix a b

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

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

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

  1028   proof (cases "a < 0")

  1029     case True note A' = this

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

  1031       case True with A'

  1032       show ?thesis by (auto dest: mult_neg_neg)

  1033     next

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

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

  1036     qed

  1037   next

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

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

  1040       case True with A'

  1041       show ?thesis by (auto dest: mult_strict_right_mono_neg)

  1042     next

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

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

  1045     qed

  1046   qed

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

  1048 qed

  1049

  1050 lemma zero_less_mult_iff:

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

  1052   apply (auto simp add: mult_pos_pos mult_neg_neg)

  1053   apply (simp_all add: not_less le_less)

  1054   apply (erule disjE) apply assumption defer

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

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

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

  1058   apply (drule sym) apply simp

  1059   apply (blast dest: zero_less_mult_pos)

  1060   apply (blast dest: zero_less_mult_pos2)

  1061   done

  1062

  1063 lemma zero_le_mult_iff:

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

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

  1066

  1067 lemma mult_less_0_iff:

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

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

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

  1071   done

  1072

  1073 lemma mult_le_0_iff:

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

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

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

  1077   done

  1078

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

  1080 by (simp add: zero_le_mult_iff linear)

  1081

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

  1083 by (simp add: not_less)

  1084

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

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

  1087

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

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

  1090

  1091 lemma mult_less_cancel_right_disj:

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

  1093   apply (cases "c = 0")

  1094   apply (auto simp add: neq_iff mult_strict_right_mono

  1095                       mult_strict_right_mono_neg)

  1096   apply (auto simp add: not_less

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

  1098                       not_le [symmetric, of a])

  1099   apply (erule_tac [!] notE)

  1100   apply (auto simp add: less_imp_le mult_right_mono

  1101                       mult_right_mono_neg)

  1102   done

  1103

  1104 lemma mult_less_cancel_left_disj:

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

  1106   apply (cases "c = 0")

  1107   apply (auto simp add: neq_iff mult_strict_left_mono

  1108                       mult_strict_left_mono_neg)

  1109   apply (auto simp add: not_less

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

  1111                       not_le [symmetric, of a])

  1112   apply (erule_tac [!] notE)

  1113   apply (auto simp add: less_imp_le mult_left_mono

  1114                       mult_left_mono_neg)

  1115   done

  1116

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

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

  1119

  1120 lemma mult_less_cancel_right:

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

  1122   using mult_less_cancel_right_disj [of a c b] by auto

  1123

  1124 lemma mult_less_cancel_left:

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

  1126   using mult_less_cancel_left_disj [of c a b] by auto

  1127

  1128 lemma mult_le_cancel_right:

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

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

  1131

  1132 lemma mult_le_cancel_left:

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

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

  1135

  1136 lemma mult_le_cancel_left_pos:

  1137   "0 < c \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> a \<le> b"

  1138 by (auto simp: mult_le_cancel_left)

  1139

  1140 lemma mult_le_cancel_left_neg:

  1141   "c < 0 \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> b \<le> a"

  1142 by (auto simp: mult_le_cancel_left)

  1143

  1144 lemma mult_less_cancel_left_pos:

  1145   "0 < c \<Longrightarrow> c * a < c * b \<longleftrightarrow> a < b"

  1146 by (auto simp: mult_less_cancel_left)

  1147

  1148 lemma mult_less_cancel_left_neg:

  1149   "c < 0 \<Longrightarrow> c * a < c * b \<longleftrightarrow> b < a"

  1150 by (auto simp: mult_less_cancel_left)

  1151

  1152 end

  1153

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

  1155 lemmas ring_simps[noatp] = algebra_simps

  1156

  1157 lemmas mult_sign_intros =

  1158   mult_nonneg_nonneg mult_nonneg_nonpos

  1159   mult_nonpos_nonneg mult_nonpos_nonpos

  1160   mult_pos_pos mult_pos_neg

  1161   mult_neg_pos mult_neg_neg

  1162

  1163 class pordered_comm_ring = comm_ring + pordered_comm_semiring

  1164 begin

  1165

  1166 subclass pordered_ring ..

  1167 subclass pordered_cancel_comm_semiring ..

  1168

  1169 end

  1170

  1171 class ordered_semidom = comm_semiring_1_cancel + ordered_comm_semiring_strict +

  1172   (*previously ordered_semiring*)

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

  1174 begin

  1175

  1176 lemma pos_add_strict:

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

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

  1179

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

  1181 by (rule zero_less_one [THEN less_imp_le])

  1182

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

  1184 by (simp add: not_le)

  1185

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

  1187 by (simp add: not_less)

  1188

  1189 lemma less_1_mult:

  1190   assumes "1 < m" and "1 < n"

  1191   shows "1 < m * n"

  1192   using assms mult_strict_mono [of 1 m 1 n]

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

  1194

  1195 end

  1196

  1197 class ordered_idom = comm_ring_1 +

  1198   ordered_comm_semiring_strict + ordered_ab_group_add +

  1199   abs_if + sgn_if

  1200   (*previously ordered_ring*)

  1201 begin

  1202

  1203 subclass ordered_ring_strict ..

  1204 subclass pordered_comm_ring ..

  1205 subclass idom ..

  1206

  1207 subclass ordered_semidom

  1208 proof

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

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

  1211 qed

  1212

  1213 lemma linorder_neqE_ordered_idom:

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

  1215   using assms by (rule neqE)

  1216

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

  1218

  1219 lemma mult_le_cancel_right1:

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

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

  1222

  1223 lemma mult_le_cancel_right2:

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

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

  1226

  1227 lemma mult_le_cancel_left1:

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

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

  1230

  1231 lemma mult_le_cancel_left2:

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

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

  1234

  1235 lemma mult_less_cancel_right1:

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

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

  1238

  1239 lemma mult_less_cancel_right2:

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

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

  1242

  1243 lemma mult_less_cancel_left1:

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

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

  1246

  1247 lemma mult_less_cancel_left2:

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

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

  1250

  1251 lemma sgn_sgn [simp]:

  1252   "sgn (sgn a) = sgn a"

  1253 unfolding sgn_if by simp

  1254

  1255 lemma sgn_0_0:

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

  1257 unfolding sgn_if by simp

  1258

  1259 lemma sgn_1_pos:

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

  1261 unfolding sgn_if by (simp add: neg_equal_zero)

  1262

  1263 lemma sgn_1_neg:

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

  1265 unfolding sgn_if by (auto simp add: equal_neg_zero)

  1266

  1267 lemma sgn_pos [simp]:

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

  1269 unfolding sgn_1_pos .

  1270

  1271 lemma sgn_neg [simp]:

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

  1273 unfolding sgn_1_neg .

  1274

  1275 lemma sgn_times:

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

  1277 by (auto simp add: sgn_if zero_less_mult_iff)

  1278

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

  1280 unfolding sgn_if abs_if by auto

  1281

  1282 lemma sgn_greater [simp]:

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

  1284   unfolding sgn_if by auto

  1285

  1286 lemma sgn_less [simp]:

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

  1288   unfolding sgn_if by auto

  1289

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

  1291   by (simp add: abs_if)

  1292

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

  1294   by (simp add: abs_if)

  1295

  1296 end

  1297

  1298 class ordered_field = field + ordered_idom

  1299

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

  1301

  1302 lemmas mult_compare_simps[noatp] =

  1303     mult_le_cancel_right mult_le_cancel_left

  1304     mult_le_cancel_right1 mult_le_cancel_right2

  1305     mult_le_cancel_left1 mult_le_cancel_left2

  1306     mult_less_cancel_right mult_less_cancel_left

  1307     mult_less_cancel_right1 mult_less_cancel_right2

  1308     mult_less_cancel_left1 mult_less_cancel_left2

  1309     mult_cancel_right mult_cancel_left

  1310     mult_cancel_right1 mult_cancel_right2

  1311     mult_cancel_left1 mult_cancel_left2

  1312

  1313 -- {* FIXME continue localization here *}

  1314

  1315 lemma inverse_nonzero_iff_nonzero [simp]:

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

  1317 by (force dest: inverse_zero_imp_zero)

  1318

  1319 lemma inverse_minus_eq [simp]:

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

  1321 proof cases

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

  1323 next

  1324   assume "a\<noteq>0"

  1325   thus ?thesis by (simp add: nonzero_inverse_minus_eq)

  1326 qed

  1327

  1328 lemma inverse_eq_imp_eq:

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

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

  1331  apply (force dest!: inverse_zero_imp_zero

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

  1333 apply (force dest!: nonzero_inverse_eq_imp_eq)

  1334 done

  1335

  1336 lemma inverse_eq_iff_eq [simp]:

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

  1338 by (force dest!: inverse_eq_imp_eq)

  1339

  1340 lemma inverse_inverse_eq [simp]:

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

  1342   proof cases

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

  1344   next

  1345     assume "a\<noteq>0"

  1346     thus ?thesis by (simp add: nonzero_inverse_inverse_eq)

  1347   qed

  1348

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

  1350       the right-hand side.*}

  1351 lemma inverse_mult_distrib [simp]:

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

  1353   proof cases

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

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

  1356   next

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

  1358     thus ?thesis by force

  1359   qed

  1360

  1361 lemma inverse_divide [simp]:

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

  1363 by (simp add: divide_inverse mult_commute)

  1364

  1365

  1366 subsection {* Calculations with fractions *}

  1367

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

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

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

  1371

  1372 lemma mult_divide_mult_cancel_left:

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

  1374 apply (cases "b = 0")

  1375 apply (simp_all add: nonzero_mult_divide_mult_cancel_left)

  1376 done

  1377

  1378 lemma mult_divide_mult_cancel_right:

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

  1380 apply (cases "b = 0")

  1381 apply (simp_all add: nonzero_mult_divide_mult_cancel_right)

  1382 done

  1383

  1384 lemma divide_divide_eq_right [simp,noatp]:

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

  1386 by (simp add: divide_inverse mult_ac)

  1387

  1388 lemma divide_divide_eq_left [simp,noatp]:

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

  1390 by (simp add: divide_inverse mult_assoc)

  1391

  1392

  1393 subsubsection{*Special Cancellation Simprules for Division*}

  1394

  1395 lemma mult_divide_mult_cancel_left_if[simp,noatp]:

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

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

  1398 by (simp add: mult_divide_mult_cancel_left)

  1399

  1400

  1401 subsection {* Division and Unary Minus *}

  1402

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

  1404 by (simp add: divide_inverse)

  1405

  1406 lemma divide_minus_right [simp, noatp]:

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

  1408 by (simp add: divide_inverse)

  1409

  1410 lemma minus_divide_divide:

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

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

  1413 apply (simp add: nonzero_minus_divide_divide)

  1414 done

  1415

  1416 lemma eq_divide_eq:

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

  1418 by (simp add: nonzero_eq_divide_eq)

  1419

  1420 lemma divide_eq_eq:

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

  1422 by (force simp add: nonzero_divide_eq_eq)

  1423

  1424

  1425 subsection {* Ordered Fields *}

  1426

  1427 lemma positive_imp_inverse_positive:

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

  1429 proof -

  1430   have "0 < a * inverse a"

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

  1432   thus "0 < inverse a"

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

  1434 qed

  1435

  1436 lemma negative_imp_inverse_negative:

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

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

  1439     simp add: nonzero_inverse_minus_eq order_less_imp_not_eq)

  1440

  1441 lemma inverse_le_imp_le:

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

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

  1444 proof (rule classical)

  1445   assume "~ b \<le> a"

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

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

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

  1449     by (simp add: apos invle order_less_imp_le mult_left_mono)

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

  1451     by (simp add: bpos order_less_imp_le mult_right_mono)

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

  1453 qed

  1454

  1455 lemma inverse_positive_imp_positive:

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

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

  1458 proof -

  1459   have "0 < inverse (inverse a)"

  1460     using inv_gt_0 by (rule positive_imp_inverse_positive)

  1461   thus "0 < a"

  1462     using nz by (simp add: nonzero_inverse_inverse_eq)

  1463 qed

  1464

  1465 lemma inverse_positive_iff_positive [simp]:

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

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

  1468 apply (blast intro: inverse_positive_imp_positive positive_imp_inverse_positive)

  1469 done

  1470

  1471 lemma inverse_negative_imp_negative:

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

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

  1474 proof -

  1475   have "inverse (inverse a) < 0"

  1476     using inv_less_0 by (rule negative_imp_inverse_negative)

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

  1478 qed

  1479

  1480 lemma inverse_negative_iff_negative [simp]:

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

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

  1483 apply (blast intro: inverse_negative_imp_negative negative_imp_inverse_negative)

  1484 done

  1485

  1486 lemma inverse_nonnegative_iff_nonnegative [simp]:

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

  1488 by (simp add: linorder_not_less [symmetric])

  1489

  1490 lemma inverse_nonpositive_iff_nonpositive [simp]:

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

  1492 by (simp add: linorder_not_less [symmetric])

  1493

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

  1495 proof

  1496   fix x::'a

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

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

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

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

  1501 qed

  1502

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

  1504 proof

  1505   fix x::'a

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

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

  1508   have "1 + x > x" by simp

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

  1510 qed

  1511

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

  1513

  1514 lemma less_imp_inverse_less:

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

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

  1517 proof (rule ccontr)

  1518   assume "~ inverse b < inverse a"

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

  1520   hence "~ (a < b)"

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

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

  1523 qed

  1524

  1525 lemma inverse_less_imp_less:

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

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

  1528 apply (force dest!: inverse_le_imp_le nonzero_inverse_eq_imp_eq)

  1529 done

  1530

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

  1532 lemma inverse_less_iff_less [simp,noatp]:

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

  1534 by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less)

  1535

  1536 lemma le_imp_inverse_le:

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

  1538 by (force simp add: order_le_less less_imp_inverse_less)

  1539

  1540 lemma inverse_le_iff_le [simp,noatp]:

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

  1542 by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le)

  1543

  1544

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

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

  1547 lemma inverse_le_imp_le_neg:

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

  1549 apply (rule classical)

  1550 apply (subgoal_tac "a < 0")

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

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

  1553 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)

  1554 done

  1555

  1556 lemma less_imp_inverse_less_neg:

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

  1558 apply (subgoal_tac "a < 0")

  1559  prefer 2 apply (blast intro: order_less_trans)

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

  1561 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)

  1562 done

  1563

  1564 lemma inverse_less_imp_less_neg:

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

  1566 apply (rule classical)

  1567 apply (subgoal_tac "a < 0")

  1568  prefer 2

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

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

  1571 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)

  1572 done

  1573

  1574 lemma inverse_less_iff_less_neg [simp,noatp]:

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

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

  1577 apply (simp del: inverse_less_iff_less

  1578             add: order_less_imp_not_eq nonzero_inverse_minus_eq)

  1579 done

  1580

  1581 lemma le_imp_inverse_le_neg:

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

  1583 by (force simp add: order_le_less less_imp_inverse_less_neg)

  1584

  1585 lemma inverse_le_iff_le_neg [simp,noatp]:

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

  1587 by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg)

  1588

  1589

  1590 subsection{*Inverses and the Number One*}

  1591

  1592 lemma one_less_inverse_iff:

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

  1594 proof cases

  1595   assume "0 < x"

  1596     with inverse_less_iff_less [OF zero_less_one, of x]

  1597     show ?thesis by simp

  1598 next

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

  1600   have "~ (1 < inverse x)"

  1601   proof

  1602     assume "1 < inverse x"

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

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

  1605     finally show False by auto

  1606   qed

  1607   with notless show ?thesis by simp

  1608 qed

  1609

  1610 lemma inverse_eq_1_iff [simp]:

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

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

  1613

  1614 lemma one_le_inverse_iff:

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

  1616 by (force simp add: order_le_less one_less_inverse_iff zero_less_one

  1617                     eq_commute [of 1])

  1618

  1619 lemma inverse_less_1_iff:

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

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

  1622

  1623 lemma inverse_le_1_iff:

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

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

  1626

  1627

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

  1629

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

  1631 proof -

  1632   assume less: "0<c"

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

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

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

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

  1637   finally show ?thesis .

  1638 qed

  1639

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

  1641 proof -

  1642   assume less: "c<0"

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

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

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

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

  1647   finally show ?thesis .

  1648 qed

  1649

  1650 lemma le_divide_eq:

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

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

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

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

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

  1656 apply (force simp add: pos_le_divide_eq neg_le_divide_eq linorder_neq_iff)

  1657 done

  1658

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

  1660 proof -

  1661   assume less: "0<c"

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

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

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

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

  1666   finally show ?thesis .

  1667 qed

  1668

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

  1670 proof -

  1671   assume less: "c<0"

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

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

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

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

  1676   finally show ?thesis .

  1677 qed

  1678

  1679 lemma divide_le_eq:

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

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

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

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

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

  1685 apply (force simp add: pos_divide_le_eq neg_divide_le_eq linorder_neq_iff)

  1686 done

  1687

  1688 lemma pos_less_divide_eq:

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

  1690 proof -

  1691   assume less: "0<c"

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

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

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

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

  1696   finally show ?thesis .

  1697 qed

  1698

  1699 lemma neg_less_divide_eq:

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

  1701 proof -

  1702   assume less: "c<0"

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

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

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

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

  1707   finally show ?thesis .

  1708 qed

  1709

  1710 lemma less_divide_eq:

  1711   "(a < b/c) =

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

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

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

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

  1716 apply (force simp add: pos_less_divide_eq neg_less_divide_eq linorder_neq_iff)

  1717 done

  1718

  1719 lemma pos_divide_less_eq:

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

  1721 proof -

  1722   assume less: "0<c"

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

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

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

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

  1727   finally show ?thesis .

  1728 qed

  1729

  1730 lemma neg_divide_less_eq:

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

  1732 proof -

  1733   assume less: "c<0"

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

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

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

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

  1738   finally show ?thesis .

  1739 qed

  1740

  1741 lemma divide_less_eq:

  1742   "(b/c < a) =

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

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

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

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

  1747 apply (force simp add: pos_divide_less_eq neg_divide_less_eq linorder_neq_iff)

  1748 done

  1749

  1750

  1751 subsection{*Field simplification*}

  1752

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

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

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

  1756 more benign @{text algebra_simps}. *}

  1757

  1758 lemmas field_simps[noatp] = field_eq_simps

  1759   (* multiply ineqn *)

  1760   pos_divide_less_eq neg_divide_less_eq

  1761   pos_less_divide_eq neg_less_divide_eq

  1762   pos_divide_le_eq neg_divide_le_eq

  1763   pos_le_divide_eq neg_le_divide_eq

  1764

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

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

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

  1768 explosions. *}

  1769

  1770 lemmas sign_simps[noatp] = group_simps

  1771   zero_less_mult_iff  mult_less_0_iff

  1772

  1773 (* Only works once linear arithmetic is installed:

  1774 text{*An example:*}

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

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

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

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

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

  1780  prefer 2 apply(simp add:sign_simps)

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

  1782  prefer 2 apply(simp add:sign_simps)

  1783 apply(simp add:field_simps)

  1784 done

  1785 *)

  1786

  1787

  1788 subsection{*Division and Signs*}

  1789

  1790 lemma zero_less_divide_iff:

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

  1792 by (simp add: divide_inverse zero_less_mult_iff)

  1793

  1794 lemma divide_less_0_iff:

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

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

  1797 by (simp add: divide_inverse mult_less_0_iff)

  1798

  1799 lemma zero_le_divide_iff:

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

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

  1802 by (simp add: divide_inverse zero_le_mult_iff)

  1803

  1804 lemma divide_le_0_iff:

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

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

  1807 by (simp add: divide_inverse mult_le_0_iff)

  1808

  1809 lemma divide_eq_0_iff [simp,noatp]:

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

  1811 by (simp add: divide_inverse)

  1812

  1813 lemma divide_pos_pos:

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

  1815 by(simp add:field_simps)

  1816

  1817

  1818 lemma divide_nonneg_pos:

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

  1820 by(simp add:field_simps)

  1821

  1822 lemma divide_neg_pos:

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

  1824 by(simp add:field_simps)

  1825

  1826 lemma divide_nonpos_pos:

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

  1828 by(simp add:field_simps)

  1829

  1830 lemma divide_pos_neg:

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

  1832 by(simp add:field_simps)

  1833

  1834 lemma divide_nonneg_neg:

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

  1836 by(simp add:field_simps)

  1837

  1838 lemma divide_neg_neg:

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

  1840 by(simp add:field_simps)

  1841

  1842 lemma divide_nonpos_neg:

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

  1844 by(simp add:field_simps)

  1845

  1846

  1847 subsection{*Cancellation Laws for Division*}

  1848

  1849 lemma divide_cancel_right [simp,noatp]:

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

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

  1852 apply (simp add: divide_inverse)

  1853 done

  1854

  1855 lemma divide_cancel_left [simp,noatp]:

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

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

  1858 apply (simp add: divide_inverse)

  1859 done

  1860

  1861

  1862 subsection {* Division and the Number One *}

  1863

  1864 text{*Simplify expressions equated with 1*}

  1865 lemma divide_eq_1_iff [simp,noatp]:

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

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

  1868 apply (simp add: right_inverse_eq)

  1869 done

  1870

  1871 lemma one_eq_divide_iff [simp,noatp]:

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

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

  1874

  1875 lemma zero_eq_1_divide_iff [simp,noatp]:

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

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

  1878 apply (auto simp add: nonzero_eq_divide_eq)

  1879 done

  1880

  1881 lemma one_divide_eq_0_iff [simp,noatp]:

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

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

  1884 apply (insert zero_neq_one [THEN not_sym])

  1885 apply (auto simp add: nonzero_divide_eq_eq)

  1886 done

  1887

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

  1889 lemmas zero_less_divide_1_iff = zero_less_divide_iff [of 1, simplified]

  1890 lemmas divide_less_0_1_iff = divide_less_0_iff [of 1, simplified]

  1891 lemmas zero_le_divide_1_iff = zero_le_divide_iff [of 1, simplified]

  1892 lemmas divide_le_0_1_iff = divide_le_0_iff [of 1, simplified]

  1893

  1894 declare zero_less_divide_1_iff [simp,noatp]

  1895 declare divide_less_0_1_iff [simp,noatp]

  1896 declare zero_le_divide_1_iff [simp,noatp]

  1897 declare divide_le_0_1_iff [simp,noatp]

  1898

  1899

  1900 subsection {* Ordering Rules for Division *}

  1901

  1902 lemma divide_strict_right_mono:

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

  1904 by (simp add: order_less_imp_not_eq2 divide_inverse mult_strict_right_mono

  1905               positive_imp_inverse_positive)

  1906

  1907 lemma divide_right_mono:

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

  1909 by (force simp add: divide_strict_right_mono order_le_less)

  1910

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

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

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

  1914 apply auto

  1915 done

  1916

  1917 lemma divide_strict_right_mono_neg:

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

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

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

  1921 done

  1922

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

  1924       have the same sign*}

  1925 lemma divide_strict_left_mono:

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

  1927 by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono)

  1928

  1929 lemma divide_left_mono:

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

  1931 by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_right_mono)

  1932

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

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

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

  1936   apply (auto simp add: mult_commute)

  1937 done

  1938

  1939 lemma divide_strict_left_mono_neg:

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

  1941 by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono_neg)

  1942

  1943

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

  1945

  1946 lemma le_divide_eq_1 [noatp]:

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

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

  1949 by (auto simp add: le_divide_eq)

  1950

  1951 lemma divide_le_eq_1 [noatp]:

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

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

  1954 by (auto simp add: divide_le_eq)

  1955

  1956 lemma less_divide_eq_1 [noatp]:

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

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

  1959 by (auto simp add: less_divide_eq)

  1960

  1961 lemma divide_less_eq_1 [noatp]:

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

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

  1964 by (auto simp add: divide_less_eq)

  1965

  1966

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

  1968

  1969 lemma le_divide_eq_1_pos [simp,noatp]:

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

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

  1972 by (auto simp add: le_divide_eq)

  1973

  1974 lemma le_divide_eq_1_neg [simp,noatp]:

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

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

  1977 by (auto simp add: le_divide_eq)

  1978

  1979 lemma divide_le_eq_1_pos [simp,noatp]:

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

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

  1982 by (auto simp add: divide_le_eq)

  1983

  1984 lemma divide_le_eq_1_neg [simp,noatp]:

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

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

  1987 by (auto simp add: divide_le_eq)

  1988

  1989 lemma less_divide_eq_1_pos [simp,noatp]:

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

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

  1992 by (auto simp add: less_divide_eq)

  1993

  1994 lemma less_divide_eq_1_neg [simp,noatp]:

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

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

  1997 by (auto simp add: less_divide_eq)

  1998

  1999 lemma divide_less_eq_1_pos [simp,noatp]:

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

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

  2002 by (auto simp add: divide_less_eq)

  2003

  2004 lemma divide_less_eq_1_neg [simp,noatp]:

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

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

  2007 by (auto simp add: divide_less_eq)

  2008

  2009 lemma eq_divide_eq_1 [simp,noatp]:

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

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

  2012 by (auto simp add: eq_divide_eq)

  2013

  2014 lemma divide_eq_eq_1 [simp,noatp]:

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

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

  2017 by (auto simp add: divide_eq_eq)

  2018

  2019

  2020 subsection {* Reasoning about inequalities with division *}

  2021

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

  2023     ==> x * y <= x"

  2024 by (auto simp add: mult_compare_simps);

  2025

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

  2027     ==> y * x <= x"

  2028 by (auto simp add: mult_compare_simps);

  2029

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

  2031     x / y <= z";

  2032 by (subst pos_divide_le_eq, assumption+);

  2033

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

  2035     z <= x / y"

  2036 by(simp add:field_simps)

  2037

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

  2039     x / y < z"

  2040 by(simp add:field_simps)

  2041

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

  2043     z < x / y"

  2044 by(simp add:field_simps)

  2045

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

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

  2048   apply (rule mult_imp_div_pos_le)

  2049   apply simp

  2050   apply (subst times_divide_eq_left)

  2051   apply (rule mult_imp_le_div_pos, assumption)

  2052   apply (rule mult_mono)

  2053   apply simp_all

  2054 done

  2055

  2056 lemma frac_less: "(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;

  2060   apply (subst times_divide_eq_left);

  2061   apply (rule mult_imp_less_div_pos, assumption)

  2062   apply (erule mult_less_le_imp_less)

  2063   apply simp_all

  2064 done

  2065

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

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

  2068   apply (rule mult_imp_div_pos_less)

  2069   apply simp_all

  2070   apply (subst times_divide_eq_left);

  2071   apply (rule mult_imp_less_div_pos, assumption)

  2072   apply (erule mult_le_less_imp_less)

  2073   apply simp_all

  2074 done

  2075

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

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

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

  2079   seem to need them.*}

  2080

  2081 declare times_divide_eq [simp]

  2082

  2083

  2084 subsection {* Ordered Fields are Dense *}

  2085

  2086 context ordered_semidom

  2087 begin

  2088

  2089 lemma less_add_one: "a < a + 1"

  2090 proof -

  2091   have "a + 0 < a + 1"

  2092     by (blast intro: zero_less_one add_strict_left_mono)

  2093   thus ?thesis by simp

  2094 qed

  2095

  2096 lemma zero_less_two: "0 < 1 + 1"

  2097 by (blast intro: less_trans zero_less_one less_add_one)

  2098

  2099 end

  2100

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

  2102 by (simp add: field_simps zero_less_two)

  2103

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

  2105 by (simp add: field_simps zero_less_two)

  2106

  2107 instance ordered_field < dense_linear_order

  2108 proof

  2109   fix x y :: 'a

  2110   have "x < x + 1" by simp

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

  2112   have "x - 1 < x" by simp

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

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

  2115 qed

  2116

  2117

  2118 subsection {* Absolute Value *}

  2119

  2120 context ordered_idom

  2121 begin

  2122

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

  2124   unfolding abs_if sgn_if by auto

  2125

  2126 end

  2127

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

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

  2130

  2131 class pordered_ring_abs = pordered_ring + pordered_ab_group_add_abs +

  2132   assumes abs_eq_mult:

  2133     "(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>"

  2134

  2135

  2136 class lordered_ring = pordered_ring + lordered_ab_group_add_abs

  2137 begin

  2138

  2139 subclass lordered_ab_group_add_meet ..

  2140 subclass lordered_ab_group_add_join ..

  2141

  2142 end

  2143

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

  2145 proof -

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

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

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

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

  2150   {

  2151     fix u v :: 'a

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

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

  2154                       nprt a * pprt b + nprt a * nprt b"

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

  2156       apply (simp add: algebra_simps)

  2157       done

  2158   }

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

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

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

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

  2163     apply (simp)

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

  2165     apply (rule addm2)

  2166     apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)

  2167     apply (rule addm)

  2168     apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)

  2169     done

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

  2171     apply (simp add:diff_def)

  2172     apply (rule_tac y=0 in order_trans)

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

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

  2175     done

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

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

  2178   show ?thesis

  2179     apply (rule abs_leI)

  2180     apply (simp add: i1)

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

  2182     done

  2183 qed

  2184

  2185 instance lordered_ring \<subseteq> pordered_ring_abs

  2186 proof

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

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

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

  2190 proof -

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

  2192     apply (auto)

  2193     apply (rule_tac split_mult_pos_le)

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

  2195     apply (simp)

  2196     apply (rule_tac split_mult_neg_le)

  2197     apply (insert prems)

  2198     apply (blast)

  2199     done

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

  2201     by (simp add: prts[symmetric])

  2202   show ?thesis

  2203   proof cases

  2204     assume "0 <= a * b"

  2205     then show ?thesis

  2206       apply (simp_all add: mulprts abs_prts)

  2207       apply (insert prems)

  2208       apply (auto simp add:

  2209 	algebra_simps

  2210 	iffD1[OF zero_le_iff_zero_nprt] iffD1[OF le_zero_iff_zero_pprt]

  2211 	iffD1[OF le_zero_iff_pprt_id] iffD1[OF zero_le_iff_nprt_id])

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

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

  2214       done

  2215   next

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

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

  2218     then show ?thesis

  2219       apply (simp_all add: mulprts abs_prts)

  2220       apply (insert prems)

  2221       apply (auto simp add: algebra_simps)

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

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

  2224       done

  2225   qed

  2226 qed

  2227 qed

  2228

  2229 context ordered_idom

  2230 begin

  2231

  2232 subclass pordered_ring_abs proof

  2233 qed (auto simp add: abs_if not_less equal_neg_zero neg_equal_zero mult_less_0_iff)

  2234

  2235 lemma abs_mult:

  2236   "abs (a * b) = abs a * abs b"

  2237   by (rule abs_eq_mult) auto

  2238

  2239 lemma abs_mult_self:

  2240   "abs a * abs a = a * a"

  2241   by (simp add: abs_if)

  2242

  2243 end

  2244

  2245 lemma nonzero_abs_inverse:

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

  2247 apply (auto simp add: linorder_neq_iff abs_if nonzero_inverse_minus_eq

  2248                       negative_imp_inverse_negative)

  2249 apply (blast intro: positive_imp_inverse_positive elim: order_less_asym)

  2250 done

  2251

  2252 lemma abs_inverse [simp]:

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

  2254       inverse (abs a)"

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

  2256 apply (simp add: nonzero_abs_inverse)

  2257 done

  2258

  2259 lemma nonzero_abs_divide:

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

  2261 by (simp add: divide_inverse abs_mult nonzero_abs_inverse)

  2262

  2263 lemma abs_divide [simp]:

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

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

  2266 apply (simp add: nonzero_abs_divide)

  2267 done

  2268

  2269 lemma abs_mult_less:

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

  2271 proof -

  2272   assume ac: "abs a < c"

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

  2274   assume "abs b < d"

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

  2276 qed

  2277

  2278 lemmas eq_minus_self_iff[noatp] = equal_neg_zero

  2279

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

  2281   unfolding order_less_le less_eq_neg_nonpos equal_neg_zero ..

  2282

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

  2284 apply (simp add: order_less_le abs_le_iff)

  2285 apply (auto simp add: abs_if neg_less_eq_nonneg less_eq_neg_nonpos)

  2286 done

  2287

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

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

  2290   apply (subst abs_mult)

  2291   apply simp

  2292 done

  2293

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

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

  2296   apply (subst abs_divide)

  2297   apply (simp add: order_less_imp_le)

  2298 done

  2299

  2300

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

  2302

  2303 lemma mult_le_prts:

  2304   assumes

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

  2306   "a <= a2"

  2307   "b1 <= b"

  2308   "b <= b2"

  2309   shows

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

  2311 proof -

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

  2313     apply (subst prts[symmetric])+

  2314     apply simp

  2315     done

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

  2317     by (simp add: algebra_simps)

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

  2319     by (simp_all add: prems mult_mono)

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

  2321   proof -

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

  2323       by (simp add: mult_left_mono prems)

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

  2325       by (simp add: mult_right_mono_neg prems)

  2326     ultimately show ?thesis

  2327       by simp

  2328   qed

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

  2330   proof -

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

  2332       by (simp add: mult_right_mono prems)

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

  2334       by (simp add: mult_left_mono_neg prems)

  2335     ultimately show ?thesis

  2336       by simp

  2337   qed

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

  2339   proof -

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

  2341       by (simp add: mult_left_mono_neg prems)

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

  2343       by (simp add: mult_right_mono_neg prems)

  2344     ultimately show ?thesis

  2345       by simp

  2346   qed

  2347   ultimately show ?thesis

  2348     by - (rule add_mono | simp)+

  2349 qed

  2350

  2351 lemma mult_ge_prts:

  2352   assumes

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

  2354   "a <= a2"

  2355   "b1 <= b"

  2356   "b <= b2"

  2357   shows

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

  2359 proof -

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

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

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

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

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

  2365     by (simp only: minus_le_iff)

  2366   then show ?thesis by simp

  2367 qed

  2368

  2369 end