src/HOL/Ring_and_Field.thy
 author huffman Mon Jan 12 12:09:54 2009 -0800 (2009-01-12) changeset 29460 ad87e5d1488b parent 29409 f0a8fe83bc07 child 29461 7c1841a7bdf4 permissions -rw-r--r--
new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]
     1 (*  Title:   HOL/Ring_and_Field.thy

     2     ID:      $Id$

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

     4              with contributions by Jeremy Avigad

     5 *)

     6

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

     8

     9 theory Ring_and_Field

    10 imports OrderedGroup

    11 begin

    12

    13 text {*

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

    15   \begin{itemize}

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

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

    18   \end{itemize}

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

    20   \begin{itemize}

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

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

    23   \end{itemize}

    24 *}

    25

    26 class semiring = ab_semigroup_add + semigroup_mult +

    27   assumes left_distrib: "(a + b) * c = a * c + b * c"

    28   assumes right_distrib: "a * (b + c) = a * b + a * c"

    29 begin

    30

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

    32 lemma combine_common_factor:

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

    34   by (simp add: left_distrib add_ac)

    35

    36 end

    37

    38 class mult_zero = times + zero +

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

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

    41

    42 class semiring_0 = semiring + comm_monoid_add + mult_zero

    43

    44 class semiring_0_cancel = semiring + comm_monoid_add + cancel_ab_semigroup_add

    45 begin

    46

    47 subclass semiring_0

    48 proof

    49   fix a :: 'a

    50   have "0 * a + 0 * a = 0 * a + 0"

    51     by (simp add: left_distrib [symmetric])

    52   thus "0 * a = 0"

    53     by (simp only: add_left_cancel)

    54 next

    55   fix a :: 'a

    56   have "a * 0 + a * 0 = a * 0 + 0"

    57     by (simp add: right_distrib [symmetric])

    58   thus "a * 0 = 0"

    59     by (simp only: add_left_cancel)

    60 qed

    61

    62 end

    63

    64 class comm_semiring = ab_semigroup_add + ab_semigroup_mult +

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

    66 begin

    67

    68 subclass semiring

    69 proof

    70   fix a b c :: 'a

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

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

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

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

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

    76 qed

    77

    78 end

    79

    80 class comm_semiring_0 = comm_semiring + comm_monoid_add + mult_zero

    81 begin

    82

    83 subclass semiring_0 ..

    84

    85 end

    86

    87 class comm_semiring_0_cancel = comm_semiring + comm_monoid_add + cancel_ab_semigroup_add

    88 begin

    89

    90 subclass semiring_0_cancel ..

    91

    92 subclass comm_semiring_0 ..

    93

    94 end

    95

    96 class zero_neq_one = zero + one +

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

    98 begin

    99

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

   101   by (rule not_sym) (rule zero_neq_one)

   102

   103 end

   104

   105 class semiring_1 = zero_neq_one + semiring_0 + monoid_mult

   106

   107 text {* Abstract divisibility *}

   108

   109 class dvd = times

   110 begin

   111

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

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

   114

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

   116   unfolding dvd_def ..

   117

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

   119   unfolding dvd_def by blast

   120

   121 end

   122

   123 class comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult + dvd

   124   (*previously almost_semiring*)

   125 begin

   126

   127 subclass semiring_1 ..

   128

   129 lemma dvd_refl: "a dvd a"

   130 proof

   131   show "a = a * 1" by simp

   132 qed

   133

   134 lemma dvd_trans:

   135   assumes "a dvd b" and "b dvd c"

   136   shows "a dvd c"

   137 proof -

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

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

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

   141   then show ?thesis ..

   142 qed

   143

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

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

   146

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

   148 proof

   149   show "0 = a * 0" by simp

   150 qed

   151

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

   153   by (auto intro!: dvdI)

   154

   155 lemma dvd_mult: "a dvd c \<Longrightarrow> a dvd (b * c)"

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

   157

   158 lemma dvd_mult2: "a dvd b \<Longrightarrow> a dvd (b * c)"

   159   apply (subst mult_commute)

   160   apply (erule dvd_mult)

   161   done

   162

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

   164   by (rule dvd_mult) (rule dvd_refl)

   165

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

   167   by (rule dvd_mult2) (rule dvd_refl)

   168

   169 lemma mult_dvd_mono:

   170   assumes ab: "a dvd b"

   171     and "cd": "c dvd d"

   172   shows "a * c dvd b * d"

   173 proof -

   174   from ab obtain b' where "b = a * b'" ..

   175   moreover from "cd" obtain d' where "d = c * d'" ..

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

   177   then show ?thesis ..

   178 qed

   179

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

   181   by (simp add: dvd_def mult_assoc, blast)

   182

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

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

   185

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

   187   by simp

   188

   189 lemma dvd_add:

   190   assumes ab: "a dvd b"

   191     and ac: "a dvd c"

   192     shows "a dvd (b + c)"

   193 proof -

   194   from ab obtain b' where "b = a * b'" ..

   195   moreover from ac obtain c' where "c = a * c'" ..

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

   197   then show ?thesis ..

   198 qed

   199

   200 end

   201

   202 class no_zero_divisors = zero + times +

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

   204

   205 class semiring_1_cancel = semiring + comm_monoid_add + zero_neq_one

   206   + cancel_ab_semigroup_add + monoid_mult

   207 begin

   208

   209 subclass semiring_0_cancel ..

   210

   211 subclass semiring_1 ..

   212

   213 end

   214

   215 class comm_semiring_1_cancel = comm_semiring + comm_monoid_add + comm_monoid_mult

   216   + zero_neq_one + cancel_ab_semigroup_add

   217 begin

   218

   219 subclass semiring_1_cancel ..

   220 subclass comm_semiring_0_cancel ..

   221 subclass comm_semiring_1 ..

   222

   223 end

   224

   225 class ring = semiring + ab_group_add

   226 begin

   227

   228 subclass semiring_0_cancel ..

   229

   230 text {* Distribution rules *}

   231

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

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

   234

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

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

   237

   238 text{*Extract signs from products*}

   239 lemmas mult_minus_left [simp] = minus_mult_left [symmetric]

   240 lemmas mult_minus_right [simp] = minus_mult_right [symmetric]

   241

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

   243   by simp

   244

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

   246   by simp

   247

   248 lemma right_diff_distrib: "a * (b - c) = a * b - a * c"

   249   by (simp add: right_distrib diff_minus)

   250

   251 lemma left_diff_distrib: "(a - b) * c = a * c - b * c"

   252   by (simp add: left_distrib diff_minus)

   253

   254 lemmas ring_distribs =

   255   right_distrib left_distrib left_diff_distrib right_diff_distrib

   256

   257 lemmas ring_simps =

   258   add_ac

   259   add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2

   260   diff_eq_eq eq_diff_eq diff_minus [symmetric] uminus_add_conv_diff

   261   ring_distribs

   262

   263 lemma eq_add_iff1:

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

   265   by (simp add: ring_simps)

   266

   267 lemma eq_add_iff2:

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

   269   by (simp add: ring_simps)

   270

   271 end

   272

   273 lemmas ring_distribs =

   274   right_distrib left_distrib left_diff_distrib right_diff_distrib

   275

   276 class comm_ring = comm_semiring + ab_group_add

   277 begin

   278

   279 subclass ring ..

   280 subclass comm_semiring_0_cancel ..

   281

   282 end

   283

   284 class ring_1 = ring + zero_neq_one + monoid_mult

   285 begin

   286

   287 subclass semiring_1_cancel ..

   288

   289 end

   290

   291 class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult

   292   (*previously ring*)

   293 begin

   294

   295 subclass ring_1 ..

   296 subclass comm_semiring_1_cancel ..

   297

   298 lemma dvd_minus_iff: "x dvd - y \<longleftrightarrow> x dvd y"

   299 proof

   300   assume "x dvd - y"

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

   302   then show "x dvd y" by simp

   303 next

   304   assume "x dvd y"

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

   306   then show "x dvd - y" by simp

   307 qed

   308

   309 lemma minus_dvd_iff: "- x dvd y \<longleftrightarrow> x dvd y"

   310 proof

   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 next

   316   assume "x dvd y"

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

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

   319   then show "- x dvd y" ..

   320 qed

   321

   322 lemma dvd_diff: "x dvd y \<Longrightarrow> x dvd z \<Longrightarrow> x dvd (y - z)"

   323   by (simp add: diff_minus dvd_add dvd_minus_iff)

   324

   325 end

   326

   327 class ring_no_zero_divisors = ring + no_zero_divisors

   328 begin

   329

   330 lemma mult_eq_0_iff [simp]:

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

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

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

   334     then show ?thesis using no_zero_divisors by simp

   335 next

   336   case True then show ?thesis by auto

   337 qed

   338

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

   340 lemma mult_cancel_right [simp, noatp]:

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

   342 proof -

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

   344     by (simp add: ring_distribs right_minus_eq)

   345   thus ?thesis

   346     by (simp add: disj_commute right_minus_eq)

   347 qed

   348

   349 lemma mult_cancel_left [simp, noatp]:

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

   351 proof -

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

   353     by (simp add: ring_distribs right_minus_eq)

   354   thus ?thesis

   355     by (simp add: right_minus_eq)

   356 qed

   357

   358 end

   359

   360 class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors

   361 begin

   362

   363 lemma mult_cancel_right1 [simp]:

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

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

   366

   367 lemma mult_cancel_right2 [simp]:

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

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

   370

   371 lemma mult_cancel_left1 [simp]:

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

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

   374

   375 lemma mult_cancel_left2 [simp]:

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

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

   378

   379 end

   380

   381 class idom = comm_ring_1 + no_zero_divisors

   382 begin

   383

   384 subclass ring_1_no_zero_divisors ..

   385

   386 end

   387

   388 class division_ring = ring_1 + inverse +

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

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

   391 begin

   392

   393 subclass ring_1_no_zero_divisors

   394 proof

   395   fix a b :: 'a

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

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

   398   proof

   399     assume ab: "a * b = 0"

   400     hence "0 = inverse a * (a * b) * inverse b"

   401       by simp

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

   403       by (simp only: mult_assoc)

   404     also have "\<dots> = 1"

   405       using a b by simp

   406     finally show False

   407       by simp

   408   qed

   409 qed

   410

   411 lemma nonzero_imp_inverse_nonzero:

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

   413 proof

   414   assume ianz: "inverse a = 0"

   415   assume "a \<noteq> 0"

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

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

   418   finally have "1 = 0" .

   419   thus False by (simp add: eq_commute)

   420 qed

   421

   422 lemma inverse_zero_imp_zero:

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

   424 apply (rule classical)

   425 apply (drule nonzero_imp_inverse_nonzero)

   426 apply auto

   427 done

   428

   429 lemma inverse_unique:

   430   assumes ab: "a * b = 1"

   431   shows "inverse a = b"

   432 proof -

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

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

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

   436 qed

   437

   438 lemma nonzero_inverse_minus_eq:

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

   440   by (rule inverse_unique) simp

   441

   442 lemma nonzero_inverse_inverse_eq:

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

   444   by (rule inverse_unique) simp

   445

   446 lemma nonzero_inverse_eq_imp_eq:

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

   448   shows "a = b"

   449 proof -

   450   from inverse a = inverse b

   451   have "inverse (inverse a) = inverse (inverse b)"

   452     by (rule arg_cong)

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

   454     by (simp add: nonzero_inverse_inverse_eq)

   455 qed

   456

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

   458   by (rule inverse_unique) simp

   459

   460 lemma nonzero_inverse_mult_distrib:

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

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

   463 proof -

   464   have "a * (b * inverse b) * inverse a = 1"

   465     using assms by simp

   466   hence "a * b * (inverse b * inverse a) = 1"

   467     by (simp only: mult_assoc)

   468   thus ?thesis

   469     by (rule inverse_unique)

   470 qed

   471

   472 lemma division_ring_inverse_add:

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

   474   by (simp add: ring_simps mult_assoc)

   475

   476 lemma division_ring_inverse_diff:

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

   478   by (simp add: ring_simps mult_assoc)

   479

   480 end

   481

   482 class field = comm_ring_1 + inverse +

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

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

   485 begin

   486

   487 subclass division_ring

   488 proof

   489   fix a :: 'a

   490   assume "a \<noteq> 0"

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

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

   493 qed

   494

   495 subclass idom ..

   496

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

   498 proof

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

   500   {

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

   502     also assume "a / b = 1"

   503     finally show "a = b" by simp

   504   next

   505     assume "a = b"

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

   507   }

   508 qed

   509

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

   511   by (simp add: divide_inverse)

   512

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

   514   by (simp add: divide_inverse)

   515

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

   517   by (simp add: divide_inverse)

   518

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

   520   by (simp add: divide_inverse)

   521

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

   523   by (simp add: divide_inverse ring_distribs)

   524

   525 end

   526

   527 class division_by_zero = zero + inverse +

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

   529

   530 lemma divide_zero [simp]:

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

   532   by (simp add: divide_inverse)

   533

   534 lemma divide_self_if [simp]:

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

   536   by simp

   537

   538 class mult_mono = times + zero + ord +

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

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

   541

   542 class pordered_semiring = mult_mono + semiring_0 + pordered_ab_semigroup_add

   543 begin

   544

   545 lemma mult_mono:

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

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

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

   549 apply (erule mult_left_mono, assumption)

   550 done

   551

   552 lemma mult_mono':

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

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

   555 apply (rule mult_mono)

   556 apply (fast intro: order_trans)+

   557 done

   558

   559 end

   560

   561 class pordered_cancel_semiring = mult_mono + pordered_ab_semigroup_add

   562   + semiring + comm_monoid_add + cancel_ab_semigroup_add

   563 begin

   564

   565 subclass semiring_0_cancel ..

   566 subclass pordered_semiring ..

   567

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

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

   570

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

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

   573

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

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

   576

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

   578   by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)

   579

   580 end

   581

   582 class ordered_semiring = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add + mult_mono

   583 begin

   584

   585 subclass pordered_cancel_semiring ..

   586

   587 subclass pordered_comm_monoid_add ..

   588

   589 lemma mult_left_less_imp_less:

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

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

   592

   593 lemma mult_right_less_imp_less:

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

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

   596

   597 end

   598

   599 class ordered_semiring_strict = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add +

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

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

   602 begin

   603

   604 subclass semiring_0_cancel ..

   605

   606 subclass ordered_semiring

   607 proof

   608   fix a b c :: 'a

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

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

   611     unfolding le_less

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

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

   614     unfolding le_less

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

   616 qed

   617

   618 lemma mult_left_le_imp_le:

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

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

   621

   622 lemma mult_right_le_imp_le:

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

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

   625

   626 lemma mult_pos_pos:

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

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

   629

   630 lemma mult_pos_neg:

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

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

   633

   634 lemma mult_pos_neg2:

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

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

   637

   638 lemma zero_less_mult_pos:

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

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

   641  apply (auto simp add: le_less not_less)

   642 apply (drule_tac mult_pos_neg [of a b])

   643  apply (auto dest: less_not_sym)

   644 done

   645

   646 lemma zero_less_mult_pos2:

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

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

   649  apply (auto simp add: le_less not_less)

   650 apply (drule_tac mult_pos_neg2 [of a b])

   651  apply (auto dest: less_not_sym)

   652 done

   653

   654 text{*Strict monotonicity in both arguments*}

   655 lemma mult_strict_mono:

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

   657   shows "a * c < b * d"

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

   659   apply (simp add: mult_pos_pos)

   660   apply (erule mult_strict_right_mono [THEN less_trans])

   661   apply (force simp add: le_less)

   662   apply (erule mult_strict_left_mono, assumption)

   663   done

   664

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

   666 lemma mult_strict_mono':

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

   668   shows "a * c < b * d"

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

   670

   671 lemma mult_less_le_imp_less:

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

   673   shows "a * c < b * d"

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

   675   apply (erule less_le_trans)

   676   apply (erule mult_left_mono)

   677   apply simp

   678   apply (erule mult_strict_right_mono)

   679   apply assumption

   680   done

   681

   682 lemma mult_le_less_imp_less:

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

   684   shows "a * c < b * d"

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

   686   apply (erule le_less_trans)

   687   apply (erule mult_strict_left_mono)

   688   apply simp

   689   apply (erule mult_right_mono)

   690   apply simp

   691   done

   692

   693 lemma mult_less_imp_less_left:

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

   695   shows "a < b"

   696 proof (rule ccontr)

   697   assume "\<not>  a < b"

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

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

   700   with this and less show False

   701     by (simp add: not_less [symmetric])

   702 qed

   703

   704 lemma mult_less_imp_less_right:

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

   706   shows "a < b"

   707 proof (rule ccontr)

   708   assume "\<not> a < b"

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

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

   711   with this and less show False

   712     by (simp add: not_less [symmetric])

   713 qed

   714

   715 end

   716

   717 class mult_mono1 = times + zero + ord +

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

   719

   720 class pordered_comm_semiring = comm_semiring_0

   721   + pordered_ab_semigroup_add + mult_mono1

   722 begin

   723

   724 subclass pordered_semiring

   725 proof

   726   fix a b c :: 'a

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

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

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

   730 qed

   731

   732 end

   733

   734 class pordered_cancel_comm_semiring = comm_semiring_0_cancel

   735   + pordered_ab_semigroup_add + mult_mono1

   736 begin

   737

   738 subclass pordered_comm_semiring ..

   739 subclass pordered_cancel_semiring ..

   740

   741 end

   742

   743 class ordered_comm_semiring_strict = comm_semiring_0 + ordered_cancel_ab_semigroup_add +

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

   745 begin

   746

   747 subclass ordered_semiring_strict

   748 proof

   749   fix a b c :: 'a

   750   assume "a < b" "0 < c"

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

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

   753 qed

   754

   755 subclass pordered_cancel_comm_semiring

   756 proof

   757   fix a b c :: 'a

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

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

   760     unfolding le_less

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

   762 qed

   763

   764 end

   765

   766 class pordered_ring = ring + pordered_cancel_semiring

   767 begin

   768

   769 subclass pordered_ab_group_add ..

   770

   771 lemmas ring_simps = ring_simps group_simps

   772

   773 lemma less_add_iff1:

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

   775   by (simp add: ring_simps)

   776

   777 lemma less_add_iff2:

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

   779   by (simp add: ring_simps)

   780

   781 lemma le_add_iff1:

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

   783   by (simp add: ring_simps)

   784

   785 lemma le_add_iff2:

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

   787   by (simp add: ring_simps)

   788

   789 lemma mult_left_mono_neg:

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

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

   792   apply (simp_all add: minus_mult_left [symmetric])

   793   done

   794

   795 lemma mult_right_mono_neg:

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

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

   798   apply (simp_all add: minus_mult_right [symmetric])

   799   done

   800

   801 lemma mult_nonpos_nonpos:

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

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

   804

   805 lemma split_mult_pos_le:

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

   807   by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)

   808

   809 end

   810

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

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

   813

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

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

   816

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

   818 by(simp add:sgn_if)

   819

   820 class ordered_ring = ring + ordered_semiring

   821   + ordered_ab_group_add + abs_if

   822 begin

   823

   824 subclass pordered_ring ..

   825

   826 subclass pordered_ab_group_add_abs

   827 proof

   828   fix a b

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

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

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

   832      neg_less_eq_nonneg less_eq_neg_nonpos, auto intro: add_nonneg_nonneg,

   833       auto intro!: less_imp_le add_neg_neg)

   834 qed (auto simp add: abs_if less_eq_neg_nonpos neg_equal_zero)

   835

   836 end

   837

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

   839    Basically, ordered_ring + no_zero_divisors = ordered_ring_strict.

   840  *)

   841 class ordered_ring_strict = ring + ordered_semiring_strict

   842   + ordered_ab_group_add + abs_if

   843 begin

   844

   845 subclass ordered_ring ..

   846

   847 lemma mult_strict_left_mono_neg:

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

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

   850   apply (simp_all add: minus_mult_left [symmetric])

   851   done

   852

   853 lemma mult_strict_right_mono_neg:

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

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

   856   apply (simp_all add: minus_mult_right [symmetric])

   857   done

   858

   859 lemma mult_neg_neg:

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

   861   by (drule mult_strict_right_mono_neg, auto)

   862

   863 subclass ring_no_zero_divisors

   864 proof

   865   fix a b

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

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

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

   869   proof (cases "a < 0")

   870     case True note A' = this

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

   872       case True with A'

   873       show ?thesis by (auto dest: mult_neg_neg)

   874     next

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

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

   877     qed

   878   next

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

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

   881       case True with A'

   882       show ?thesis by (auto dest: mult_strict_right_mono_neg)

   883     next

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

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

   886     qed

   887   qed

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

   889 qed

   890

   891 lemma zero_less_mult_iff:

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

   893   apply (auto simp add: mult_pos_pos mult_neg_neg)

   894   apply (simp_all add: not_less le_less)

   895   apply (erule disjE) apply assumption defer

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

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

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

   899   apply (drule sym) apply simp

   900   apply (blast dest: zero_less_mult_pos)

   901   apply (blast dest: zero_less_mult_pos2)

   902   done

   903

   904 lemma zero_le_mult_iff:

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

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

   907

   908 lemma mult_less_0_iff:

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

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

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

   912   done

   913

   914 lemma mult_le_0_iff:

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

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

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

   918   done

   919

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

   921   by (simp add: zero_le_mult_iff linear)

   922

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

   924   by (simp add: not_less)

   925

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

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

   928

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

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

   931

   932 lemma mult_less_cancel_right_disj:

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

   934   apply (cases "c = 0")

   935   apply (auto simp add: neq_iff mult_strict_right_mono

   936                       mult_strict_right_mono_neg)

   937   apply (auto simp add: not_less

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

   939                       not_le [symmetric, of a])

   940   apply (erule_tac [!] notE)

   941   apply (auto simp add: less_imp_le mult_right_mono

   942                       mult_right_mono_neg)

   943   done

   944

   945 lemma mult_less_cancel_left_disj:

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

   947   apply (cases "c = 0")

   948   apply (auto simp add: neq_iff mult_strict_left_mono

   949                       mult_strict_left_mono_neg)

   950   apply (auto simp add: not_less

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

   952                       not_le [symmetric, of a])

   953   apply (erule_tac [!] notE)

   954   apply (auto simp add: less_imp_le mult_left_mono

   955                       mult_left_mono_neg)

   956   done

   957

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

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

   960

   961 lemma mult_less_cancel_right:

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

   963   using mult_less_cancel_right_disj [of a c b] by auto

   964

   965 lemma mult_less_cancel_left:

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

   967   using mult_less_cancel_left_disj [of c a b] by auto

   968

   969 lemma mult_le_cancel_right:

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

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

   972

   973 lemma mult_le_cancel_left:

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

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

   976

   977 end

   978

   979 text{*This list of rewrites simplifies ring terms by multiplying

   980 everything out and bringing sums and products into a canonical form

   981 (by ordered rewriting). As a result it decides ring equalities but

   982 also helps with inequalities. *}

   983 lemmas ring_simps = group_simps ring_distribs

   984

   985

   986 class pordered_comm_ring = comm_ring + pordered_comm_semiring

   987 begin

   988

   989 subclass pordered_ring ..

   990 subclass pordered_cancel_comm_semiring ..

   991

   992 end

   993

   994 class ordered_semidom = comm_semiring_1_cancel + ordered_comm_semiring_strict +

   995   (*previously ordered_semiring*)

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

   997 begin

   998

   999 lemma pos_add_strict:

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

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

  1002

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

  1004   by (rule zero_less_one [THEN less_imp_le])

  1005

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

  1007   by (simp add: not_le)

  1008

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

  1010   by (simp add: not_less)

  1011

  1012 lemma less_1_mult:

  1013   assumes "1 < m" and "1 < n"

  1014   shows "1 < m * n"

  1015   using assms mult_strict_mono [of 1 m 1 n]

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

  1017

  1018 end

  1019

  1020 class ordered_idom = comm_ring_1 +

  1021   ordered_comm_semiring_strict + ordered_ab_group_add +

  1022   abs_if + sgn_if

  1023   (*previously ordered_ring*)

  1024 begin

  1025

  1026 subclass ordered_ring_strict ..

  1027 subclass pordered_comm_ring ..

  1028 subclass idom ..

  1029

  1030 subclass ordered_semidom

  1031 proof

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

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

  1034 qed

  1035

  1036 lemma linorder_neqE_ordered_idom:

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

  1038   using assms by (rule neqE)

  1039

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

  1041

  1042 lemma mult_le_cancel_right1:

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

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

  1045

  1046 lemma mult_le_cancel_right2:

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

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

  1049

  1050 lemma mult_le_cancel_left1:

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

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

  1053

  1054 lemma mult_le_cancel_left2:

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

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

  1057

  1058 lemma mult_less_cancel_right1:

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

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

  1061

  1062 lemma mult_less_cancel_right2:

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

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

  1065

  1066 lemma mult_less_cancel_left1:

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

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

  1069

  1070 lemma mult_less_cancel_left2:

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

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

  1073

  1074 lemma sgn_sgn [simp]:

  1075   "sgn (sgn a) = sgn a"

  1076   unfolding sgn_if by simp

  1077

  1078 lemma sgn_0_0:

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

  1080   unfolding sgn_if by simp

  1081

  1082 lemma sgn_1_pos:

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

  1084   unfolding sgn_if by (simp add: neg_equal_zero)

  1085

  1086 lemma sgn_1_neg:

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

  1088   unfolding sgn_if by (auto simp add: equal_neg_zero)

  1089

  1090 lemma sgn_times:

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

  1092   by (auto simp add: sgn_if zero_less_mult_iff)

  1093

  1094 end

  1095

  1096 class ordered_field = field + ordered_idom

  1097

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

  1099

  1100 lemmas mult_compare_simps =

  1101     mult_le_cancel_right mult_le_cancel_left

  1102     mult_le_cancel_right1 mult_le_cancel_right2

  1103     mult_le_cancel_left1 mult_le_cancel_left2

  1104     mult_less_cancel_right mult_less_cancel_left

  1105     mult_less_cancel_right1 mult_less_cancel_right2

  1106     mult_less_cancel_left1 mult_less_cancel_left2

  1107     mult_cancel_right mult_cancel_left

  1108     mult_cancel_right1 mult_cancel_right2

  1109     mult_cancel_left1 mult_cancel_left2

  1110

  1111 -- {* FIXME continue localization here *}

  1112

  1113 lemma inverse_nonzero_iff_nonzero [simp]:

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

  1115 by (force dest: inverse_zero_imp_zero)

  1116

  1117 lemma inverse_minus_eq [simp]:

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

  1119 proof cases

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

  1121 next

  1122   assume "a\<noteq>0"

  1123   thus ?thesis by (simp add: nonzero_inverse_minus_eq)

  1124 qed

  1125

  1126 lemma inverse_eq_imp_eq:

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

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

  1129  apply (force dest!: inverse_zero_imp_zero

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

  1131 apply (force dest!: nonzero_inverse_eq_imp_eq)

  1132 done

  1133

  1134 lemma inverse_eq_iff_eq [simp]:

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

  1136 by (force dest!: inverse_eq_imp_eq)

  1137

  1138 lemma inverse_inverse_eq [simp]:

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

  1140   proof cases

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

  1142   next

  1143     assume "a\<noteq>0"

  1144     thus ?thesis by (simp add: nonzero_inverse_inverse_eq)

  1145   qed

  1146

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

  1148       the right-hand side.*}

  1149 lemma inverse_mult_distrib [simp]:

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

  1151   proof cases

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

  1153     thus ?thesis

  1154       by (simp add: nonzero_inverse_mult_distrib mult_commute)

  1155   next

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

  1157     thus ?thesis

  1158       by force

  1159   qed

  1160

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

  1162 lemma inverse_add:

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

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

  1165 by (simp add: division_ring_inverse_add mult_ac)

  1166

  1167 lemma inverse_divide [simp]:

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

  1169 by (simp add: divide_inverse mult_commute)

  1170

  1171

  1172 subsection {* Calculations with fractions *}

  1173

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

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

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

  1177

  1178 lemma nonzero_mult_divide_mult_cancel_left[simp,noatp]:

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

  1180 proof -

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

  1182     by (simp add: divide_inverse nonzero_inverse_mult_distrib)

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

  1184     by (simp only: mult_ac)

  1185   also have "... =  a * inverse b"

  1186     by simp

  1187     finally show ?thesis

  1188     by (simp add: divide_inverse)

  1189 qed

  1190

  1191 lemma mult_divide_mult_cancel_left:

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

  1193 apply (cases "b = 0")

  1194 apply (simp_all add: nonzero_mult_divide_mult_cancel_left)

  1195 done

  1196

  1197 lemma nonzero_mult_divide_mult_cancel_right [noatp]:

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

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

  1200

  1201 lemma mult_divide_mult_cancel_right:

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

  1203 apply (cases "b = 0")

  1204 apply (simp_all add: nonzero_mult_divide_mult_cancel_right)

  1205 done

  1206

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

  1208 by (simp add: divide_inverse)

  1209

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

  1211 by (simp add: divide_inverse mult_assoc)

  1212

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

  1214 by (simp add: divide_inverse mult_ac)

  1215

  1216 lemmas times_divide_eq = times_divide_eq_right times_divide_eq_left

  1217

  1218 lemma divide_divide_eq_right [simp,noatp]:

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

  1220 by (simp add: divide_inverse mult_ac)

  1221

  1222 lemma divide_divide_eq_left [simp,noatp]:

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

  1224 by (simp add: divide_inverse mult_assoc)

  1225

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

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

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

  1229 apply (erule ssubst)

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

  1231 apply (erule ssubst)

  1232 apply (rule add_divide_distrib [THEN sym])

  1233 apply (subst mult_commute)

  1234 apply (erule nonzero_mult_divide_mult_cancel_left [THEN sym])

  1235 apply assumption

  1236 apply (erule nonzero_mult_divide_mult_cancel_right [THEN sym])

  1237 apply assumption

  1238 done

  1239

  1240

  1241 subsubsection{*Special Cancellation Simprules for Division*}

  1242

  1243 lemma mult_divide_mult_cancel_left_if[simp,noatp]:

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

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

  1246 by (simp add: mult_divide_mult_cancel_left)

  1247

  1248 lemma nonzero_mult_divide_cancel_right[simp,noatp]:

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

  1250 using nonzero_mult_divide_mult_cancel_right[of 1 b a] by simp

  1251

  1252 lemma nonzero_mult_divide_cancel_left[simp,noatp]:

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

  1254 using nonzero_mult_divide_mult_cancel_left[of 1 a b] by simp

  1255

  1256

  1257 lemma nonzero_divide_mult_cancel_right[simp,noatp]:

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

  1259 using nonzero_mult_divide_mult_cancel_right[of a b 1] by simp

  1260

  1261 lemma nonzero_divide_mult_cancel_left[simp,noatp]:

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

  1263 using nonzero_mult_divide_mult_cancel_left[of b a 1] by simp

  1264

  1265

  1266 lemma nonzero_mult_divide_mult_cancel_left2[simp,noatp]:

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

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

  1269

  1270 lemma nonzero_mult_divide_mult_cancel_right2[simp,noatp]:

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

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

  1273

  1274

  1275 subsection {* Division and Unary Minus *}

  1276

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

  1278 by (simp add: divide_inverse)

  1279

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

  1281 by (simp add: divide_inverse nonzero_inverse_minus_eq)

  1282

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

  1284 by (simp add: divide_inverse nonzero_inverse_minus_eq)

  1285

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

  1287 by (simp add: divide_inverse)

  1288

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

  1290 by (simp add: divide_inverse)

  1291

  1292

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

  1294 lemmas divide_minus_left = minus_divide_left [symmetric]

  1295 lemmas divide_minus_right = minus_divide_right [symmetric]

  1296 declare divide_minus_left [simp]   divide_minus_right [simp]

  1297

  1298 lemma minus_divide_divide [simp]:

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

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

  1301 apply (simp add: nonzero_minus_divide_divide)

  1302 done

  1303

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

  1305 by (simp add: diff_minus add_divide_distrib)

  1306

  1307 lemma add_divide_eq_iff:

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

  1309 by(simp add:add_divide_distrib nonzero_mult_divide_cancel_left)

  1310

  1311 lemma divide_add_eq_iff:

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

  1313 by(simp add:add_divide_distrib nonzero_mult_divide_cancel_left)

  1314

  1315 lemma diff_divide_eq_iff:

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

  1317 by(simp add:diff_divide_distrib nonzero_mult_divide_cancel_left)

  1318

  1319 lemma divide_diff_eq_iff:

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

  1321 by(simp add:diff_divide_distrib nonzero_mult_divide_cancel_left)

  1322

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

  1324 proof -

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

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

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

  1328   finally show ?thesis .

  1329 qed

  1330

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

  1332 proof -

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

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

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

  1336   finally show ?thesis .

  1337 qed

  1338

  1339 lemma eq_divide_eq:

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

  1341 by (simp add: nonzero_eq_divide_eq)

  1342

  1343 lemma divide_eq_eq:

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

  1345 by (force simp add: nonzero_divide_eq_eq)

  1346

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

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

  1349   by (subst divide_eq_eq, simp)

  1350

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

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

  1353   by (subst eq_divide_eq, simp)

  1354

  1355

  1356 lemmas field_eq_simps = ring_simps

  1357   (* pull / out*)

  1358   add_divide_eq_iff divide_add_eq_iff

  1359   diff_divide_eq_iff divide_diff_eq_iff

  1360   (* multiply eqn *)

  1361   nonzero_eq_divide_eq nonzero_divide_eq_eq

  1362 (* is added later:

  1363   times_divide_eq_left times_divide_eq_right

  1364 *)

  1365

  1366 text{*An example:*}

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

  1368 shows "\<lbrakk>a\<noteq>b; c\<noteq>d; e\<noteq>f \<rbrakk> \<Longrightarrow> ((a-b)*(c-d)*(e-f))/((c-d)*(e-f)*(a-b)) = 1"

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

  1370  apply(simp add:field_eq_simps)

  1371 apply(simp)

  1372 done

  1373

  1374

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

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

  1377 by (simp add:field_eq_simps times_divide_eq)

  1378

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

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

  1381 by (simp add:field_eq_simps times_divide_eq)

  1382

  1383

  1384 subsection {* Ordered Fields *}

  1385

  1386 lemma positive_imp_inverse_positive:

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

  1388 proof -

  1389   have "0 < a * inverse a"

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

  1391   thus "0 < inverse a"

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

  1393 qed

  1394

  1395 lemma negative_imp_inverse_negative:

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

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

  1398     simp add: nonzero_inverse_minus_eq order_less_imp_not_eq)

  1399

  1400 lemma inverse_le_imp_le:

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

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

  1403 proof (rule classical)

  1404   assume "~ b \<le> a"

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

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

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

  1408     by (simp add: apos invle order_less_imp_le mult_left_mono)

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

  1410     by (simp add: bpos order_less_imp_le mult_right_mono)

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

  1412 qed

  1413

  1414 lemma inverse_positive_imp_positive:

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

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

  1417 proof -

  1418   have "0 < inverse (inverse a)"

  1419     using inv_gt_0 by (rule positive_imp_inverse_positive)

  1420   thus "0 < a"

  1421     using nz by (simp add: nonzero_inverse_inverse_eq)

  1422 qed

  1423

  1424 lemma inverse_positive_iff_positive [simp]:

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

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

  1427 apply (blast intro: inverse_positive_imp_positive positive_imp_inverse_positive)

  1428 done

  1429

  1430 lemma inverse_negative_imp_negative:

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

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

  1433 proof -

  1434   have "inverse (inverse a) < 0"

  1435     using inv_less_0 by (rule negative_imp_inverse_negative)

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

  1437 qed

  1438

  1439 lemma inverse_negative_iff_negative [simp]:

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

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

  1442 apply (blast intro: inverse_negative_imp_negative negative_imp_inverse_negative)

  1443 done

  1444

  1445 lemma inverse_nonnegative_iff_nonnegative [simp]:

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

  1447 by (simp add: linorder_not_less [symmetric])

  1448

  1449 lemma inverse_nonpositive_iff_nonpositive [simp]:

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

  1451 by (simp add: linorder_not_less [symmetric])

  1452

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

  1454 proof

  1455   fix x::'a

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

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

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

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

  1460 qed

  1461

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

  1463 proof

  1464   fix x::'a

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

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

  1467   have "1 + x > x" by simp

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

  1469 qed

  1470

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

  1472

  1473 lemma less_imp_inverse_less:

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

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

  1476 proof (rule ccontr)

  1477   assume "~ inverse b < inverse a"

  1478   hence "inverse a \<le> inverse b"

  1479     by (simp add: linorder_not_less)

  1480   hence "~ (a < b)"

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

  1482   thus False

  1483     by (rule notE [OF _ less])

  1484 qed

  1485

  1486 lemma inverse_less_imp_less:

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

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

  1489 apply (force dest!: inverse_le_imp_le nonzero_inverse_eq_imp_eq)

  1490 done

  1491

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

  1493 lemma inverse_less_iff_less [simp,noatp]:

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

  1495 by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less)

  1496

  1497 lemma le_imp_inverse_le:

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

  1499 by (force simp add: order_le_less less_imp_inverse_less)

  1500

  1501 lemma inverse_le_iff_le [simp,noatp]:

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

  1503 by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le)

  1504

  1505

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

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

  1508 lemma inverse_le_imp_le_neg:

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

  1510 apply (rule classical)

  1511 apply (subgoal_tac "a < 0")

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

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

  1514 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)

  1515 done

  1516

  1517 lemma less_imp_inverse_less_neg:

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

  1519 apply (subgoal_tac "a < 0")

  1520  prefer 2 apply (blast intro: order_less_trans)

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

  1522 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)

  1523 done

  1524

  1525 lemma inverse_less_imp_less_neg:

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

  1527 apply (rule classical)

  1528 apply (subgoal_tac "a < 0")

  1529  prefer 2

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

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

  1532 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)

  1533 done

  1534

  1535 lemma inverse_less_iff_less_neg [simp,noatp]:

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

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

  1538 apply (simp del: inverse_less_iff_less

  1539             add: order_less_imp_not_eq nonzero_inverse_minus_eq)

  1540 done

  1541

  1542 lemma le_imp_inverse_le_neg:

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

  1544 by (force simp add: order_le_less less_imp_inverse_less_neg)

  1545

  1546 lemma inverse_le_iff_le_neg [simp,noatp]:

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

  1548 by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg)

  1549

  1550

  1551 subsection{*Inverses and the Number One*}

  1552

  1553 lemma one_less_inverse_iff:

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

  1555 proof cases

  1556   assume "0 < x"

  1557     with inverse_less_iff_less [OF zero_less_one, of x]

  1558     show ?thesis by simp

  1559 next

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

  1561   have "~ (1 < inverse x)"

  1562   proof

  1563     assume "1 < inverse x"

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

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

  1566     finally show False by auto

  1567   qed

  1568   with notless show ?thesis by simp

  1569 qed

  1570

  1571 lemma inverse_eq_1_iff [simp]:

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

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

  1574

  1575 lemma one_le_inverse_iff:

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

  1577 by (force simp add: order_le_less one_less_inverse_iff zero_less_one

  1578                     eq_commute [of 1])

  1579

  1580 lemma inverse_less_1_iff:

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

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

  1583

  1584 lemma inverse_le_1_iff:

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

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

  1587

  1588

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

  1590

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

  1592 proof -

  1593   assume less: "0<c"

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

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

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

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

  1598   finally show ?thesis .

  1599 qed

  1600

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

  1602 proof -

  1603   assume less: "c<0"

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

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

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

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

  1608   finally show ?thesis .

  1609 qed

  1610

  1611 lemma le_divide_eq:

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

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

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

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

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

  1617 apply (force simp add: pos_le_divide_eq neg_le_divide_eq linorder_neq_iff)

  1618 done

  1619

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

  1621 proof -

  1622   assume less: "0<c"

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

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

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

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

  1627   finally show ?thesis .

  1628 qed

  1629

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

  1631 proof -

  1632   assume less: "c<0"

  1633   hence "(b/c \<le> a) = (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_eq [OF less] divide_inverse mult_assoc)

  1637   finally show ?thesis .

  1638 qed

  1639

  1640 lemma divide_le_eq:

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

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

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

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

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

  1646 apply (force simp add: pos_divide_le_eq neg_divide_le_eq linorder_neq_iff)

  1647 done

  1648

  1649 lemma pos_less_divide_eq:

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

  1651 proof -

  1652   assume less: "0<c"

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

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

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

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

  1657   finally show ?thesis .

  1658 qed

  1659

  1660 lemma neg_less_divide_eq:

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

  1662 proof -

  1663   assume less: "c<0"

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

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

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

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

  1668   finally show ?thesis .

  1669 qed

  1670

  1671 lemma less_divide_eq:

  1672   "(a < b/c) =

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

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

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

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

  1677 apply (force simp add: pos_less_divide_eq neg_less_divide_eq linorder_neq_iff)

  1678 done

  1679

  1680 lemma pos_divide_less_eq:

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

  1682 proof -

  1683   assume less: "0<c"

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

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

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

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

  1688   finally show ?thesis .

  1689 qed

  1690

  1691 lemma neg_divide_less_eq:

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

  1693 proof -

  1694   assume less: "c<0"

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

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

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

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

  1699   finally show ?thesis .

  1700 qed

  1701

  1702 lemma divide_less_eq:

  1703   "(b/c < a) =

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

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

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

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

  1708 apply (force simp add: pos_divide_less_eq neg_divide_less_eq linorder_neq_iff)

  1709 done

  1710

  1711

  1712 subsection{*Field simplification*}

  1713

  1714 text{* Lemmas @{text field_simps} multiply with denominators in

  1715 in(equations) if they can be proved to be non-zero (for equations) or

  1716 positive/negative (for inequations). *}

  1717

  1718 lemmas field_simps = field_eq_simps

  1719   (* multiply ineqn *)

  1720   pos_divide_less_eq neg_divide_less_eq

  1721   pos_less_divide_eq neg_less_divide_eq

  1722   pos_divide_le_eq neg_divide_le_eq

  1723   pos_le_divide_eq neg_le_divide_eq

  1724

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

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

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

  1728 explosions. *}

  1729

  1730 lemmas sign_simps = group_simps

  1731   zero_less_mult_iff  mult_less_0_iff

  1732

  1733 (* Only works once linear arithmetic is installed:

  1734 text{*An example:*}

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

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

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

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

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

  1740  prefer 2 apply(simp add:sign_simps)

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

  1742  prefer 2 apply(simp add:sign_simps)

  1743 apply(simp add:field_simps)

  1744 done

  1745 *)

  1746

  1747

  1748 subsection{*Division and Signs*}

  1749

  1750 lemma zero_less_divide_iff:

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

  1752 by (simp add: divide_inverse zero_less_mult_iff)

  1753

  1754 lemma divide_less_0_iff:

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

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

  1757 by (simp add: divide_inverse mult_less_0_iff)

  1758

  1759 lemma zero_le_divide_iff:

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

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

  1762 by (simp add: divide_inverse zero_le_mult_iff)

  1763

  1764 lemma divide_le_0_iff:

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

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

  1767 by (simp add: divide_inverse mult_le_0_iff)

  1768

  1769 lemma divide_eq_0_iff [simp,noatp]:

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

  1771 by (simp add: divide_inverse)

  1772

  1773 lemma divide_pos_pos:

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

  1775 by(simp add:field_simps)

  1776

  1777

  1778 lemma divide_nonneg_pos:

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

  1780 by(simp add:field_simps)

  1781

  1782 lemma divide_neg_pos:

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

  1784 by(simp add:field_simps)

  1785

  1786 lemma divide_nonpos_pos:

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

  1788 by(simp add:field_simps)

  1789

  1790 lemma divide_pos_neg:

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

  1792 by(simp add:field_simps)

  1793

  1794 lemma divide_nonneg_neg:

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

  1796 by(simp add:field_simps)

  1797

  1798 lemma divide_neg_neg:

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

  1800 by(simp add:field_simps)

  1801

  1802 lemma divide_nonpos_neg:

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

  1804 by(simp add:field_simps)

  1805

  1806

  1807 subsection{*Cancellation Laws for Division*}

  1808

  1809 lemma divide_cancel_right [simp,noatp]:

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

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

  1812 apply (simp add: divide_inverse)

  1813 done

  1814

  1815 lemma divide_cancel_left [simp,noatp]:

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

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

  1818 apply (simp add: divide_inverse)

  1819 done

  1820

  1821

  1822 subsection {* Division and the Number One *}

  1823

  1824 text{*Simplify expressions equated with 1*}

  1825 lemma divide_eq_1_iff [simp,noatp]:

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

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

  1828 apply (simp add: right_inverse_eq)

  1829 done

  1830

  1831 lemma one_eq_divide_iff [simp,noatp]:

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

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

  1834

  1835 lemma zero_eq_1_divide_iff [simp,noatp]:

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

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

  1838 apply (auto simp add: nonzero_eq_divide_eq)

  1839 done

  1840

  1841 lemma one_divide_eq_0_iff [simp,noatp]:

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

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

  1844 apply (insert zero_neq_one [THEN not_sym])

  1845 apply (auto simp add: nonzero_divide_eq_eq)

  1846 done

  1847

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

  1849 lemmas zero_less_divide_1_iff = zero_less_divide_iff [of 1, simplified]

  1850 lemmas divide_less_0_1_iff = divide_less_0_iff [of 1, simplified]

  1851 lemmas zero_le_divide_1_iff = zero_le_divide_iff [of 1, simplified]

  1852 lemmas divide_le_0_1_iff = divide_le_0_iff [of 1, simplified]

  1853

  1854 declare zero_less_divide_1_iff [simp]

  1855 declare divide_less_0_1_iff [simp,noatp]

  1856 declare zero_le_divide_1_iff [simp]

  1857 declare divide_le_0_1_iff [simp,noatp]

  1858

  1859

  1860 subsection {* Ordering Rules for Division *}

  1861

  1862 lemma divide_strict_right_mono:

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

  1864 by (simp add: order_less_imp_not_eq2 divide_inverse mult_strict_right_mono

  1865               positive_imp_inverse_positive)

  1866

  1867 lemma divide_right_mono:

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

  1869 by (force simp add: divide_strict_right_mono order_le_less)

  1870

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

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

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

  1874 apply auto

  1875 done

  1876

  1877 lemma divide_strict_right_mono_neg:

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

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

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

  1881 done

  1882

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

  1884       have the same sign*}

  1885 lemma divide_strict_left_mono:

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

  1887 by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono)

  1888

  1889 lemma divide_left_mono:

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

  1891 by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_right_mono)

  1892

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

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

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

  1896   apply (auto simp add: mult_commute)

  1897 done

  1898

  1899 lemma divide_strict_left_mono_neg:

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

  1901 by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono_neg)

  1902

  1903

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

  1905

  1906 lemma le_divide_eq_1 [noatp]:

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

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

  1909 by (auto simp add: le_divide_eq)

  1910

  1911 lemma divide_le_eq_1 [noatp]:

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

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

  1914 by (auto simp add: divide_le_eq)

  1915

  1916 lemma less_divide_eq_1 [noatp]:

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

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

  1919 by (auto simp add: less_divide_eq)

  1920

  1921 lemma divide_less_eq_1 [noatp]:

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

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

  1924 by (auto simp add: divide_less_eq)

  1925

  1926

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

  1928

  1929 lemma le_divide_eq_1_pos [simp,noatp]:

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

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

  1932 by (auto simp add: le_divide_eq)

  1933

  1934 lemma le_divide_eq_1_neg [simp,noatp]:

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

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

  1937 by (auto simp add: le_divide_eq)

  1938

  1939 lemma divide_le_eq_1_pos [simp,noatp]:

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

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

  1942 by (auto simp add: divide_le_eq)

  1943

  1944 lemma divide_le_eq_1_neg [simp,noatp]:

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

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

  1947 by (auto simp add: divide_le_eq)

  1948

  1949 lemma less_divide_eq_1_pos [simp,noatp]:

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

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

  1952 by (auto simp add: less_divide_eq)

  1953

  1954 lemma less_divide_eq_1_neg [simp,noatp]:

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

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

  1957 by (auto simp add: less_divide_eq)

  1958

  1959 lemma divide_less_eq_1_pos [simp,noatp]:

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

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

  1962 by (auto simp add: divide_less_eq)

  1963

  1964 lemma divide_less_eq_1_neg [simp,noatp]:

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

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

  1967 by (auto simp add: divide_less_eq)

  1968

  1969 lemma eq_divide_eq_1 [simp,noatp]:

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

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

  1972 by (auto simp add: eq_divide_eq)

  1973

  1974 lemma divide_eq_eq_1 [simp,noatp]:

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

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

  1977 by (auto simp add: divide_eq_eq)

  1978

  1979

  1980 subsection {* Reasoning about inequalities with division *}

  1981

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

  1983     ==> x * y <= x"

  1984   by (auto simp add: mult_compare_simps);

  1985

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

  1987     ==> y * x <= x"

  1988   by (auto simp add: mult_compare_simps);

  1989

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

  1991     x / y <= z";

  1992   by (subst pos_divide_le_eq, assumption+);

  1993

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

  1995     z <= x / y"

  1996 by(simp add:field_simps)

  1997

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

  1999     x / y < z"

  2000 by(simp add:field_simps)

  2001

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

  2003     z < x / y"

  2004 by(simp add:field_simps)

  2005

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

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

  2008   apply (rule mult_imp_div_pos_le)

  2009   apply simp

  2010   apply (subst times_divide_eq_left)

  2011   apply (rule mult_imp_le_div_pos, assumption)

  2012   apply (rule mult_mono)

  2013   apply simp_all

  2014 done

  2015

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

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

  2018   apply (rule mult_imp_div_pos_less)

  2019   apply simp;

  2020   apply (subst times_divide_eq_left);

  2021   apply (rule mult_imp_less_div_pos, assumption)

  2022   apply (erule mult_less_le_imp_less)

  2023   apply simp_all

  2024 done

  2025

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

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

  2028   apply (rule mult_imp_div_pos_less)

  2029   apply simp_all

  2030   apply (subst times_divide_eq_left);

  2031   apply (rule mult_imp_less_div_pos, assumption)

  2032   apply (erule mult_le_less_imp_less)

  2033   apply simp_all

  2034 done

  2035

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

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

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

  2039   seem to need them.*}

  2040

  2041 declare times_divide_eq [simp]

  2042

  2043

  2044 subsection {* Ordered Fields are Dense *}

  2045

  2046 context ordered_semidom

  2047 begin

  2048

  2049 lemma less_add_one: "a < a + 1"

  2050 proof -

  2051   have "a + 0 < a + 1"

  2052     by (blast intro: zero_less_one add_strict_left_mono)

  2053   thus ?thesis by simp

  2054 qed

  2055

  2056 lemma zero_less_two: "0 < 1 + 1"

  2057   by (blast intro: less_trans zero_less_one less_add_one)

  2058

  2059 end

  2060

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

  2062 by (simp add: field_simps zero_less_two)

  2063

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

  2065 by (simp add: field_simps zero_less_two)

  2066

  2067 instance ordered_field < dense_linear_order

  2068 proof

  2069   fix x y :: 'a

  2070   have "x < x + 1" by simp

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

  2072   have "x - 1 < x" by simp

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

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

  2075 qed

  2076

  2077

  2078 subsection {* Absolute Value *}

  2079

  2080 context ordered_idom

  2081 begin

  2082

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

  2084   unfolding abs_if sgn_if by auto

  2085

  2086 end

  2087

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

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

  2090

  2091 class pordered_ring_abs = pordered_ring + pordered_ab_group_add_abs +

  2092   assumes abs_eq_mult:

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

  2094

  2095

  2096 class lordered_ring = pordered_ring + lordered_ab_group_add_abs

  2097 begin

  2098

  2099 subclass lordered_ab_group_add_meet ..

  2100 subclass lordered_ab_group_add_join ..

  2101

  2102 end

  2103

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

  2105 proof -

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

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

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

  2109     by (simp only: abs_prts[of a] abs_prts[of b] ring_simps)

  2110   {

  2111     fix u v :: 'a

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

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

  2114                       nprt a * pprt b + nprt a * nprt b"

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

  2116       apply (simp add: ring_simps)

  2117       done

  2118   }

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

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

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

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

  2123     apply (simp)

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

  2125     apply (rule addm2)

  2126     apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)

  2127     apply (rule addm)

  2128     apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)

  2129     done

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

  2131     apply (simp add:diff_def)

  2132     apply (rule_tac y=0 in order_trans)

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

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

  2135     done

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

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

  2138   show ?thesis

  2139     apply (rule abs_leI)

  2140     apply (simp add: i1)

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

  2142     done

  2143 qed

  2144

  2145 instance lordered_ring \<subseteq> pordered_ring_abs

  2146 proof

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

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

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

  2150 proof -

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

  2152     apply (auto)

  2153     apply (rule_tac split_mult_pos_le)

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

  2155     apply (simp)

  2156     apply (rule_tac split_mult_neg_le)

  2157     apply (insert prems)

  2158     apply (blast)

  2159     done

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

  2161     by (simp add: prts[symmetric])

  2162   show ?thesis

  2163   proof cases

  2164     assume "0 <= a * b"

  2165     then show ?thesis

  2166       apply (simp_all add: mulprts abs_prts)

  2167       apply (insert prems)

  2168       apply (auto simp add:

  2169 	ring_simps

  2170 	iffD1[OF zero_le_iff_zero_nprt] iffD1[OF le_zero_iff_zero_pprt]

  2171 	iffD1[OF le_zero_iff_pprt_id] iffD1[OF zero_le_iff_nprt_id])

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

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

  2174       done

  2175   next

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

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

  2178     then show ?thesis

  2179       apply (simp_all add: mulprts abs_prts)

  2180       apply (insert prems)

  2181       apply (auto simp add: ring_simps)

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

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

  2184       done

  2185   qed

  2186 qed

  2187 qed

  2188

  2189 instance ordered_idom \<subseteq> pordered_ring_abs

  2190 by default (auto simp add: abs_if not_less

  2191   equal_neg_zero neg_equal_zero mult_less_0_iff)

  2192

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

  2194   by (simp add: abs_eq_mult linorder_linear)

  2195

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

  2197   by (simp add: abs_if)

  2198

  2199 lemma nonzero_abs_inverse:

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

  2201 apply (auto simp add: linorder_neq_iff abs_if nonzero_inverse_minus_eq

  2202                       negative_imp_inverse_negative)

  2203 apply (blast intro: positive_imp_inverse_positive elim: order_less_asym)

  2204 done

  2205

  2206 lemma abs_inverse [simp]:

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

  2208       inverse (abs a)"

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

  2210 apply (simp add: nonzero_abs_inverse)

  2211 done

  2212

  2213 lemma nonzero_abs_divide:

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

  2215 by (simp add: divide_inverse abs_mult nonzero_abs_inverse)

  2216

  2217 lemma abs_divide [simp]:

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

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

  2220 apply (simp add: nonzero_abs_divide)

  2221 done

  2222

  2223 lemma abs_mult_less:

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

  2225 proof -

  2226   assume ac: "abs a < c"

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

  2228   assume "abs b < d"

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

  2230 qed

  2231

  2232 lemmas eq_minus_self_iff = equal_neg_zero

  2233

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

  2235   unfolding order_less_le less_eq_neg_nonpos equal_neg_zero ..

  2236

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

  2238 apply (simp add: order_less_le abs_le_iff)

  2239 apply (auto simp add: abs_if neg_less_eq_nonneg less_eq_neg_nonpos)

  2240 done

  2241

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

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

  2244   apply (subst abs_mult)

  2245   apply simp

  2246 done

  2247

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

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

  2250   apply (subst abs_divide)

  2251   apply (simp add: order_less_imp_le)

  2252 done

  2253

  2254

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

  2256

  2257 lemma mult_le_prts:

  2258   assumes

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

  2260   "a <= a2"

  2261   "b1 <= b"

  2262   "b <= b2"

  2263   shows

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

  2265 proof -

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

  2267     apply (subst prts[symmetric])+

  2268     apply simp

  2269     done

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

  2271     by (simp add: ring_simps)

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

  2273     by (simp_all add: prems mult_mono)

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

  2275   proof -

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

  2277       by (simp add: mult_left_mono prems)

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

  2279       by (simp add: mult_right_mono_neg prems)

  2280     ultimately show ?thesis

  2281       by simp

  2282   qed

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

  2284   proof -

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

  2286       by (simp add: mult_right_mono prems)

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

  2288       by (simp add: mult_left_mono_neg prems)

  2289     ultimately show ?thesis

  2290       by simp

  2291   qed

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

  2293   proof -

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

  2295       by (simp add: mult_left_mono_neg prems)

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

  2297       by (simp add: mult_right_mono_neg prems)

  2298     ultimately show ?thesis

  2299       by simp

  2300   qed

  2301   ultimately show ?thesis

  2302     by - (rule add_mono | simp)+

  2303 qed

  2304

  2305 lemma mult_ge_prts:

  2306   assumes

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

  2308   "a <= a2"

  2309   "b1 <= b"

  2310   "b <= b2"

  2311   shows

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

  2313 proof -

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

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

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

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

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

  2319     by (simp only: minus_le_iff)

  2320   then show ?thesis by simp

  2321 qed

  2322

  2323 end