src/HOL/Ring_and_Field.thy
 author haftmann Mon Feb 08 14:22:22 2010 +0100 (2010-02-08) changeset 35043 07dbdf60d5ad parent 35032 7efe662e41b4 permissions -rw-r--r--
dropped accidental duplication of "lin" prefix from cs. 108662d50512
     1 (*  Title:      HOL/Ring_and_Field.thy

     2     Author:     Gertrud Bauer

     3     Author:     Steven Obua

     4     Author:     Tobias Nipkow

     5     Author:     Lawrence C Paulson

     6     Author:     Markus Wenzel

     7     Author:     Jeremy Avigad

     8 *)

     9

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

    11

    12 theory Ring_and_Field

    13 imports OrderedGroup

    14 begin

    15

    16 text {*

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

    18   \begin{itemize}

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

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

    21   \end{itemize}

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

    23   \begin{itemize}

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

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

    26   \end{itemize}

    27 *}

    28

    29 class semiring = ab_semigroup_add + semigroup_mult +

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

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

    32 begin

    33

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

    35 lemma combine_common_factor:

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

    37 by (simp add: left_distrib add_ac)

    38

    39 end

    40

    41 class mult_zero = times + zero +

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

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

    44

    45 class semiring_0 = semiring + comm_monoid_add + mult_zero

    46

    47 class semiring_0_cancel = semiring + cancel_comm_monoid_add

    48 begin

    49

    50 subclass semiring_0

    51 proof

    52   fix a :: 'a

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

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

    55 next

    56   fix a :: 'a

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

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

    59 qed

    60

    61 end

    62

    63 class comm_semiring = ab_semigroup_add + ab_semigroup_mult +

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

    65 begin

    66

    67 subclass semiring

    68 proof

    69   fix a b c :: 'a

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

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

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

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

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

    75 qed

    76

    77 end

    78

    79 class comm_semiring_0 = comm_semiring + comm_monoid_add + mult_zero

    80 begin

    81

    82 subclass semiring_0 ..

    83

    84 end

    85

    86 class comm_semiring_0_cancel = comm_semiring + cancel_comm_monoid_add

    87 begin

    88

    89 subclass semiring_0_cancel ..

    90

    91 subclass comm_semiring_0 ..

    92

    93 end

    94

    95 class zero_neq_one = zero + one +

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

    97 begin

    98

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

   100 by (rule not_sym) (rule zero_neq_one)

   101

   102 end

   103

   104 class semiring_1 = zero_neq_one + semiring_0 + monoid_mult

   105

   106 text {* Abstract divisibility *}

   107

   108 class dvd = times

   109 begin

   110

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

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

   113

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

   115   unfolding dvd_def ..

   116

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

   118   unfolding dvd_def by blast

   119

   120 end

   121

   122 class comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult + dvd

   123   (*previously almost_semiring*)

   124 begin

   125

   126 subclass semiring_1 ..

   127

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

   129 proof

   130   show "a = a * 1" by simp

   131 qed

   132

   133 lemma dvd_trans:

   134   assumes "a dvd b" and "b dvd c"

   135   shows "a dvd c"

   136 proof -

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

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

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

   140   then show ?thesis ..

   141 qed

   142

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

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

   145

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

   147 proof

   148   show "0 = a * 0" by simp

   149 qed

   150

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

   152 by (auto intro!: dvdI)

   153

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

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

   156

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

   158   apply (subst mult_commute)

   159   apply (erule dvd_mult)

   160   done

   161

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

   163 by (rule dvd_mult) (rule dvd_refl)

   164

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

   166 by (rule dvd_mult2) (rule dvd_refl)

   167

   168 lemma mult_dvd_mono:

   169   assumes "a dvd b"

   170     and "c dvd d"

   171   shows "a * c dvd b * d"

   172 proof -

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

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

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

   176   then show ?thesis ..

   177 qed

   178

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

   180 by (simp add: dvd_def mult_assoc, blast)

   181

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

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

   184

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

   186 by simp

   187

   188 lemma dvd_add[simp]:

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

   190 proof -

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

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

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

   194   then show ?thesis ..

   195 qed

   196

   197 end

   198

   199

   200 class no_zero_divisors = zero + times +

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

   202

   203 class semiring_1_cancel = semiring + cancel_comm_monoid_add

   204   + zero_neq_one + monoid_mult

   205 begin

   206

   207 subclass semiring_0_cancel ..

   208

   209 subclass semiring_1 ..

   210

   211 end

   212

   213 class comm_semiring_1_cancel = comm_semiring + cancel_comm_monoid_add

   214   + zero_neq_one + comm_monoid_mult

   215 begin

   216

   217 subclass semiring_1_cancel ..

   218 subclass comm_semiring_0_cancel ..

   219 subclass comm_semiring_1 ..

   220

   221 end

   222

   223 class ring = semiring + ab_group_add

   224 begin

   225

   226 subclass semiring_0_cancel ..

   227

   228 text {* Distribution rules *}

   229

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

   231 by (rule minus_unique) (simp add: left_distrib [symmetric])

   232

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

   234 by (rule minus_unique) (simp add: right_distrib [symmetric])

   235

   236 text{*Extract signs from products*}

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

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

   239

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

   241 by simp

   242

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

   244 by simp

   245

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

   247 by (simp add: right_distrib diff_minus)

   248

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

   250 by (simp add: left_distrib diff_minus)

   251

   252 lemmas ring_distribs[noatp] =

   253   right_distrib left_distrib left_diff_distrib right_diff_distrib

   254

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

   256 lemmas ring_simps[noatp] = algebra_simps

   257

   258 lemma eq_add_iff1:

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

   260 by (simp add: algebra_simps)

   261

   262 lemma eq_add_iff2:

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

   264 by (simp add: algebra_simps)

   265

   266 end

   267

   268 lemmas ring_distribs[noatp] =

   269   right_distrib left_distrib left_diff_distrib right_diff_distrib

   270

   271 class comm_ring = comm_semiring + ab_group_add

   272 begin

   273

   274 subclass ring ..

   275 subclass comm_semiring_0_cancel ..

   276

   277 end

   278

   279 class ring_1 = ring + zero_neq_one + monoid_mult

   280 begin

   281

   282 subclass semiring_1_cancel ..

   283

   284 end

   285

   286 class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult

   287   (*previously ring*)

   288 begin

   289

   290 subclass ring_1 ..

   291 subclass comm_semiring_1_cancel ..

   292

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

   294 proof

   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 next

   299   assume "x dvd y"

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

   301   then show "x dvd - y" by simp

   302 qed

   303

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

   305 proof

   306   assume "- x dvd y"

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

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

   309   then show "x dvd y" ..

   310 next

   311   assume "x dvd y"

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

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

   314   then show "- x dvd y" ..

   315 qed

   316

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

   318 by (simp add: diff_minus dvd_minus_iff)

   319

   320 end

   321

   322 class ring_no_zero_divisors = ring + no_zero_divisors

   323 begin

   324

   325 lemma mult_eq_0_iff [simp]:

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

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

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

   329     then show ?thesis using no_zero_divisors by simp

   330 next

   331   case True then show ?thesis by auto

   332 qed

   333

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

   335 lemma mult_cancel_right [simp, noatp]:

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

   337 proof -

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

   339     by (simp add: algebra_simps right_minus_eq)

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

   341 qed

   342

   343 lemma mult_cancel_left [simp, noatp]:

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

   345 proof -

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

   347     by (simp add: algebra_simps right_minus_eq)

   348   thus ?thesis by (simp add: right_minus_eq)

   349 qed

   350

   351 end

   352

   353 class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors

   354 begin

   355

   356 lemma mult_cancel_right1 [simp]:

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

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

   359

   360 lemma mult_cancel_right2 [simp]:

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

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

   363

   364 lemma mult_cancel_left1 [simp]:

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

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

   367

   368 lemma mult_cancel_left2 [simp]:

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

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

   371

   372 end

   373

   374 class idom = comm_ring_1 + no_zero_divisors

   375 begin

   376

   377 subclass ring_1_no_zero_divisors ..

   378

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

   380 proof

   381   assume "a * a = b * b"

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

   383     by (simp add: algebra_simps)

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

   385     by (simp add: right_minus_eq eq_neg_iff_add_eq_0)

   386 next

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

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

   389 qed

   390

   391 lemma dvd_mult_cancel_right [simp]:

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

   393 proof -

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

   395     unfolding dvd_def by (simp add: mult_ac)

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

   397     unfolding dvd_def by simp

   398   finally show ?thesis .

   399 qed

   400

   401 lemma dvd_mult_cancel_left [simp]:

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

   403 proof -

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

   405     unfolding dvd_def by (simp add: mult_ac)

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

   407     unfolding dvd_def by simp

   408   finally show ?thesis .

   409 qed

   410

   411 end

   412

   413 class division_ring = ring_1 + inverse +

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

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

   416 begin

   417

   418 subclass ring_1_no_zero_divisors

   419 proof

   420   fix a b :: 'a

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

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

   423   proof

   424     assume ab: "a * b = 0"

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

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

   427       by (simp only: mult_assoc)

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

   429     finally show False by simp

   430   qed

   431 qed

   432

   433 lemma nonzero_imp_inverse_nonzero:

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

   435 proof

   436   assume ianz: "inverse a = 0"

   437   assume "a \<noteq> 0"

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

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

   440   finally have "1 = 0" .

   441   thus False by (simp add: eq_commute)

   442 qed

   443

   444 lemma inverse_zero_imp_zero:

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

   446 apply (rule classical)

   447 apply (drule nonzero_imp_inverse_nonzero)

   448 apply auto

   449 done

   450

   451 lemma inverse_unique:

   452   assumes ab: "a * b = 1"

   453   shows "inverse a = b"

   454 proof -

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

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

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

   458 qed

   459

   460 lemma nonzero_inverse_minus_eq:

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

   462 by (rule inverse_unique) simp

   463

   464 lemma nonzero_inverse_inverse_eq:

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

   466 by (rule inverse_unique) simp

   467

   468 lemma nonzero_inverse_eq_imp_eq:

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

   470   shows "a = b"

   471 proof -

   472   from inverse a = inverse b

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

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

   475     by (simp add: nonzero_inverse_inverse_eq)

   476 qed

   477

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

   479 by (rule inverse_unique) simp

   480

   481 lemma nonzero_inverse_mult_distrib:

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

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

   484 proof -

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

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

   487   thus ?thesis by (rule inverse_unique)

   488 qed

   489

   490 lemma division_ring_inverse_add:

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

   492 by (simp add: algebra_simps)

   493

   494 lemma division_ring_inverse_diff:

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

   496 by (simp add: algebra_simps)

   497

   498 end

   499

   500 class field = comm_ring_1 + inverse +

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

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

   503 begin

   504

   505 subclass division_ring

   506 proof

   507   fix a :: 'a

   508   assume "a \<noteq> 0"

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

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

   511 qed

   512

   513 subclass idom ..

   514

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

   516 proof

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

   518   {

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

   520     also assume "a / b = 1"

   521     finally show "a = b" by simp

   522   next

   523     assume "a = b"

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

   525   }

   526 qed

   527

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

   529 by (simp add: divide_inverse)

   530

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

   532 by (simp add: divide_inverse)

   533

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

   535 by (simp add: divide_inverse)

   536

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

   538 by (simp add: divide_inverse)

   539

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

   541 by (simp add: divide_inverse algebra_simps)

   542

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

   544 lemma inverse_add:

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

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

   547 by (simp add: division_ring_inverse_add mult_ac)

   548

   549 lemma nonzero_mult_divide_mult_cancel_left [simp, noatp]:

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

   551 proof -

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

   553     by (simp add: divide_inverse nonzero_inverse_mult_distrib)

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

   555     by (simp only: mult_ac)

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

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

   558 qed

   559

   560 lemma nonzero_mult_divide_mult_cancel_right [simp, noatp]:

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

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

   563

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

   565 by (simp add: divide_inverse)

   566

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

   568 by (simp add: divide_inverse mult_assoc)

   569

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

   571 by (simp add: divide_inverse mult_ac)

   572

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

   574 lemmas times_divide_eq [noatp] = times_divide_eq_right times_divide_eq_left

   575

   576 lemma add_frac_eq:

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

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

   579 proof -

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

   581     using assms by simp

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

   583     by (simp only: add_divide_distrib)

   584   finally show ?thesis

   585     by (simp only: mult_commute)

   586 qed

   587

   588 text{*Special Cancellation Simprules for Division*}

   589

   590 lemma nonzero_mult_divide_cancel_right [simp, noatp]:

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

   592 using nonzero_mult_divide_mult_cancel_right [of 1 b a] by simp

   593

   594 lemma nonzero_mult_divide_cancel_left [simp, noatp]:

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

   596 using nonzero_mult_divide_mult_cancel_left [of 1 a b] by simp

   597

   598 lemma nonzero_divide_mult_cancel_right [simp, noatp]:

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

   600 using nonzero_mult_divide_mult_cancel_right [of a b 1] by simp

   601

   602 lemma nonzero_divide_mult_cancel_left [simp, noatp]:

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

   604 using nonzero_mult_divide_mult_cancel_left [of b a 1] by simp

   605

   606 lemma nonzero_mult_divide_mult_cancel_left2 [simp, noatp]:

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

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

   609

   610 lemma nonzero_mult_divide_mult_cancel_right2 [simp, noatp]:

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

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

   613

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

   615 by (simp add: divide_inverse)

   616

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

   618 by (simp add: divide_inverse nonzero_inverse_minus_eq)

   619

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

   621 by (simp add: divide_inverse nonzero_inverse_minus_eq)

   622

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

   624 by (simp add: divide_inverse)

   625

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

   627 by (simp add: diff_minus add_divide_distrib)

   628

   629 lemma add_divide_eq_iff:

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

   631 by (simp add: add_divide_distrib)

   632

   633 lemma divide_add_eq_iff:

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

   635 by (simp add: add_divide_distrib)

   636

   637 lemma diff_divide_eq_iff:

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

   639 by (simp add: diff_divide_distrib)

   640

   641 lemma divide_diff_eq_iff:

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

   643 by (simp add: diff_divide_distrib)

   644

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

   646 proof -

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

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

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

   650   finally show ?thesis .

   651 qed

   652

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

   654 proof -

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

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

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

   658   finally show ?thesis .

   659 qed

   660

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

   662 by simp

   663

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

   665 by (erule subst, simp)

   666

   667 lemmas field_eq_simps[noatp] = algebra_simps

   668   (* pull / out*)

   669   add_divide_eq_iff divide_add_eq_iff

   670   diff_divide_eq_iff divide_diff_eq_iff

   671   (* multiply eqn *)

   672   nonzero_eq_divide_eq nonzero_divide_eq_eq

   673 (* is added later:

   674   times_divide_eq_left times_divide_eq_right

   675 *)

   676

   677 text{*An example:*}

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

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

   680  apply(simp add:field_eq_simps)

   681 apply(simp)

   682 done

   683

   684 lemma diff_frac_eq:

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

   686 by (simp add: field_eq_simps times_divide_eq)

   687

   688 lemma frac_eq_eq:

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

   690 by (simp add: field_eq_simps times_divide_eq)

   691

   692 end

   693

   694 class division_by_zero = zero + inverse +

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

   696

   697 lemma divide_zero [simp]:

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

   699 by (simp add: divide_inverse)

   700

   701 lemma divide_self_if [simp]:

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

   703 by simp

   704

   705 class mult_mono = times + zero + ord +

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

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

   708

   709 class ordered_semiring = mult_mono + semiring_0 + ordered_ab_semigroup_add

   710 begin

   711

   712 lemma mult_mono:

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

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

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

   716 apply (erule mult_left_mono, assumption)

   717 done

   718

   719 lemma mult_mono':

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

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

   722 apply (rule mult_mono)

   723 apply (fast intro: order_trans)+

   724 done

   725

   726 end

   727

   728 class ordered_cancel_semiring = mult_mono + ordered_ab_semigroup_add

   729   + semiring + cancel_comm_monoid_add

   730 begin

   731

   732 subclass semiring_0_cancel ..

   733 subclass ordered_semiring ..

   734

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

   736 using mult_left_mono [of zero b a] by simp

   737

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

   739 using mult_left_mono [of b zero a] by simp

   740

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

   742 using mult_right_mono [of a zero b] by simp

   743

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

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

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

   747

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

   749 by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)

   750

   751 end

   752

   753 class linordered_semiring = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add + mult_mono

   754 begin

   755

   756 subclass ordered_cancel_semiring ..

   757

   758 subclass ordered_comm_monoid_add ..

   759

   760 lemma mult_left_less_imp_less:

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

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

   763

   764 lemma mult_right_less_imp_less:

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

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

   767

   768 end

   769

   770 class linordered_semiring_1 = linordered_semiring + semiring_1

   771

   772 class linordered_semiring_strict = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add +

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

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

   775 begin

   776

   777 subclass semiring_0_cancel ..

   778

   779 subclass linordered_semiring

   780 proof

   781   fix a b c :: 'a

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

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

   784     unfolding le_less

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

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

   787     unfolding le_less

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

   789 qed

   790

   791 lemma mult_left_le_imp_le:

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

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

   794

   795 lemma mult_right_le_imp_le:

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

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

   798

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

   800 using mult_strict_left_mono [of zero b a] by simp

   801

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

   803 using mult_strict_left_mono [of b zero a] by simp

   804

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

   806 using mult_strict_right_mono [of a zero b] by simp

   807

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

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

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

   811

   812 lemma zero_less_mult_pos:

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

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

   815  apply (auto simp add: le_less not_less)

   816 apply (drule_tac mult_pos_neg [of a b])

   817  apply (auto dest: less_not_sym)

   818 done

   819

   820 lemma zero_less_mult_pos2:

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

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

   823  apply (auto simp add: le_less not_less)

   824 apply (drule_tac mult_pos_neg2 [of a b])

   825  apply (auto dest: less_not_sym)

   826 done

   827

   828 text{*Strict monotonicity in both arguments*}

   829 lemma mult_strict_mono:

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

   831   shows "a * c < b * d"

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

   833   apply (simp add: mult_pos_pos)

   834   apply (erule mult_strict_right_mono [THEN less_trans])

   835   apply (force simp add: le_less)

   836   apply (erule mult_strict_left_mono, assumption)

   837   done

   838

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

   840 lemma mult_strict_mono':

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

   842   shows "a * c < b * d"

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

   844

   845 lemma mult_less_le_imp_less:

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

   847   shows "a * c < b * d"

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

   849   apply (erule less_le_trans)

   850   apply (erule mult_left_mono)

   851   apply simp

   852   apply (erule mult_strict_right_mono)

   853   apply assumption

   854   done

   855

   856 lemma mult_le_less_imp_less:

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

   858   shows "a * c < b * d"

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

   860   apply (erule le_less_trans)

   861   apply (erule mult_strict_left_mono)

   862   apply simp

   863   apply (erule mult_right_mono)

   864   apply simp

   865   done

   866

   867 lemma mult_less_imp_less_left:

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

   869   shows "a < b"

   870 proof (rule ccontr)

   871   assume "\<not>  a < b"

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

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

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

   875 qed

   876

   877 lemma mult_less_imp_less_right:

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

   879   shows "a < b"

   880 proof (rule ccontr)

   881   assume "\<not> a < b"

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

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

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

   885 qed

   886

   887 end

   888

   889 class linlinordered_semiring_1_strict = linordered_semiring_strict + semiring_1

   890

   891 class mult_mono1 = times + zero + ord +

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

   893

   894 class ordered_comm_semiring = comm_semiring_0

   895   + ordered_ab_semigroup_add + mult_mono1

   896 begin

   897

   898 subclass ordered_semiring

   899 proof

   900   fix a b c :: 'a

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

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

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

   904 qed

   905

   906 end

   907

   908 class ordered_cancel_comm_semiring = comm_semiring_0_cancel

   909   + ordered_ab_semigroup_add + mult_mono1

   910 begin

   911

   912 subclass ordered_comm_semiring ..

   913 subclass ordered_cancel_semiring ..

   914

   915 end

   916

   917 class linordered_comm_semiring_strict = comm_semiring_0 + linordered_cancel_ab_semigroup_add +

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

   919 begin

   920

   921 subclass linordered_semiring_strict

   922 proof

   923   fix a b c :: 'a

   924   assume "a < b" "0 < c"

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

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

   927 qed

   928

   929 subclass ordered_cancel_comm_semiring

   930 proof

   931   fix a b c :: 'a

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

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

   934     unfolding le_less

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

   936 qed

   937

   938 end

   939

   940 class ordered_ring = ring + ordered_cancel_semiring

   941 begin

   942

   943 subclass ordered_ab_group_add ..

   944

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

   946 lemmas ring_simps[noatp] = algebra_simps

   947

   948 lemma less_add_iff1:

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

   950 by (simp add: algebra_simps)

   951

   952 lemma less_add_iff2:

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

   954 by (simp add: algebra_simps)

   955

   956 lemma le_add_iff1:

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

   958 by (simp add: algebra_simps)

   959

   960 lemma le_add_iff2:

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

   962 by (simp add: algebra_simps)

   963

   964 lemma mult_left_mono_neg:

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

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

   967   apply (simp_all add: minus_mult_left [symmetric])

   968   done

   969

   970 lemma mult_right_mono_neg:

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

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

   973   apply (simp_all add: minus_mult_right [symmetric])

   974   done

   975

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

   977 using mult_right_mono_neg [of a zero b] by simp

   978

   979 lemma split_mult_pos_le:

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

   981 by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)

   982

   983 end

   984

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

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

   987

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

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

   990

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

   992 by(simp add:sgn_if)

   993

   994 class linordered_ring = ring + linordered_semiring + linordered_ab_group_add + abs_if

   995 begin

   996

   997 subclass ordered_ring ..

   998

   999 subclass ordered_ab_group_add_abs

  1000 proof

  1001   fix a b

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

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

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

  1005      neg_less_eq_nonneg less_eq_neg_nonpos, auto intro: add_nonneg_nonneg,

  1006       auto intro!: less_imp_le add_neg_neg)

  1007 qed (auto simp add: abs_if less_eq_neg_nonpos neg_equal_zero)

  1008

  1009 end

  1010

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

  1012    Basically, linordered_ring + no_zero_divisors = linordered_ring_strict.

  1013  *)

  1014 class linordered_ring_strict = ring + linordered_semiring_strict

  1015   + ordered_ab_group_add + abs_if

  1016 begin

  1017

  1018 subclass linordered_ring ..

  1019

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

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

  1022

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

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

  1025

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

  1027 using mult_strict_right_mono_neg [of a zero b] by simp

  1028

  1029 subclass ring_no_zero_divisors

  1030 proof

  1031   fix a b

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

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

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

  1035   proof (cases "a < 0")

  1036     case True note A' = this

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

  1038       case True with A'

  1039       show ?thesis by (auto dest: mult_neg_neg)

  1040     next

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

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

  1043     qed

  1044   next

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

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

  1047       case True with A'

  1048       show ?thesis by (auto dest: mult_strict_right_mono_neg)

  1049     next

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

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

  1052     qed

  1053   qed

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

  1055 qed

  1056

  1057 lemma zero_less_mult_iff:

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

  1059   apply (auto simp add: mult_pos_pos mult_neg_neg)

  1060   apply (simp_all add: not_less le_less)

  1061   apply (erule disjE) apply assumption defer

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

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

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

  1065   apply (drule sym) apply simp

  1066   apply (blast dest: zero_less_mult_pos)

  1067   apply (blast dest: zero_less_mult_pos2)

  1068   done

  1069

  1070 lemma zero_le_mult_iff:

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

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

  1073

  1074 lemma mult_less_0_iff:

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

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

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

  1078   done

  1079

  1080 lemma mult_le_0_iff:

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

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

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

  1084   done

  1085

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

  1087 by (simp add: zero_le_mult_iff linear)

  1088

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

  1090 by (simp add: not_less)

  1091

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

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

  1094

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

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

  1097

  1098 lemma mult_less_cancel_right_disj:

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

  1100   apply (cases "c = 0")

  1101   apply (auto simp add: neq_iff mult_strict_right_mono

  1102                       mult_strict_right_mono_neg)

  1103   apply (auto simp add: not_less

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

  1105                       not_le [symmetric, of a])

  1106   apply (erule_tac [!] notE)

  1107   apply (auto simp add: less_imp_le mult_right_mono

  1108                       mult_right_mono_neg)

  1109   done

  1110

  1111 lemma mult_less_cancel_left_disj:

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

  1113   apply (cases "c = 0")

  1114   apply (auto simp add: neq_iff mult_strict_left_mono

  1115                       mult_strict_left_mono_neg)

  1116   apply (auto simp add: not_less

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

  1118                       not_le [symmetric, of a])

  1119   apply (erule_tac [!] notE)

  1120   apply (auto simp add: less_imp_le mult_left_mono

  1121                       mult_left_mono_neg)

  1122   done

  1123

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

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

  1126

  1127 lemma mult_less_cancel_right:

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

  1129   using mult_less_cancel_right_disj [of a c b] by auto

  1130

  1131 lemma mult_less_cancel_left:

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

  1133   using mult_less_cancel_left_disj [of c a b] by auto

  1134

  1135 lemma mult_le_cancel_right:

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

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

  1138

  1139 lemma mult_le_cancel_left:

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

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

  1142

  1143 lemma mult_le_cancel_left_pos:

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

  1145 by (auto simp: mult_le_cancel_left)

  1146

  1147 lemma mult_le_cancel_left_neg:

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

  1149 by (auto simp: mult_le_cancel_left)

  1150

  1151 lemma mult_less_cancel_left_pos:

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

  1153 by (auto simp: mult_less_cancel_left)

  1154

  1155 lemma mult_less_cancel_left_neg:

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

  1157 by (auto simp: mult_less_cancel_left)

  1158

  1159 end

  1160

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

  1162 lemmas ring_simps[noatp] = algebra_simps

  1163

  1164 lemmas mult_sign_intros =

  1165   mult_nonneg_nonneg mult_nonneg_nonpos

  1166   mult_nonpos_nonneg mult_nonpos_nonpos

  1167   mult_pos_pos mult_pos_neg

  1168   mult_neg_pos mult_neg_neg

  1169

  1170 class ordered_comm_ring = comm_ring + ordered_comm_semiring

  1171 begin

  1172

  1173 subclass ordered_ring ..

  1174 subclass ordered_cancel_comm_semiring ..

  1175

  1176 end

  1177

  1178 class linordered_semidom = comm_semiring_1_cancel + linordered_comm_semiring_strict +

  1179   (*previously linordered_semiring*)

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

  1181 begin

  1182

  1183 lemma pos_add_strict:

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

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

  1186

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

  1188 by (rule zero_less_one [THEN less_imp_le])

  1189

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

  1191 by (simp add: not_le)

  1192

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

  1194 by (simp add: not_less)

  1195

  1196 lemma less_1_mult:

  1197   assumes "1 < m" and "1 < n"

  1198   shows "1 < m * n"

  1199   using assms mult_strict_mono [of 1 m 1 n]

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

  1201

  1202 end

  1203

  1204 class linordered_idom = comm_ring_1 +

  1205   linordered_comm_semiring_strict + ordered_ab_group_add +

  1206   abs_if + sgn_if

  1207   (*previously linordered_ring*)

  1208 begin

  1209

  1210 subclass linordered_ring_strict ..

  1211 subclass ordered_comm_ring ..

  1212 subclass idom ..

  1213

  1214 subclass linordered_semidom

  1215 proof

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

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

  1218 qed

  1219

  1220 lemma linorder_neqE_linordered_idom:

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

  1222   using assms by (rule neqE)

  1223

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

  1225

  1226 lemma mult_le_cancel_right1:

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

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

  1229

  1230 lemma mult_le_cancel_right2:

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

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

  1233

  1234 lemma mult_le_cancel_left1:

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

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

  1237

  1238 lemma mult_le_cancel_left2:

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

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

  1241

  1242 lemma mult_less_cancel_right1:

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

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

  1245

  1246 lemma mult_less_cancel_right2:

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

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

  1249

  1250 lemma mult_less_cancel_left1:

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

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

  1253

  1254 lemma mult_less_cancel_left2:

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

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

  1257

  1258 lemma sgn_sgn [simp]:

  1259   "sgn (sgn a) = sgn a"

  1260 unfolding sgn_if by simp

  1261

  1262 lemma sgn_0_0:

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

  1264 unfolding sgn_if by simp

  1265

  1266 lemma sgn_1_pos:

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

  1268 unfolding sgn_if by (simp add: neg_equal_zero)

  1269

  1270 lemma sgn_1_neg:

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

  1272 unfolding sgn_if by (auto simp add: equal_neg_zero)

  1273

  1274 lemma sgn_pos [simp]:

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

  1276 unfolding sgn_1_pos .

  1277

  1278 lemma sgn_neg [simp]:

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

  1280 unfolding sgn_1_neg .

  1281

  1282 lemma sgn_times:

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

  1284 by (auto simp add: sgn_if zero_less_mult_iff)

  1285

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

  1287 unfolding sgn_if abs_if by auto

  1288

  1289 lemma sgn_greater [simp]:

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

  1291   unfolding sgn_if by auto

  1292

  1293 lemma sgn_less [simp]:

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

  1295   unfolding sgn_if by auto

  1296

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

  1298   by (simp add: abs_if)

  1299

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

  1301   by (simp add: abs_if)

  1302

  1303 lemma dvd_if_abs_eq:

  1304   "abs l = abs (k) \<Longrightarrow> l dvd k"

  1305 by(subst abs_dvd_iff[symmetric]) simp

  1306

  1307 end

  1308

  1309 class linordered_field = field + linordered_idom

  1310

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

  1312

  1313 lemmas mult_compare_simps[noatp] =

  1314     mult_le_cancel_right mult_le_cancel_left

  1315     mult_le_cancel_right1 mult_le_cancel_right2

  1316     mult_le_cancel_left1 mult_le_cancel_left2

  1317     mult_less_cancel_right mult_less_cancel_left

  1318     mult_less_cancel_right1 mult_less_cancel_right2

  1319     mult_less_cancel_left1 mult_less_cancel_left2

  1320     mult_cancel_right mult_cancel_left

  1321     mult_cancel_right1 mult_cancel_right2

  1322     mult_cancel_left1 mult_cancel_left2

  1323

  1324 -- {* FIXME continue localization here *}

  1325

  1326 lemma inverse_nonzero_iff_nonzero [simp]:

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

  1328 by (force dest: inverse_zero_imp_zero)

  1329

  1330 lemma inverse_minus_eq [simp]:

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

  1332 proof cases

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

  1334 next

  1335   assume "a\<noteq>0"

  1336   thus ?thesis by (simp add: nonzero_inverse_minus_eq)

  1337 qed

  1338

  1339 lemma inverse_eq_imp_eq:

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

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

  1342  apply (force dest!: inverse_zero_imp_zero

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

  1344 apply (force dest!: nonzero_inverse_eq_imp_eq)

  1345 done

  1346

  1347 lemma inverse_eq_iff_eq [simp]:

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

  1349 by (force dest!: inverse_eq_imp_eq)

  1350

  1351 lemma inverse_inverse_eq [simp]:

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

  1353   proof cases

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

  1355   next

  1356     assume "a\<noteq>0"

  1357     thus ?thesis by (simp add: nonzero_inverse_inverse_eq)

  1358   qed

  1359

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

  1361       the right-hand side.*}

  1362 lemma inverse_mult_distrib [simp]:

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

  1364   proof cases

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

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

  1367   next

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

  1369     thus ?thesis by force

  1370   qed

  1371

  1372 lemma inverse_divide [simp]:

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

  1374 by (simp add: divide_inverse mult_commute)

  1375

  1376

  1377 subsection {* Calculations with fractions *}

  1378

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

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

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

  1382

  1383 lemma mult_divide_mult_cancel_left:

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

  1385 apply (cases "b = 0")

  1386 apply (simp_all add: nonzero_mult_divide_mult_cancel_left)

  1387 done

  1388

  1389 lemma mult_divide_mult_cancel_right:

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

  1391 apply (cases "b = 0")

  1392 apply (simp_all add: nonzero_mult_divide_mult_cancel_right)

  1393 done

  1394

  1395 lemma divide_divide_eq_right [simp,noatp]:

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

  1397 by (simp add: divide_inverse mult_ac)

  1398

  1399 lemma divide_divide_eq_left [simp,noatp]:

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

  1401 by (simp add: divide_inverse mult_assoc)

  1402

  1403

  1404 subsubsection{*Special Cancellation Simprules for Division*}

  1405

  1406 lemma mult_divide_mult_cancel_left_if[simp,noatp]:

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

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

  1409 by (simp add: mult_divide_mult_cancel_left)

  1410

  1411

  1412 subsection {* Division and Unary Minus *}

  1413

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

  1415 by (simp add: divide_inverse)

  1416

  1417 lemma divide_minus_right [simp, noatp]:

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

  1419 by (simp add: divide_inverse)

  1420

  1421 lemma minus_divide_divide:

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

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

  1424 apply (simp add: nonzero_minus_divide_divide)

  1425 done

  1426

  1427 lemma eq_divide_eq:

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

  1429 by (simp add: nonzero_eq_divide_eq)

  1430

  1431 lemma divide_eq_eq:

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

  1433 by (force simp add: nonzero_divide_eq_eq)

  1434

  1435

  1436 subsection {* Ordered Fields *}

  1437

  1438 lemma positive_imp_inverse_positive:

  1439 assumes a_gt_0: "0 < a"  shows "0 < inverse (a::'a::linordered_field)"

  1440 proof -

  1441   have "0 < a * inverse a"

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

  1443   thus "0 < inverse a"

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

  1445 qed

  1446

  1447 lemma negative_imp_inverse_negative:

  1448   "a < 0 ==> inverse a < (0::'a::linordered_field)"

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

  1450     simp add: nonzero_inverse_minus_eq order_less_imp_not_eq)

  1451

  1452 lemma inverse_le_imp_le:

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

  1454 shows "b \<le> (a::'a::linordered_field)"

  1455 proof (rule classical)

  1456   assume "~ b \<le> a"

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

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

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

  1460     by (simp add: apos invle order_less_imp_le mult_left_mono)

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

  1462     by (simp add: bpos order_less_imp_le mult_right_mono)

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

  1464 qed

  1465

  1466 lemma inverse_positive_imp_positive:

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

  1468 shows "0 < (a::'a::linordered_field)"

  1469 proof -

  1470   have "0 < inverse (inverse a)"

  1471     using inv_gt_0 by (rule positive_imp_inverse_positive)

  1472   thus "0 < a"

  1473     using nz by (simp add: nonzero_inverse_inverse_eq)

  1474 qed

  1475

  1476 lemma inverse_positive_iff_positive [simp]:

  1477   "(0 < inverse a) = (0 < (a::'a::{linordered_field,division_by_zero}))"

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

  1479 apply (blast intro: inverse_positive_imp_positive positive_imp_inverse_positive)

  1480 done

  1481

  1482 lemma inverse_negative_imp_negative:

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

  1484 shows "a < (0::'a::linordered_field)"

  1485 proof -

  1486   have "inverse (inverse a) < 0"

  1487     using inv_less_0 by (rule negative_imp_inverse_negative)

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

  1489 qed

  1490

  1491 lemma inverse_negative_iff_negative [simp]:

  1492   "(inverse a < 0) = (a < (0::'a::{linordered_field,division_by_zero}))"

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

  1494 apply (blast intro: inverse_negative_imp_negative negative_imp_inverse_negative)

  1495 done

  1496

  1497 lemma inverse_nonnegative_iff_nonnegative [simp]:

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

  1499 by (simp add: linorder_not_less [symmetric])

  1500

  1501 lemma inverse_nonpositive_iff_nonpositive [simp]:

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

  1503 by (simp add: linorder_not_less [symmetric])

  1504

  1505 lemma linordered_field_no_lb: "\<forall> x. \<exists>y. y < (x::'a::linordered_field)"

  1506 proof

  1507   fix x::'a

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

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

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

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

  1512 qed

  1513

  1514 lemma linordered_field_no_ub: "\<forall> x. \<exists>y. y > (x::'a::linordered_field)"

  1515 proof

  1516   fix x::'a

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

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

  1519   have "1 + x > x" by simp

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

  1521 qed

  1522

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

  1524

  1525 lemma less_imp_inverse_less:

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

  1527 shows "inverse b < inverse (a::'a::linordered_field)"

  1528 proof (rule ccontr)

  1529   assume "~ inverse b < inverse a"

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

  1531   hence "~ (a < b)"

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

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

  1534 qed

  1535

  1536 lemma inverse_less_imp_less:

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

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

  1539 apply (force dest!: inverse_le_imp_le nonzero_inverse_eq_imp_eq)

  1540 done

  1541

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

  1543 lemma inverse_less_iff_less [simp,noatp]:

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

  1545 by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less)

  1546

  1547 lemma le_imp_inverse_le:

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

  1549 by (force simp add: order_le_less less_imp_inverse_less)

  1550

  1551 lemma inverse_le_iff_le [simp,noatp]:

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

  1553 by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le)

  1554

  1555

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

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

  1558 lemma inverse_le_imp_le_neg:

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

  1560 apply (rule classical)

  1561 apply (subgoal_tac "a < 0")

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

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

  1564 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)

  1565 done

  1566

  1567 lemma less_imp_inverse_less_neg:

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

  1569 apply (subgoal_tac "a < 0")

  1570  prefer 2 apply (blast intro: order_less_trans)

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

  1572 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)

  1573 done

  1574

  1575 lemma inverse_less_imp_less_neg:

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

  1577 apply (rule classical)

  1578 apply (subgoal_tac "a < 0")

  1579  prefer 2

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

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

  1582 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)

  1583 done

  1584

  1585 lemma inverse_less_iff_less_neg [simp,noatp]:

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

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

  1588 apply (simp del: inverse_less_iff_less

  1589             add: order_less_imp_not_eq nonzero_inverse_minus_eq)

  1590 done

  1591

  1592 lemma le_imp_inverse_le_neg:

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

  1594 by (force simp add: order_le_less less_imp_inverse_less_neg)

  1595

  1596 lemma inverse_le_iff_le_neg [simp,noatp]:

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

  1598 by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg)

  1599

  1600

  1601 subsection{*Inverses and the Number One*}

  1602

  1603 lemma one_less_inverse_iff:

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

  1605 proof cases

  1606   assume "0 < x"

  1607     with inverse_less_iff_less [OF zero_less_one, of x]

  1608     show ?thesis by simp

  1609 next

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

  1611   have "~ (1 < inverse x)"

  1612   proof

  1613     assume "1 < inverse x"

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

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

  1616     finally show False by auto

  1617   qed

  1618   with notless show ?thesis by simp

  1619 qed

  1620

  1621 lemma inverse_eq_1_iff [simp]:

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

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

  1624

  1625 lemma one_le_inverse_iff:

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

  1627 by (force simp add: order_le_less one_less_inverse_iff zero_less_one

  1628                     eq_commute [of 1])

  1629

  1630 lemma inverse_less_1_iff:

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

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

  1633

  1634 lemma inverse_le_1_iff:

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

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

  1637

  1638

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

  1640

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

  1642 proof -

  1643   assume less: "0<c"

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

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

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

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

  1648   finally show ?thesis .

  1649 qed

  1650

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

  1652 proof -

  1653   assume less: "c<0"

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

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

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

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

  1658   finally show ?thesis .

  1659 qed

  1660

  1661 lemma le_divide_eq:

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

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

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

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

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

  1667 apply (force simp add: pos_le_divide_eq neg_le_divide_eq linorder_neq_iff)

  1668 done

  1669

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

  1671 proof -

  1672   assume less: "0<c"

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

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

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

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

  1677   finally show ?thesis .

  1678 qed

  1679

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

  1681 proof -

  1682   assume less: "c<0"

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

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

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

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

  1687   finally show ?thesis .

  1688 qed

  1689

  1690 lemma divide_le_eq:

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

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

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

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

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

  1696 apply (force simp add: pos_divide_le_eq neg_divide_le_eq linorder_neq_iff)

  1697 done

  1698

  1699 lemma pos_less_divide_eq:

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

  1701 proof -

  1702   assume less: "0<c"

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

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

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

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

  1707   finally show ?thesis .

  1708 qed

  1709

  1710 lemma neg_less_divide_eq:

  1711  "c < (0::'a::linordered_field) ==> (a < b/c) = (b < a*c)"

  1712 proof -

  1713   assume less: "c<0"

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

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

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

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

  1718   finally show ?thesis .

  1719 qed

  1720

  1721 lemma less_divide_eq:

  1722   "(a < b/c) =

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

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

  1725              else  a < (0::'a::{linordered_field,division_by_zero}))"

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

  1727 apply (force simp add: pos_less_divide_eq neg_less_divide_eq linorder_neq_iff)

  1728 done

  1729

  1730 lemma pos_divide_less_eq:

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

  1732 proof -

  1733   assume less: "0<c"

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

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

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

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

  1738   finally show ?thesis .

  1739 qed

  1740

  1741 lemma neg_divide_less_eq:

  1742  "c < (0::'a::linordered_field) ==> (b/c < a) = (a*c < b)"

  1743 proof -

  1744   assume less: "c<0"

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

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

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

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

  1749   finally show ?thesis .

  1750 qed

  1751

  1752 lemma divide_less_eq:

  1753   "(b/c < a) =

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

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

  1756              else 0 < (a::'a::{linordered_field,division_by_zero}))"

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

  1758 apply (force simp add: pos_divide_less_eq neg_divide_less_eq linorder_neq_iff)

  1759 done

  1760

  1761

  1762 subsection{*Field simplification*}

  1763

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

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

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

  1767 more benign @{text algebra_simps}. *}

  1768

  1769 lemmas field_simps[noatp] = field_eq_simps

  1770   (* multiply ineqn *)

  1771   pos_divide_less_eq neg_divide_less_eq

  1772   pos_less_divide_eq neg_less_divide_eq

  1773   pos_divide_le_eq neg_divide_le_eq

  1774   pos_le_divide_eq neg_le_divide_eq

  1775

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

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

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

  1779 explosions. *}

  1780

  1781 lemmas sign_simps[noatp] = group_simps

  1782   zero_less_mult_iff  mult_less_0_iff

  1783

  1784 (* Only works once linear arithmetic is installed:

  1785 text{*An example:*}

  1786 lemma fixes a b c d e f :: "'a::linordered_field"

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

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

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

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

  1791  prefer 2 apply(simp add:sign_simps)

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

  1793  prefer 2 apply(simp add:sign_simps)

  1794 apply(simp add:field_simps)

  1795 done

  1796 *)

  1797

  1798

  1799 subsection{*Division and Signs*}

  1800

  1801 lemma zero_less_divide_iff:

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

  1803 by (simp add: divide_inverse zero_less_mult_iff)

  1804

  1805 lemma divide_less_0_iff:

  1806      "(a/b < (0::'a::{linordered_field,division_by_zero})) =

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

  1808 by (simp add: divide_inverse mult_less_0_iff)

  1809

  1810 lemma zero_le_divide_iff:

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

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

  1813 by (simp add: divide_inverse zero_le_mult_iff)

  1814

  1815 lemma divide_le_0_iff:

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

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

  1818 by (simp add: divide_inverse mult_le_0_iff)

  1819

  1820 lemma divide_eq_0_iff [simp,noatp]:

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

  1822 by (simp add: divide_inverse)

  1823

  1824 lemma divide_pos_pos:

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

  1826 by(simp add:field_simps)

  1827

  1828

  1829 lemma divide_nonneg_pos:

  1830   "0 <= (x::'a::linordered_field) ==> 0 < y ==> 0 <= x / y"

  1831 by(simp add:field_simps)

  1832

  1833 lemma divide_neg_pos:

  1834   "(x::'a::linordered_field) < 0 ==> 0 < y ==> x / y < 0"

  1835 by(simp add:field_simps)

  1836

  1837 lemma divide_nonpos_pos:

  1838   "(x::'a::linordered_field) <= 0 ==> 0 < y ==> x / y <= 0"

  1839 by(simp add:field_simps)

  1840

  1841 lemma divide_pos_neg:

  1842   "0 < (x::'a::linordered_field) ==> y < 0 ==> x / y < 0"

  1843 by(simp add:field_simps)

  1844

  1845 lemma divide_nonneg_neg:

  1846   "0 <= (x::'a::linordered_field) ==> y < 0 ==> x / y <= 0"

  1847 by(simp add:field_simps)

  1848

  1849 lemma divide_neg_neg:

  1850   "(x::'a::linordered_field) < 0 ==> y < 0 ==> 0 < x / y"

  1851 by(simp add:field_simps)

  1852

  1853 lemma divide_nonpos_neg:

  1854   "(x::'a::linordered_field) <= 0 ==> y < 0 ==> 0 <= x / y"

  1855 by(simp add:field_simps)

  1856

  1857

  1858 subsection{*Cancellation Laws for Division*}

  1859

  1860 lemma divide_cancel_right [simp,noatp]:

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

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

  1863 apply (simp add: divide_inverse)

  1864 done

  1865

  1866 lemma divide_cancel_left [simp,noatp]:

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

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

  1869 apply (simp add: divide_inverse)

  1870 done

  1871

  1872

  1873 subsection {* Division and the Number One *}

  1874

  1875 text{*Simplify expressions equated with 1*}

  1876 lemma divide_eq_1_iff [simp,noatp]:

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

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

  1879 apply (simp add: right_inverse_eq)

  1880 done

  1881

  1882 lemma one_eq_divide_iff [simp,noatp]:

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

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

  1885

  1886 lemma zero_eq_1_divide_iff [simp,noatp]:

  1887      "((0::'a::{linordered_field,division_by_zero}) = 1/a) = (a = 0)"

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

  1889 apply (auto simp add: nonzero_eq_divide_eq)

  1890 done

  1891

  1892 lemma one_divide_eq_0_iff [simp,noatp]:

  1893      "(1/a = (0::'a::{linordered_field,division_by_zero})) = (a = 0)"

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

  1895 apply (insert zero_neq_one [THEN not_sym])

  1896 apply (auto simp add: nonzero_divide_eq_eq)

  1897 done

  1898

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

  1900 lemmas zero_less_divide_1_iff = zero_less_divide_iff [of 1, simplified]

  1901 lemmas divide_less_0_1_iff = divide_less_0_iff [of 1, simplified]

  1902 lemmas zero_le_divide_1_iff = zero_le_divide_iff [of 1, simplified]

  1903 lemmas divide_le_0_1_iff = divide_le_0_iff [of 1, simplified]

  1904

  1905 declare zero_less_divide_1_iff [simp,noatp]

  1906 declare divide_less_0_1_iff [simp,noatp]

  1907 declare zero_le_divide_1_iff [simp,noatp]

  1908 declare divide_le_0_1_iff [simp,noatp]

  1909

  1910

  1911 subsection {* Ordering Rules for Division *}

  1912

  1913 lemma divide_strict_right_mono:

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

  1915 by (simp add: order_less_imp_not_eq2 divide_inverse mult_strict_right_mono

  1916               positive_imp_inverse_positive)

  1917

  1918 lemma divide_right_mono:

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

  1920 by (force simp add: divide_strict_right_mono order_le_less)

  1921

  1922 lemma divide_right_mono_neg: "(a::'a::{division_by_zero,linordered_field}) <= b

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

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

  1925 apply auto

  1926 done

  1927

  1928 lemma divide_strict_right_mono_neg:

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

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

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

  1932 done

  1933

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

  1935       have the same sign*}

  1936 lemma divide_strict_left_mono:

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

  1938 by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono)

  1939

  1940 lemma divide_left_mono:

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

  1942 by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_right_mono)

  1943

  1944 lemma divide_left_mono_neg: "(a::'a::{division_by_zero,linordered_field}) <= b

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

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

  1947   apply (auto simp add: mult_commute)

  1948 done

  1949

  1950 lemma divide_strict_left_mono_neg:

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

  1952 by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono_neg)

  1953

  1954

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

  1956

  1957 lemma le_divide_eq_1 [noatp]:

  1958   fixes a :: "'a :: {linordered_field,division_by_zero}"

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

  1960 by (auto simp add: le_divide_eq)

  1961

  1962 lemma divide_le_eq_1 [noatp]:

  1963   fixes a :: "'a :: {linordered_field,division_by_zero}"

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

  1965 by (auto simp add: divide_le_eq)

  1966

  1967 lemma less_divide_eq_1 [noatp]:

  1968   fixes a :: "'a :: {linordered_field,division_by_zero}"

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

  1970 by (auto simp add: less_divide_eq)

  1971

  1972 lemma divide_less_eq_1 [noatp]:

  1973   fixes a :: "'a :: {linordered_field,division_by_zero}"

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

  1975 by (auto simp add: divide_less_eq)

  1976

  1977

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

  1979

  1980 lemma le_divide_eq_1_pos [simp,noatp]:

  1981   fixes a :: "'a :: {linordered_field,division_by_zero}"

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

  1983 by (auto simp add: le_divide_eq)

  1984

  1985 lemma le_divide_eq_1_neg [simp,noatp]:

  1986   fixes a :: "'a :: {linordered_field,division_by_zero}"

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

  1988 by (auto simp add: le_divide_eq)

  1989

  1990 lemma divide_le_eq_1_pos [simp,noatp]:

  1991   fixes a :: "'a :: {linordered_field,division_by_zero}"

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

  1993 by (auto simp add: divide_le_eq)

  1994

  1995 lemma divide_le_eq_1_neg [simp,noatp]:

  1996   fixes a :: "'a :: {linordered_field,division_by_zero}"

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

  1998 by (auto simp add: divide_le_eq)

  1999

  2000 lemma less_divide_eq_1_pos [simp,noatp]:

  2001   fixes a :: "'a :: {linordered_field,division_by_zero}"

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

  2003 by (auto simp add: less_divide_eq)

  2004

  2005 lemma less_divide_eq_1_neg [simp,noatp]:

  2006   fixes a :: "'a :: {linordered_field,division_by_zero}"

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

  2008 by (auto simp add: less_divide_eq)

  2009

  2010 lemma divide_less_eq_1_pos [simp,noatp]:

  2011   fixes a :: "'a :: {linordered_field,division_by_zero}"

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

  2013 by (auto simp add: divide_less_eq)

  2014

  2015 lemma divide_less_eq_1_neg [simp,noatp]:

  2016   fixes a :: "'a :: {linordered_field,division_by_zero}"

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

  2018 by (auto simp add: divide_less_eq)

  2019

  2020 lemma eq_divide_eq_1 [simp,noatp]:

  2021   fixes a :: "'a :: {linordered_field,division_by_zero}"

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

  2023 by (auto simp add: eq_divide_eq)

  2024

  2025 lemma divide_eq_eq_1 [simp,noatp]:

  2026   fixes a :: "'a :: {linordered_field,division_by_zero}"

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

  2028 by (auto simp add: divide_eq_eq)

  2029

  2030

  2031 subsection {* Reasoning about inequalities with division *}

  2032

  2033 lemma mult_right_le_one_le: "0 <= (x::'a::linordered_idom) ==> 0 <= y ==> y <= 1

  2034     ==> x * y <= x"

  2035 by (auto simp add: mult_compare_simps)

  2036

  2037 lemma mult_left_le_one_le: "0 <= (x::'a::linordered_idom) ==> 0 <= y ==> y <= 1

  2038     ==> y * x <= x"

  2039 by (auto simp add: mult_compare_simps)

  2040

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

  2042     x / y <= z"

  2043 by (subst pos_divide_le_eq, assumption+)

  2044

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

  2046     z <= x / y"

  2047 by(simp add:field_simps)

  2048

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

  2050     x / y < z"

  2051 by(simp add:field_simps)

  2052

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

  2054     z < x / y"

  2055 by(simp add:field_simps)

  2056

  2057 lemma frac_le: "(0::'a::linordered_field) <= x ==>

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

  2059   apply (rule mult_imp_div_pos_le)

  2060   apply simp

  2061   apply (subst times_divide_eq_left)

  2062   apply (rule mult_imp_le_div_pos, assumption)

  2063   apply (rule mult_mono)

  2064   apply simp_all

  2065 done

  2066

  2067 lemma frac_less: "(0::'a::linordered_field) <= x ==>

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

  2069   apply (rule mult_imp_div_pos_less)

  2070   apply simp

  2071   apply (subst times_divide_eq_left)

  2072   apply (rule mult_imp_less_div_pos, assumption)

  2073   apply (erule mult_less_le_imp_less)

  2074   apply simp_all

  2075 done

  2076

  2077 lemma frac_less2: "(0::'a::linordered_field) < x ==>

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

  2079   apply (rule mult_imp_div_pos_less)

  2080   apply simp_all

  2081   apply (subst times_divide_eq_left)

  2082   apply (rule mult_imp_less_div_pos, assumption)

  2083   apply (erule mult_le_less_imp_less)

  2084   apply simp_all

  2085 done

  2086

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

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

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

  2090   seem to need them.*}

  2091

  2092 declare times_divide_eq [simp]

  2093

  2094

  2095 subsection {* Ordered Fields are Dense *}

  2096

  2097 context linordered_semidom

  2098 begin

  2099

  2100 lemma less_add_one: "a < a + 1"

  2101 proof -

  2102   have "a + 0 < a + 1"

  2103     by (blast intro: zero_less_one add_strict_left_mono)

  2104   thus ?thesis by simp

  2105 qed

  2106

  2107 lemma zero_less_two: "0 < 1 + 1"

  2108 by (blast intro: less_trans zero_less_one less_add_one)

  2109

  2110 end

  2111

  2112 lemma less_half_sum: "a < b ==> a < (a+b) / (1+1::'a::linordered_field)"

  2113 by (simp add: field_simps zero_less_two)

  2114

  2115 lemma gt_half_sum: "a < b ==> (a+b)/(1+1::'a::linordered_field) < b"

  2116 by (simp add: field_simps zero_less_two)

  2117

  2118 instance linordered_field < dense_linorder

  2119 proof

  2120   fix x y :: 'a

  2121   have "x < x + 1" by simp

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

  2123   have "x - 1 < x" by simp

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

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

  2126 qed

  2127

  2128

  2129 subsection {* Absolute Value *}

  2130

  2131 context linordered_idom

  2132 begin

  2133

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

  2135   unfolding abs_if sgn_if by auto

  2136

  2137 end

  2138

  2139 lemma abs_one [simp]: "abs 1 = (1::'a::linordered_idom)"

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

  2141

  2142 class ordered_ring_abs = ordered_ring + ordered_ab_group_add_abs +

  2143   assumes abs_eq_mult:

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

  2145

  2146 context linordered_idom

  2147 begin

  2148

  2149 subclass ordered_ring_abs proof

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

  2151

  2152 lemma abs_mult:

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

  2154   by (rule abs_eq_mult) auto

  2155

  2156 lemma abs_mult_self:

  2157   "abs a * abs a = a * a"

  2158   by (simp add: abs_if)

  2159

  2160 end

  2161

  2162 lemma nonzero_abs_inverse:

  2163      "a \<noteq> 0 ==> abs (inverse (a::'a::linordered_field)) = inverse (abs a)"

  2164 apply (auto simp add: linorder_neq_iff abs_if nonzero_inverse_minus_eq

  2165                       negative_imp_inverse_negative)

  2166 apply (blast intro: positive_imp_inverse_positive elim: order_less_asym)

  2167 done

  2168

  2169 lemma abs_inverse [simp]:

  2170      "abs (inverse (a::'a::{linordered_field,division_by_zero})) =

  2171       inverse (abs a)"

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

  2173 apply (simp add: nonzero_abs_inverse)

  2174 done

  2175

  2176 lemma nonzero_abs_divide:

  2177      "b \<noteq> 0 ==> abs (a / (b::'a::linordered_field)) = abs a / abs b"

  2178 by (simp add: divide_inverse abs_mult nonzero_abs_inverse)

  2179

  2180 lemma abs_divide [simp]:

  2181      "abs (a / (b::'a::{linordered_field,division_by_zero})) = abs a / abs b"

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

  2183 apply (simp add: nonzero_abs_divide)

  2184 done

  2185

  2186 lemma abs_mult_less:

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

  2188 proof -

  2189   assume ac: "abs a < c"

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

  2191   assume "abs b < d"

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

  2193 qed

  2194

  2195 lemmas eq_minus_self_iff[noatp] = equal_neg_zero

  2196

  2197 lemma less_minus_self_iff: "(a < -a) = (a < (0::'a::linordered_idom))"

  2198   unfolding order_less_le less_eq_neg_nonpos equal_neg_zero ..

  2199

  2200 lemma abs_less_iff: "(abs a < b) = (a < b & -a < (b::'a::linordered_idom))"

  2201 apply (simp add: order_less_le abs_le_iff)

  2202 apply (auto simp add: abs_if neg_less_eq_nonneg less_eq_neg_nonpos)

  2203 done

  2204

  2205 lemma abs_mult_pos: "(0::'a::linordered_idom) <= x ==>

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

  2207   apply (subst abs_mult)

  2208   apply simp

  2209 done

  2210

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

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

  2213   apply (subst abs_divide)

  2214   apply (simp add: order_less_imp_le)

  2215 done

  2216

  2217 code_modulename SML

  2218   Ring_and_Field Arith

  2219

  2220 code_modulename OCaml

  2221   Ring_and_Field Arith

  2222

  2223 code_modulename Haskell

  2224   Ring_and_Field Arith

  2225

  2226 end