src/HOL/Ring_and_Field.thy
 author wenzelm Fri Mar 28 19:43:54 2008 +0100 (2008-03-28) changeset 26462 dac4e2bce00d parent 26274 2bdb61a28971 child 27516 9a5d4a8d4aac permissions -rw-r--r--
avoid rebinding of existing facts;
     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 unfold_locales

    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 unfold_locales

    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 by intro_locales

    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 by intro_locales

    91

    92 end

    93

    94 class zero_neq_one = zero + one +

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

    96 begin

    97

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

    99   by (rule not_sym) (rule zero_neq_one)

   100

   101 end

   102

   103 class semiring_1 = zero_neq_one + semiring_0 + monoid_mult

   104

   105 class comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult

   106   (*previously almost_semiring*)

   107 begin

   108

   109 subclass semiring_1 by intro_locales

   110

   111 end

   112

   113 class no_zero_divisors = zero + times +

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

   115

   116 class semiring_1_cancel = semiring + comm_monoid_add + zero_neq_one

   117   + cancel_ab_semigroup_add + monoid_mult

   118 begin

   119

   120 subclass semiring_0_cancel by intro_locales

   121

   122 subclass semiring_1 by intro_locales

   123

   124 end

   125

   126 class comm_semiring_1_cancel = comm_semiring + comm_monoid_add + comm_monoid_mult

   127   + zero_neq_one + cancel_ab_semigroup_add

   128 begin

   129

   130 subclass semiring_1_cancel by intro_locales

   131 subclass comm_semiring_0_cancel by intro_locales

   132 subclass comm_semiring_1 by intro_locales

   133

   134 end

   135

   136 class ring = semiring + ab_group_add

   137 begin

   138

   139 subclass semiring_0_cancel by intro_locales

   140

   141 text {* Distribution rules *}

   142

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

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

   145

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

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

   148

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

   150   by (simp add: minus_mult_left [symmetric] minus_mult_right [symmetric])

   151

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

   153   by (simp add: minus_mult_left [symmetric] minus_mult_right [symmetric])

   154

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

   156   by (simp add: right_distrib diff_minus

   157     minus_mult_left [symmetric] minus_mult_right [symmetric])

   158

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

   160   by (simp add: left_distrib diff_minus

   161     minus_mult_left [symmetric] minus_mult_right [symmetric])

   162

   163 lemmas ring_distribs =

   164   right_distrib left_distrib left_diff_distrib right_diff_distrib

   165

   166 lemmas ring_simps =

   167   add_ac

   168   add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2

   169   diff_eq_eq eq_diff_eq diff_minus [symmetric] uminus_add_conv_diff

   170   ring_distribs

   171

   172 lemma eq_add_iff1:

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

   174   by (simp add: ring_simps)

   175

   176 lemma eq_add_iff2:

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

   178   by (simp add: ring_simps)

   179

   180 end

   181

   182 lemmas ring_distribs =

   183   right_distrib left_distrib left_diff_distrib right_diff_distrib

   184

   185 class comm_ring = comm_semiring + ab_group_add

   186 begin

   187

   188 subclass ring by intro_locales

   189 subclass comm_semiring_0 by intro_locales

   190

   191 end

   192

   193 class ring_1 = ring + zero_neq_one + monoid_mult

   194 begin

   195

   196 subclass semiring_1_cancel by intro_locales

   197

   198 end

   199

   200 class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult

   201   (*previously ring*)

   202 begin

   203

   204 subclass ring_1 by intro_locales

   205 subclass comm_semiring_1_cancel by intro_locales

   206

   207 end

   208

   209 class ring_no_zero_divisors = ring + no_zero_divisors

   210 begin

   211

   212 lemma mult_eq_0_iff [simp]:

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

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

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

   216     then show ?thesis using no_zero_divisors by simp

   217 next

   218   case True then show ?thesis by auto

   219 qed

   220

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

   222 lemma mult_cancel_right [simp, noatp]:

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

   224 proof -

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

   226     by (simp add: ring_distribs right_minus_eq)

   227   thus ?thesis

   228     by (simp add: disj_commute right_minus_eq)

   229 qed

   230

   231 lemma mult_cancel_left [simp, noatp]:

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

   233 proof -

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

   235     by (simp add: ring_distribs right_minus_eq)

   236   thus ?thesis

   237     by (simp add: right_minus_eq)

   238 qed

   239

   240 end

   241

   242 class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors

   243 begin

   244

   245 lemma mult_cancel_right1 [simp]:

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

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

   248

   249 lemma mult_cancel_right2 [simp]:

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

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

   252

   253 lemma mult_cancel_left1 [simp]:

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

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

   256

   257 lemma mult_cancel_left2 [simp]:

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

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

   260

   261 end

   262

   263 class idom = comm_ring_1 + no_zero_divisors

   264 begin

   265

   266 subclass ring_1_no_zero_divisors by intro_locales

   267

   268 end

   269

   270 class division_ring = ring_1 + inverse +

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

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

   273 begin

   274

   275 subclass ring_1_no_zero_divisors

   276 proof unfold_locales

   277   fix a b :: 'a

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

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

   280   proof

   281     assume ab: "a * b = 0"

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

   283       by simp

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

   285       by (simp only: mult_assoc)

   286     also have "\<dots> = 1"

   287       using a b by simp

   288     finally show False

   289       by simp

   290   qed

   291 qed

   292

   293 lemma nonzero_imp_inverse_nonzero:

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

   295 proof

   296   assume ianz: "inverse a = 0"

   297   assume "a \<noteq> 0"

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

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

   300   finally have "1 = 0" .

   301   thus False by (simp add: eq_commute)

   302 qed

   303

   304 lemma inverse_zero_imp_zero:

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

   306 apply (rule classical)

   307 apply (drule nonzero_imp_inverse_nonzero)

   308 apply auto

   309 done

   310

   311 lemma nonzero_inverse_minus_eq:

   312   assumes "a \<noteq> 0"

   313   shows "inverse (- a) = - inverse a"

   314 proof -

   315   have "- a * inverse (- a) = - a * - inverse a"

   316     using assms by simp

   317   then show ?thesis unfolding mult_cancel_left using assms by simp

   318 qed

   319

   320 lemma nonzero_inverse_inverse_eq:

   321   assumes "a \<noteq> 0"

   322   shows "inverse (inverse a) = a"

   323 proof -

   324   have "(inverse (inverse a) * inverse a) * a = a"

   325     using assms by (simp add: nonzero_imp_inverse_nonzero)

   326   then show ?thesis using assms by (simp add: mult_assoc)

   327 qed

   328

   329 lemma nonzero_inverse_eq_imp_eq:

   330   assumes inveq: "inverse a = inverse b"

   331     and anz:  "a \<noteq> 0"

   332     and bnz:  "b \<noteq> 0"

   333   shows "a = b"

   334 proof -

   335   have "a * inverse b = a * inverse a"

   336     by (simp add: inveq)

   337   hence "(a * inverse b) * b = (a * inverse a) * b"

   338     by simp

   339   then show "a = b"

   340     by (simp add: mult_assoc anz bnz)

   341 qed

   342

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

   344 proof -

   345   have "inverse 1 * 1 = 1"

   346     by (rule left_inverse) (rule one_neq_zero)

   347   then show ?thesis by simp

   348 qed

   349

   350 lemma inverse_unique:

   351   assumes ab: "a * b = 1"

   352   shows "inverse a = b"

   353 proof -

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

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

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

   357 qed

   358

   359 lemma nonzero_inverse_mult_distrib:

   360   assumes anz: "a \<noteq> 0"

   361     and bnz: "b \<noteq> 0"

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

   363 proof -

   364   have "inverse (a * b) * (a * b) * inverse b = inverse b"

   365     by (simp add: anz bnz)

   366   hence "inverse (a * b) * a = inverse b"

   367     by (simp add: mult_assoc bnz)

   368   hence "inverse (a * b) * a * inverse a = inverse b * inverse a"

   369     by simp

   370   thus ?thesis

   371     by (simp add: mult_assoc anz)

   372 qed

   373

   374 lemma division_ring_inverse_add:

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

   376   by (simp add: ring_simps mult_assoc)

   377

   378 lemma division_ring_inverse_diff:

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

   380   by (simp add: ring_simps mult_assoc)

   381

   382 end

   383

   384 class field = comm_ring_1 + inverse +

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

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

   387 begin

   388

   389 subclass division_ring

   390 proof unfold_locales

   391   fix a :: 'a

   392   assume "a \<noteq> 0"

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

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

   395 qed

   396

   397 subclass idom by intro_locales

   398

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

   400 proof

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

   402   {

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

   404     also assume "a / b = 1"

   405     finally show "a = b" by simp

   406   next

   407     assume "a = b"

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

   409   }

   410 qed

   411

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

   413   by (simp add: divide_inverse)

   414

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

   416   by (simp add: divide_inverse)

   417

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

   419   by (simp add: divide_inverse)

   420

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

   422   by (simp add: divide_inverse)

   423

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

   425   by (simp add: divide_inverse ring_distribs)

   426

   427 end

   428

   429 class division_by_zero = zero + inverse +

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

   431

   432 lemma divide_zero [simp]:

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

   434   by (simp add: divide_inverse)

   435

   436 lemma divide_self_if [simp]:

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

   438   by (simp add: divide_self)

   439

   440 class mult_mono = times + zero + ord +

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

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

   443

   444 class pordered_semiring = mult_mono + semiring_0 + pordered_ab_semigroup_add

   445 begin

   446

   447 lemma mult_mono:

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

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

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

   451 apply (erule mult_left_mono, assumption)

   452 done

   453

   454 lemma mult_mono':

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

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

   457 apply (rule mult_mono)

   458 apply (fast intro: order_trans)+

   459 done

   460

   461 end

   462

   463 class pordered_cancel_semiring = mult_mono + pordered_ab_semigroup_add

   464   + semiring + comm_monoid_add + cancel_ab_semigroup_add

   465 begin

   466

   467 subclass semiring_0_cancel by intro_locales

   468 subclass pordered_semiring by intro_locales

   469

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

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

   472

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

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

   475

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

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

   478

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

   480   by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)

   481

   482 end

   483

   484 class ordered_semiring = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add + mult_mono

   485 begin

   486

   487 subclass pordered_cancel_semiring by intro_locales

   488

   489 subclass pordered_comm_monoid_add by intro_locales

   490

   491 lemma mult_left_less_imp_less:

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

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

   494

   495 lemma mult_right_less_imp_less:

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

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

   498

   499 end

   500

   501 class ordered_semiring_strict = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add +

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

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

   504 begin

   505

   506 subclass semiring_0_cancel by intro_locales

   507

   508 subclass ordered_semiring

   509 proof unfold_locales

   510   fix a b c :: 'a

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

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

   513     unfolding le_less

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

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

   516     unfolding le_less

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

   518 qed

   519

   520 lemma mult_left_le_imp_le:

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

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

   523

   524 lemma mult_right_le_imp_le:

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

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

   527

   528 lemma mult_pos_pos:

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

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

   531

   532 lemma mult_pos_neg:

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

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

   535

   536 lemma mult_pos_neg2:

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

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

   539

   540 lemma zero_less_mult_pos:

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

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

   543  apply (auto simp add: le_less not_less)

   544 apply (drule_tac mult_pos_neg [of a b])

   545  apply (auto dest: less_not_sym)

   546 done

   547

   548 lemma zero_less_mult_pos2:

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

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

   551  apply (auto simp add: le_less not_less)

   552 apply (drule_tac mult_pos_neg2 [of a b])

   553  apply (auto dest: less_not_sym)

   554 done

   555

   556 text{*Strict monotonicity in both arguments*}

   557 lemma mult_strict_mono:

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

   559   shows "a * c < b * d"

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

   561   apply (simp add: mult_pos_pos)

   562   apply (erule mult_strict_right_mono [THEN less_trans])

   563   apply (force simp add: le_less)

   564   apply (erule mult_strict_left_mono, assumption)

   565   done

   566

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

   568 lemma mult_strict_mono':

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

   570   shows "a * c < b * d"

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

   572

   573 lemma mult_less_le_imp_less:

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

   575   shows "a * c < b * d"

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

   577   apply (erule less_le_trans)

   578   apply (erule mult_left_mono)

   579   apply simp

   580   apply (erule mult_strict_right_mono)

   581   apply assumption

   582   done

   583

   584 lemma mult_le_less_imp_less:

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

   586   shows "a * c < b * d"

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

   588   apply (erule le_less_trans)

   589   apply (erule mult_strict_left_mono)

   590   apply simp

   591   apply (erule mult_right_mono)

   592   apply simp

   593   done

   594

   595 lemma mult_less_imp_less_left:

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

   597   shows "a < b"

   598 proof (rule ccontr)

   599   assume "\<not>  a < b"

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

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

   602   with this and less show False

   603     by (simp add: not_less [symmetric])

   604 qed

   605

   606 lemma mult_less_imp_less_right:

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

   608   shows "a < b"

   609 proof (rule ccontr)

   610   assume "\<not> a < b"

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

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

   613   with this and less show False

   614     by (simp add: not_less [symmetric])

   615 qed

   616

   617 end

   618

   619 class mult_mono1 = times + zero + ord +

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

   621

   622 class pordered_comm_semiring = comm_semiring_0

   623   + pordered_ab_semigroup_add + mult_mono1

   624 begin

   625

   626 subclass pordered_semiring

   627 proof unfold_locales

   628   fix a b c :: 'a

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

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

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

   632 qed

   633

   634 end

   635

   636 class pordered_cancel_comm_semiring = comm_semiring_0_cancel

   637   + pordered_ab_semigroup_add + mult_mono1

   638 begin

   639

   640 subclass pordered_comm_semiring by intro_locales

   641 subclass pordered_cancel_semiring by intro_locales

   642

   643 end

   644

   645 class ordered_comm_semiring_strict = comm_semiring_0 + ordered_cancel_ab_semigroup_add +

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

   647 begin

   648

   649 subclass ordered_semiring_strict

   650 proof unfold_locales

   651   fix a b c :: 'a

   652   assume "a < b" "0 < c"

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

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

   655 qed

   656

   657 subclass pordered_cancel_comm_semiring

   658 proof unfold_locales

   659   fix a b c :: 'a

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

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

   662     unfolding le_less

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

   664 qed

   665

   666 end

   667

   668 class pordered_ring = ring + pordered_cancel_semiring

   669 begin

   670

   671 subclass pordered_ab_group_add by intro_locales

   672

   673 lemmas ring_simps = ring_simps group_simps

   674

   675 lemma less_add_iff1:

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

   677   by (simp add: ring_simps)

   678

   679 lemma less_add_iff2:

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

   681   by (simp add: ring_simps)

   682

   683 lemma le_add_iff1:

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

   685   by (simp add: ring_simps)

   686

   687 lemma le_add_iff2:

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

   689   by (simp add: ring_simps)

   690

   691 lemma mult_left_mono_neg:

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

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

   694   apply (simp_all add: minus_mult_left [symmetric])

   695   done

   696

   697 lemma mult_right_mono_neg:

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

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

   700   apply (simp_all add: minus_mult_right [symmetric])

   701   done

   702

   703 lemma mult_nonpos_nonpos:

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

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

   706

   707 lemma split_mult_pos_le:

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

   709   by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)

   710

   711 end

   712

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

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

   715

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

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

   718

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

   720 by(simp add:sgn_if)

   721

   722 class ordered_ring = ring + ordered_semiring

   723   + ordered_ab_group_add + abs_if

   724 begin

   725

   726 subclass pordered_ring by intro_locales

   727

   728 subclass pordered_ab_group_add_abs

   729 proof unfold_locales

   730   fix a b

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

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

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

   734      neg_less_eq_nonneg less_eq_neg_nonpos, auto intro: add_nonneg_nonneg,

   735       auto intro!: less_imp_le add_neg_neg)

   736 qed (auto simp add: abs_if less_eq_neg_nonpos neg_equal_zero)

   737

   738 end

   739

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

   741    Basically, ordered_ring + no_zero_divisors = ordered_ring_strict.

   742  *)

   743 class ordered_ring_strict = ring + ordered_semiring_strict

   744   + ordered_ab_group_add + abs_if

   745 begin

   746

   747 subclass ordered_ring by intro_locales

   748

   749 lemma mult_strict_left_mono_neg:

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

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

   752   apply (simp_all add: minus_mult_left [symmetric])

   753   done

   754

   755 lemma mult_strict_right_mono_neg:

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

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

   758   apply (simp_all add: minus_mult_right [symmetric])

   759   done

   760

   761 lemma mult_neg_neg:

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

   763   by (drule mult_strict_right_mono_neg, auto)

   764

   765 subclass ring_no_zero_divisors

   766 proof unfold_locales

   767   fix a b

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

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

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

   771   proof (cases "a < 0")

   772     case True note A' = this

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

   774       case True with A'

   775       show ?thesis by (auto dest: mult_neg_neg)

   776     next

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

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

   779     qed

   780   next

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

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

   783       case True with A'

   784       show ?thesis by (auto dest: mult_strict_right_mono_neg)

   785     next

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

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

   788     qed

   789   qed

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

   791 qed

   792

   793 lemma zero_less_mult_iff:

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

   795   apply (auto simp add: mult_pos_pos mult_neg_neg)

   796   apply (simp_all add: not_less le_less)

   797   apply (erule disjE) apply assumption defer

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

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

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

   801   apply (drule sym) apply simp

   802   apply (blast dest: zero_less_mult_pos)

   803   apply (blast dest: zero_less_mult_pos2)

   804   done

   805

   806 lemma zero_le_mult_iff:

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

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

   809

   810 lemma mult_less_0_iff:

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

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

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

   814   done

   815

   816 lemma mult_le_0_iff:

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

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

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

   820   done

   821

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

   823   by (simp add: zero_le_mult_iff linear)

   824

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

   826   by (simp add: not_less)

   827

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

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

   830

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

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

   833

   834 lemma mult_less_cancel_right_disj:

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

   836   apply (cases "c = 0")

   837   apply (auto simp add: neq_iff mult_strict_right_mono

   838                       mult_strict_right_mono_neg)

   839   apply (auto simp add: not_less

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

   841                       not_le [symmetric, of a])

   842   apply (erule_tac [!] notE)

   843   apply (auto simp add: less_imp_le mult_right_mono

   844                       mult_right_mono_neg)

   845   done

   846

   847 lemma mult_less_cancel_left_disj:

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

   849   apply (cases "c = 0")

   850   apply (auto simp add: neq_iff mult_strict_left_mono

   851                       mult_strict_left_mono_neg)

   852   apply (auto simp add: not_less

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

   854                       not_le [symmetric, of a])

   855   apply (erule_tac [!] notE)

   856   apply (auto simp add: less_imp_le mult_left_mono

   857                       mult_left_mono_neg)

   858   done

   859

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

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

   862

   863 lemma mult_less_cancel_right:

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

   865   using mult_less_cancel_right_disj [of a c b] by auto

   866

   867 lemma mult_less_cancel_left:

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

   869   using mult_less_cancel_left_disj [of c a b] by auto

   870

   871 lemma mult_le_cancel_right:

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

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

   874

   875 lemma mult_le_cancel_left:

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

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

   878

   879 end

   880

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

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

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

   884 also helps with inequalities. *}

   885 lemmas ring_simps = group_simps ring_distribs

   886

   887

   888 class pordered_comm_ring = comm_ring + pordered_comm_semiring

   889 begin

   890

   891 subclass pordered_ring by intro_locales

   892 subclass pordered_cancel_comm_semiring by intro_locales

   893

   894 end

   895

   896 class ordered_semidom = comm_semiring_1_cancel + ordered_comm_semiring_strict +

   897   (*previously ordered_semiring*)

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

   899 begin

   900

   901 lemma pos_add_strict:

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

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

   904

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

   906   by (rule zero_less_one [THEN less_imp_le])

   907

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

   909   by (simp add: not_le)

   910

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

   912   by (simp add: not_less)

   913

   914 lemma less_1_mult:

   915   assumes "1 < m" and "1 < n"

   916   shows "1 < m * n"

   917   using assms mult_strict_mono [of 1 m 1 n]

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

   919

   920 end

   921

   922 class ordered_idom = comm_ring_1 +

   923   ordered_comm_semiring_strict + ordered_ab_group_add +

   924   abs_if + sgn_if

   925   (*previously ordered_ring*)

   926 begin

   927

   928 subclass ordered_ring_strict by intro_locales

   929 subclass pordered_comm_ring by intro_locales

   930 subclass idom by intro_locales

   931

   932 subclass ordered_semidom

   933 proof unfold_locales

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

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

   936 qed

   937

   938 lemma linorder_neqE_ordered_idom:

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

   940   using assms by (rule neqE)

   941

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

   943

   944 lemma mult_le_cancel_right1:

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

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

   947

   948 lemma mult_le_cancel_right2:

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

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

   951

   952 lemma mult_le_cancel_left1:

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

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

   955

   956 lemma mult_le_cancel_left2:

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

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

   959

   960 lemma mult_less_cancel_right1:

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

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

   963

   964 lemma mult_less_cancel_right2:

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

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

   967

   968 lemma mult_less_cancel_left1:

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

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

   971

   972 lemma mult_less_cancel_left2:

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

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

   975

   976 end

   977

   978 class ordered_field = field + ordered_idom

   979

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

   981

   982 lemmas mult_compare_simps =

   983     mult_le_cancel_right mult_le_cancel_left

   984     mult_le_cancel_right1 mult_le_cancel_right2

   985     mult_le_cancel_left1 mult_le_cancel_left2

   986     mult_less_cancel_right mult_less_cancel_left

   987     mult_less_cancel_right1 mult_less_cancel_right2

   988     mult_less_cancel_left1 mult_less_cancel_left2

   989     mult_cancel_right mult_cancel_left

   990     mult_cancel_right1 mult_cancel_right2

   991     mult_cancel_left1 mult_cancel_left2

   992

   993 -- {* FIXME continue localization here *}

   994

   995 lemma inverse_nonzero_iff_nonzero [simp]:

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

   997 by (force dest: inverse_zero_imp_zero)

   998

   999 lemma inverse_minus_eq [simp]:

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

  1001 proof cases

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

  1003 next

  1004   assume "a\<noteq>0"

  1005   thus ?thesis by (simp add: nonzero_inverse_minus_eq)

  1006 qed

  1007

  1008 lemma inverse_eq_imp_eq:

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

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

  1011  apply (force dest!: inverse_zero_imp_zero

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

  1013 apply (force dest!: nonzero_inverse_eq_imp_eq)

  1014 done

  1015

  1016 lemma inverse_eq_iff_eq [simp]:

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

  1018 by (force dest!: inverse_eq_imp_eq)

  1019

  1020 lemma inverse_inverse_eq [simp]:

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

  1022   proof cases

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

  1024   next

  1025     assume "a\<noteq>0"

  1026     thus ?thesis by (simp add: nonzero_inverse_inverse_eq)

  1027   qed

  1028

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

  1030       the right-hand side.*}

  1031 lemma inverse_mult_distrib [simp]:

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

  1033   proof cases

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

  1035     thus ?thesis

  1036       by (simp add: nonzero_inverse_mult_distrib mult_commute)

  1037   next

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

  1039     thus ?thesis

  1040       by force

  1041   qed

  1042

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

  1044 lemma inverse_add:

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

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

  1047 by (simp add: division_ring_inverse_add mult_ac)

  1048

  1049 lemma inverse_divide [simp]:

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

  1051 by (simp add: divide_inverse mult_commute)

  1052

  1053

  1054 subsection {* Calculations with fractions *}

  1055

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

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

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

  1059

  1060 lemma nonzero_mult_divide_mult_cancel_left[simp,noatp]:

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

  1062 proof -

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

  1064     by (simp add: divide_inverse nonzero_inverse_mult_distrib)

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

  1066     by (simp only: mult_ac)

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

  1068     by simp

  1069     finally show ?thesis

  1070     by (simp add: divide_inverse)

  1071 qed

  1072

  1073 lemma mult_divide_mult_cancel_left:

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

  1075 apply (cases "b = 0")

  1076 apply (simp_all add: nonzero_mult_divide_mult_cancel_left)

  1077 done

  1078

  1079 lemma nonzero_mult_divide_mult_cancel_right [noatp]:

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

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

  1082

  1083 lemma mult_divide_mult_cancel_right:

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

  1085 apply (cases "b = 0")

  1086 apply (simp_all add: nonzero_mult_divide_mult_cancel_right)

  1087 done

  1088

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

  1090 by (simp add: divide_inverse)

  1091

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

  1093 by (simp add: divide_inverse mult_assoc)

  1094

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

  1096 by (simp add: divide_inverse mult_ac)

  1097

  1098 lemmas times_divide_eq = times_divide_eq_right times_divide_eq_left

  1099

  1100 lemma divide_divide_eq_right [simp,noatp]:

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

  1102 by (simp add: divide_inverse mult_ac)

  1103

  1104 lemma divide_divide_eq_left [simp,noatp]:

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

  1106 by (simp add: divide_inverse mult_assoc)

  1107

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

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

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

  1111 apply (erule ssubst)

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

  1113 apply (erule ssubst)

  1114 apply (rule add_divide_distrib [THEN sym])

  1115 apply (subst mult_commute)

  1116 apply (erule nonzero_mult_divide_mult_cancel_left [THEN sym])

  1117 apply assumption

  1118 apply (erule nonzero_mult_divide_mult_cancel_right [THEN sym])

  1119 apply assumption

  1120 done

  1121

  1122

  1123 subsubsection{*Special Cancellation Simprules for Division*}

  1124

  1125 lemma mult_divide_mult_cancel_left_if[simp,noatp]:

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

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

  1128 by (simp add: mult_divide_mult_cancel_left)

  1129

  1130 lemma nonzero_mult_divide_cancel_right[simp,noatp]:

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

  1132 using nonzero_mult_divide_mult_cancel_right[of 1 b a] by simp

  1133

  1134 lemma nonzero_mult_divide_cancel_left[simp,noatp]:

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

  1136 using nonzero_mult_divide_mult_cancel_left[of 1 a b] by simp

  1137

  1138

  1139 lemma nonzero_divide_mult_cancel_right[simp,noatp]:

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

  1141 using nonzero_mult_divide_mult_cancel_right[of a b 1] by simp

  1142

  1143 lemma nonzero_divide_mult_cancel_left[simp,noatp]:

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

  1145 using nonzero_mult_divide_mult_cancel_left[of b a 1] by simp

  1146

  1147

  1148 lemma nonzero_mult_divide_mult_cancel_left2[simp,noatp]:

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

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

  1151

  1152 lemma nonzero_mult_divide_mult_cancel_right2[simp,noatp]:

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

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

  1155

  1156

  1157 subsection {* Division and Unary Minus *}

  1158

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

  1160 by (simp add: divide_inverse minus_mult_left)

  1161

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

  1163 by (simp add: divide_inverse nonzero_inverse_minus_eq minus_mult_right)

  1164

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

  1166 by (simp add: divide_inverse nonzero_inverse_minus_eq)

  1167

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

  1169 by (simp add: divide_inverse minus_mult_left [symmetric])

  1170

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

  1172 by (simp add: divide_inverse minus_mult_right [symmetric])

  1173

  1174

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

  1176 lemmas divide_minus_left = minus_divide_left [symmetric]

  1177 lemmas divide_minus_right = minus_divide_right [symmetric]

  1178 declare divide_minus_left [simp]   divide_minus_right [simp]

  1179

  1180 text{*Also, extract signs from products*}

  1181 lemmas mult_minus_left = minus_mult_left [symmetric]

  1182 lemmas mult_minus_right = minus_mult_right [symmetric]

  1183 declare mult_minus_left [simp]   mult_minus_right [simp]

  1184

  1185 lemma minus_divide_divide [simp]:

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

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

  1188 apply (simp add: nonzero_minus_divide_divide)

  1189 done

  1190

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

  1192 by (simp add: diff_minus add_divide_distrib)

  1193

  1194 lemma add_divide_eq_iff:

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

  1196 by(simp add:add_divide_distrib nonzero_mult_divide_cancel_left)

  1197

  1198 lemma divide_add_eq_iff:

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

  1200 by(simp add:add_divide_distrib nonzero_mult_divide_cancel_left)

  1201

  1202 lemma diff_divide_eq_iff:

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

  1204 by(simp add:diff_divide_distrib nonzero_mult_divide_cancel_left)

  1205

  1206 lemma divide_diff_eq_iff:

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

  1208 by(simp add:diff_divide_distrib nonzero_mult_divide_cancel_left)

  1209

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

  1211 proof -

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

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

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

  1215   finally show ?thesis .

  1216 qed

  1217

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

  1219 proof -

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

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

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

  1223   finally show ?thesis .

  1224 qed

  1225

  1226 lemma eq_divide_eq:

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

  1228 by (simp add: nonzero_eq_divide_eq)

  1229

  1230 lemma divide_eq_eq:

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

  1232 by (force simp add: nonzero_divide_eq_eq)

  1233

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

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

  1236   by (subst divide_eq_eq, simp)

  1237

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

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

  1240   by (subst eq_divide_eq, simp)

  1241

  1242

  1243 lemmas field_eq_simps = ring_simps

  1244   (* pull / out*)

  1245   add_divide_eq_iff divide_add_eq_iff

  1246   diff_divide_eq_iff divide_diff_eq_iff

  1247   (* multiply eqn *)

  1248   nonzero_eq_divide_eq nonzero_divide_eq_eq

  1249 (* is added later:

  1250   times_divide_eq_left times_divide_eq_right

  1251 *)

  1252

  1253 text{*An example:*}

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

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

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

  1257  apply(simp add:field_eq_simps)

  1258 apply(simp)

  1259 done

  1260

  1261

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

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

  1264 by (simp add:field_eq_simps times_divide_eq)

  1265

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

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

  1268 by (simp add:field_eq_simps times_divide_eq)

  1269

  1270

  1271 subsection {* Ordered Fields *}

  1272

  1273 lemma positive_imp_inverse_positive:

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

  1275 proof -

  1276   have "0 < a * inverse a"

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

  1278   thus "0 < inverse a"

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

  1280 qed

  1281

  1282 lemma negative_imp_inverse_negative:

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

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

  1285     simp add: nonzero_inverse_minus_eq order_less_imp_not_eq)

  1286

  1287 lemma inverse_le_imp_le:

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

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

  1290 proof (rule classical)

  1291   assume "~ b \<le> a"

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

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

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

  1295     by (simp add: apos invle order_less_imp_le mult_left_mono)

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

  1297     by (simp add: bpos order_less_imp_le mult_right_mono)

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

  1299 qed

  1300

  1301 lemma inverse_positive_imp_positive:

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

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

  1304 proof -

  1305   have "0 < inverse (inverse a)"

  1306     using inv_gt_0 by (rule positive_imp_inverse_positive)

  1307   thus "0 < a"

  1308     using nz by (simp add: nonzero_inverse_inverse_eq)

  1309 qed

  1310

  1311 lemma inverse_positive_iff_positive [simp]:

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

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

  1314 apply (blast intro: inverse_positive_imp_positive positive_imp_inverse_positive)

  1315 done

  1316

  1317 lemma inverse_negative_imp_negative:

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

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

  1320 proof -

  1321   have "inverse (inverse a) < 0"

  1322     using inv_less_0 by (rule negative_imp_inverse_negative)

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

  1324 qed

  1325

  1326 lemma inverse_negative_iff_negative [simp]:

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

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

  1329 apply (blast intro: inverse_negative_imp_negative negative_imp_inverse_negative)

  1330 done

  1331

  1332 lemma inverse_nonnegative_iff_nonnegative [simp]:

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

  1334 by (simp add: linorder_not_less [symmetric])

  1335

  1336 lemma inverse_nonpositive_iff_nonpositive [simp]:

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

  1338 by (simp add: linorder_not_less [symmetric])

  1339

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

  1341 proof

  1342   fix x::'a

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

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

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

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

  1347 qed

  1348

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

  1350 proof

  1351   fix x::'a

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

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

  1354   have "1 + x > x" by simp

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

  1356 qed

  1357

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

  1359

  1360 lemma less_imp_inverse_less:

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

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

  1363 proof (rule ccontr)

  1364   assume "~ inverse b < inverse a"

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

  1366     by (simp add: linorder_not_less)

  1367   hence "~ (a < b)"

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

  1369   thus False

  1370     by (rule notE [OF _ less])

  1371 qed

  1372

  1373 lemma inverse_less_imp_less:

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

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

  1376 apply (force dest!: inverse_le_imp_le nonzero_inverse_eq_imp_eq)

  1377 done

  1378

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

  1380 lemma inverse_less_iff_less [simp,noatp]:

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

  1382 by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less)

  1383

  1384 lemma le_imp_inverse_le:

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

  1386 by (force simp add: order_le_less less_imp_inverse_less)

  1387

  1388 lemma inverse_le_iff_le [simp,noatp]:

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

  1390 by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le)

  1391

  1392

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

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

  1395 lemma inverse_le_imp_le_neg:

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

  1397 apply (rule classical)

  1398 apply (subgoal_tac "a < 0")

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

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

  1401 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)

  1402 done

  1403

  1404 lemma less_imp_inverse_less_neg:

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

  1406 apply (subgoal_tac "a < 0")

  1407  prefer 2 apply (blast intro: order_less_trans)

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

  1409 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)

  1410 done

  1411

  1412 lemma inverse_less_imp_less_neg:

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

  1414 apply (rule classical)

  1415 apply (subgoal_tac "a < 0")

  1416  prefer 2

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

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

  1419 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)

  1420 done

  1421

  1422 lemma inverse_less_iff_less_neg [simp,noatp]:

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

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

  1425 apply (simp del: inverse_less_iff_less

  1426             add: order_less_imp_not_eq nonzero_inverse_minus_eq)

  1427 done

  1428

  1429 lemma le_imp_inverse_le_neg:

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

  1431 by (force simp add: order_le_less less_imp_inverse_less_neg)

  1432

  1433 lemma inverse_le_iff_le_neg [simp,noatp]:

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

  1435 by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg)

  1436

  1437

  1438 subsection{*Inverses and the Number One*}

  1439

  1440 lemma one_less_inverse_iff:

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

  1442 proof cases

  1443   assume "0 < x"

  1444     with inverse_less_iff_less [OF zero_less_one, of x]

  1445     show ?thesis by simp

  1446 next

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

  1448   have "~ (1 < inverse x)"

  1449   proof

  1450     assume "1 < inverse x"

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

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

  1453     finally show False by auto

  1454   qed

  1455   with notless show ?thesis by simp

  1456 qed

  1457

  1458 lemma inverse_eq_1_iff [simp]:

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

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

  1461

  1462 lemma one_le_inverse_iff:

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

  1464 by (force simp add: order_le_less one_less_inverse_iff zero_less_one

  1465                     eq_commute [of 1])

  1466

  1467 lemma inverse_less_1_iff:

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

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

  1470

  1471 lemma inverse_le_1_iff:

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

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

  1474

  1475

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

  1477

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

  1479 proof -

  1480   assume less: "0<c"

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

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

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

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

  1485   finally show ?thesis .

  1486 qed

  1487

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

  1489 proof -

  1490   assume less: "c<0"

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

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

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

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

  1495   finally show ?thesis .

  1496 qed

  1497

  1498 lemma le_divide_eq:

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

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

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

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

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

  1504 apply (force simp add: pos_le_divide_eq neg_le_divide_eq linorder_neq_iff)

  1505 done

  1506

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

  1508 proof -

  1509   assume less: "0<c"

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

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

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

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

  1514   finally show ?thesis .

  1515 qed

  1516

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

  1518 proof -

  1519   assume less: "c<0"

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

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

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

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

  1524   finally show ?thesis .

  1525 qed

  1526

  1527 lemma divide_le_eq:

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

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

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

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

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

  1533 apply (force simp add: pos_divide_le_eq neg_divide_le_eq linorder_neq_iff)

  1534 done

  1535

  1536 lemma pos_less_divide_eq:

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

  1538 proof -

  1539   assume less: "0<c"

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

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

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

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

  1544   finally show ?thesis .

  1545 qed

  1546

  1547 lemma neg_less_divide_eq:

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

  1549 proof -

  1550   assume less: "c<0"

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

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

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

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

  1555   finally show ?thesis .

  1556 qed

  1557

  1558 lemma less_divide_eq:

  1559   "(a < b/c) =

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

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

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

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

  1564 apply (force simp add: pos_less_divide_eq neg_less_divide_eq linorder_neq_iff)

  1565 done

  1566

  1567 lemma pos_divide_less_eq:

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

  1569 proof -

  1570   assume less: "0<c"

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

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

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

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

  1575   finally show ?thesis .

  1576 qed

  1577

  1578 lemma neg_divide_less_eq:

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

  1580 proof -

  1581   assume less: "c<0"

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

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

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

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

  1586   finally show ?thesis .

  1587 qed

  1588

  1589 lemma divide_less_eq:

  1590   "(b/c < a) =

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

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

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

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

  1595 apply (force simp add: pos_divide_less_eq neg_divide_less_eq linorder_neq_iff)

  1596 done

  1597

  1598

  1599 subsection{*Field simplification*}

  1600

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

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

  1603 positive/negative (for inequations). *}

  1604

  1605 lemmas field_simps = field_eq_simps

  1606   (* multiply ineqn *)

  1607   pos_divide_less_eq neg_divide_less_eq

  1608   pos_less_divide_eq neg_less_divide_eq

  1609   pos_divide_le_eq neg_divide_le_eq

  1610   pos_le_divide_eq neg_le_divide_eq

  1611

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

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

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

  1615 explosions. *}

  1616

  1617 lemmas sign_simps = group_simps

  1618   zero_less_mult_iff  mult_less_0_iff

  1619

  1620 (* Only works once linear arithmetic is installed:

  1621 text{*An example:*}

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

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

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

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

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

  1627  prefer 2 apply(simp add:sign_simps)

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

  1629  prefer 2 apply(simp add:sign_simps)

  1630 apply(simp add:field_simps)

  1631 done

  1632 *)

  1633

  1634

  1635 subsection{*Division and Signs*}

  1636

  1637 lemma zero_less_divide_iff:

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

  1639 by (simp add: divide_inverse zero_less_mult_iff)

  1640

  1641 lemma divide_less_0_iff:

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

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

  1644 by (simp add: divide_inverse mult_less_0_iff)

  1645

  1646 lemma zero_le_divide_iff:

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

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

  1649 by (simp add: divide_inverse zero_le_mult_iff)

  1650

  1651 lemma divide_le_0_iff:

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

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

  1654 by (simp add: divide_inverse mult_le_0_iff)

  1655

  1656 lemma divide_eq_0_iff [simp,noatp]:

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

  1658 by (simp add: divide_inverse)

  1659

  1660 lemma divide_pos_pos:

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

  1662 by(simp add:field_simps)

  1663

  1664

  1665 lemma divide_nonneg_pos:

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

  1667 by(simp add:field_simps)

  1668

  1669 lemma divide_neg_pos:

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

  1671 by(simp add:field_simps)

  1672

  1673 lemma divide_nonpos_pos:

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

  1675 by(simp add:field_simps)

  1676

  1677 lemma divide_pos_neg:

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

  1679 by(simp add:field_simps)

  1680

  1681 lemma divide_nonneg_neg:

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

  1683 by(simp add:field_simps)

  1684

  1685 lemma divide_neg_neg:

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

  1687 by(simp add:field_simps)

  1688

  1689 lemma divide_nonpos_neg:

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

  1691 by(simp add:field_simps)

  1692

  1693

  1694 subsection{*Cancellation Laws for Division*}

  1695

  1696 lemma divide_cancel_right [simp,noatp]:

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

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

  1699 apply (simp add: divide_inverse)

  1700 done

  1701

  1702 lemma divide_cancel_left [simp,noatp]:

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

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

  1705 apply (simp add: divide_inverse)

  1706 done

  1707

  1708

  1709 subsection {* Division and the Number One *}

  1710

  1711 text{*Simplify expressions equated with 1*}

  1712 lemma divide_eq_1_iff [simp,noatp]:

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

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

  1715 apply (simp add: right_inverse_eq)

  1716 done

  1717

  1718 lemma one_eq_divide_iff [simp,noatp]:

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

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

  1721

  1722 lemma zero_eq_1_divide_iff [simp,noatp]:

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

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

  1725 apply (auto simp add: nonzero_eq_divide_eq)

  1726 done

  1727

  1728 lemma one_divide_eq_0_iff [simp,noatp]:

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

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

  1731 apply (insert zero_neq_one [THEN not_sym])

  1732 apply (auto simp add: nonzero_divide_eq_eq)

  1733 done

  1734

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

  1736 lemmas zero_less_divide_1_iff = zero_less_divide_iff [of 1, simplified]

  1737 lemmas divide_less_0_1_iff = divide_less_0_iff [of 1, simplified]

  1738 lemmas zero_le_divide_1_iff = zero_le_divide_iff [of 1, simplified]

  1739 lemmas divide_le_0_1_iff = divide_le_0_iff [of 1, simplified]

  1740

  1741 declare zero_less_divide_1_iff [simp]

  1742 declare divide_less_0_1_iff [simp,noatp]

  1743 declare zero_le_divide_1_iff [simp]

  1744 declare divide_le_0_1_iff [simp,noatp]

  1745

  1746

  1747 subsection {* Ordering Rules for Division *}

  1748

  1749 lemma divide_strict_right_mono:

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

  1751 by (simp add: order_less_imp_not_eq2 divide_inverse mult_strict_right_mono

  1752               positive_imp_inverse_positive)

  1753

  1754 lemma divide_right_mono:

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

  1756 by (force simp add: divide_strict_right_mono order_le_less)

  1757

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

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

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

  1761 apply auto

  1762 done

  1763

  1764 lemma divide_strict_right_mono_neg:

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

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

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

  1768 done

  1769

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

  1771       have the same sign*}

  1772 lemma divide_strict_left_mono:

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

  1774 by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono)

  1775

  1776 lemma divide_left_mono:

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

  1778 by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_right_mono)

  1779

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

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

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

  1783   apply (auto simp add: mult_commute)

  1784 done

  1785

  1786 lemma divide_strict_left_mono_neg:

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

  1788 by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono_neg)

  1789

  1790

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

  1792

  1793 lemma le_divide_eq_1 [noatp]:

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

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

  1796 by (auto simp add: le_divide_eq)

  1797

  1798 lemma divide_le_eq_1 [noatp]:

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

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

  1801 by (auto simp add: divide_le_eq)

  1802

  1803 lemma less_divide_eq_1 [noatp]:

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

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

  1806 by (auto simp add: less_divide_eq)

  1807

  1808 lemma divide_less_eq_1 [noatp]:

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

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

  1811 by (auto simp add: divide_less_eq)

  1812

  1813

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

  1815

  1816 lemma le_divide_eq_1_pos [simp,noatp]:

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

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

  1819 by (auto simp add: le_divide_eq)

  1820

  1821 lemma le_divide_eq_1_neg [simp,noatp]:

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

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

  1824 by (auto simp add: le_divide_eq)

  1825

  1826 lemma divide_le_eq_1_pos [simp,noatp]:

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

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

  1829 by (auto simp add: divide_le_eq)

  1830

  1831 lemma divide_le_eq_1_neg [simp,noatp]:

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

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

  1834 by (auto simp add: divide_le_eq)

  1835

  1836 lemma less_divide_eq_1_pos [simp,noatp]:

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

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

  1839 by (auto simp add: less_divide_eq)

  1840

  1841 lemma less_divide_eq_1_neg [simp,noatp]:

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

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

  1844 by (auto simp add: less_divide_eq)

  1845

  1846 lemma divide_less_eq_1_pos [simp,noatp]:

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

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

  1849 by (auto simp add: divide_less_eq)

  1850

  1851 lemma divide_less_eq_1_neg [simp,noatp]:

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

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

  1854 by (auto simp add: divide_less_eq)

  1855

  1856 lemma eq_divide_eq_1 [simp,noatp]:

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

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

  1859 by (auto simp add: eq_divide_eq)

  1860

  1861 lemma divide_eq_eq_1 [simp,noatp]:

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

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

  1864 by (auto simp add: divide_eq_eq)

  1865

  1866

  1867 subsection {* Reasoning about inequalities with division *}

  1868

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

  1870     ==> x * y <= x"

  1871   by (auto simp add: mult_compare_simps);

  1872

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

  1874     ==> y * x <= x"

  1875   by (auto simp add: mult_compare_simps);

  1876

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

  1878     x / y <= z";

  1879   by (subst pos_divide_le_eq, assumption+);

  1880

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

  1882     z <= x / y"

  1883 by(simp add:field_simps)

  1884

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

  1886     x / y < z"

  1887 by(simp add:field_simps)

  1888

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

  1890     z < x / y"

  1891 by(simp add:field_simps)

  1892

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

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

  1895   apply (rule mult_imp_div_pos_le)

  1896   apply simp

  1897   apply (subst times_divide_eq_left)

  1898   apply (rule mult_imp_le_div_pos, assumption)

  1899   apply (rule mult_mono)

  1900   apply simp_all

  1901 done

  1902

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

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

  1905   apply (rule mult_imp_div_pos_less)

  1906   apply simp;

  1907   apply (subst times_divide_eq_left);

  1908   apply (rule mult_imp_less_div_pos, assumption)

  1909   apply (erule mult_less_le_imp_less)

  1910   apply simp_all

  1911 done

  1912

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

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

  1915   apply (rule mult_imp_div_pos_less)

  1916   apply simp_all

  1917   apply (subst times_divide_eq_left);

  1918   apply (rule mult_imp_less_div_pos, assumption)

  1919   apply (erule mult_le_less_imp_less)

  1920   apply simp_all

  1921 done

  1922

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

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

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

  1926   seem to need them.*}

  1927

  1928 declare times_divide_eq [simp]

  1929

  1930

  1931 subsection {* Ordered Fields are Dense *}

  1932

  1933 context ordered_semidom

  1934 begin

  1935

  1936 lemma less_add_one: "a < a + 1"

  1937 proof -

  1938   have "a + 0 < a + 1"

  1939     by (blast intro: zero_less_one add_strict_left_mono)

  1940   thus ?thesis by simp

  1941 qed

  1942

  1943 lemma zero_less_two: "0 < 1 + 1"

  1944   by (blast intro: less_trans zero_less_one less_add_one)

  1945

  1946 end

  1947

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

  1949 by (simp add: field_simps zero_less_two)

  1950

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

  1952 by (simp add: field_simps zero_less_two)

  1953

  1954 instance ordered_field < dense_linear_order

  1955 proof

  1956   fix x y :: 'a

  1957   have "x < x + 1" by simp

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

  1959   have "x - 1 < x" by simp

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

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

  1962 qed

  1963

  1964

  1965 subsection {* Absolute Value *}

  1966

  1967 context ordered_idom

  1968 begin

  1969

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

  1971   unfolding abs_if sgn_if by auto

  1972

  1973 end

  1974

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

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

  1977

  1978 class pordered_ring_abs = pordered_ring + pordered_ab_group_add_abs +

  1979   assumes abs_eq_mult:

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

  1981

  1982

  1983 class lordered_ring = pordered_ring + lordered_ab_group_add_abs

  1984 begin

  1985

  1986 subclass lordered_ab_group_add_meet by intro_locales

  1987 subclass lordered_ab_group_add_join by intro_locales

  1988

  1989 end

  1990

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

  1992 proof -

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

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

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

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

  1997   {

  1998     fix u v :: 'a

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

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

  2001                       nprt a * pprt b + nprt a * nprt b"

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

  2003       apply (simp add: ring_simps)

  2004       done

  2005   }

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

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

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

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

  2010     apply (simp)

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

  2012     apply (rule addm2)

  2013     apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)

  2014     apply (rule addm)

  2015     apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)

  2016     done

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

  2018     apply (simp add:diff_def)

  2019     apply (rule_tac y=0 in order_trans)

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

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

  2022     done

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

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

  2025   show ?thesis

  2026     apply (rule abs_leI)

  2027     apply (simp add: i1)

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

  2029     done

  2030 qed

  2031

  2032 instance lordered_ring \<subseteq> pordered_ring_abs

  2033 proof

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

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

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

  2037 proof -

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

  2039     apply (auto)

  2040     apply (rule_tac split_mult_pos_le)

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

  2042     apply (simp)

  2043     apply (rule_tac split_mult_neg_le)

  2044     apply (insert prems)

  2045     apply (blast)

  2046     done

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

  2048     by (simp add: prts[symmetric])

  2049   show ?thesis

  2050   proof cases

  2051     assume "0 <= a * b"

  2052     then show ?thesis

  2053       apply (simp_all add: mulprts abs_prts)

  2054       apply (insert prems)

  2055       apply (auto simp add:

  2056 	ring_simps

  2057 	iffD1[OF zero_le_iff_zero_nprt] iffD1[OF le_zero_iff_zero_pprt]

  2058 	iffD1[OF le_zero_iff_pprt_id] iffD1[OF zero_le_iff_nprt_id])

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

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

  2061       done

  2062   next

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

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

  2065     then show ?thesis

  2066       apply (simp_all add: mulprts abs_prts)

  2067       apply (insert prems)

  2068       apply (auto simp add: ring_simps)

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

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

  2071       done

  2072   qed

  2073 qed

  2074 qed

  2075

  2076 instance ordered_idom \<subseteq> pordered_ring_abs

  2077 by default (auto simp add: abs_if not_less

  2078   equal_neg_zero neg_equal_zero mult_less_0_iff)

  2079

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

  2081   by (simp add: abs_eq_mult linorder_linear)

  2082

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

  2084   by (simp add: abs_if)

  2085

  2086 lemma nonzero_abs_inverse:

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

  2088 apply (auto simp add: linorder_neq_iff abs_if nonzero_inverse_minus_eq

  2089                       negative_imp_inverse_negative)

  2090 apply (blast intro: positive_imp_inverse_positive elim: order_less_asym)

  2091 done

  2092

  2093 lemma abs_inverse [simp]:

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

  2095       inverse (abs a)"

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

  2097 apply (simp add: nonzero_abs_inverse)

  2098 done

  2099

  2100 lemma nonzero_abs_divide:

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

  2102 by (simp add: divide_inverse abs_mult nonzero_abs_inverse)

  2103

  2104 lemma abs_divide [simp]:

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

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

  2107 apply (simp add: nonzero_abs_divide)

  2108 done

  2109

  2110 lemma abs_mult_less:

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

  2112 proof -

  2113   assume ac: "abs a < c"

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

  2115   assume "abs b < d"

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

  2117 qed

  2118

  2119 lemmas eq_minus_self_iff = equal_neg_zero

  2120

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

  2122   unfolding order_less_le less_eq_neg_nonpos equal_neg_zero ..

  2123

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

  2125 apply (simp add: order_less_le abs_le_iff)

  2126 apply (auto simp add: abs_if neg_less_eq_nonneg less_eq_neg_nonpos)

  2127 done

  2128

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

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

  2131   apply (subst abs_mult)

  2132   apply simp

  2133 done

  2134

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

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

  2137   apply (subst abs_divide)

  2138   apply (simp add: order_less_imp_le)

  2139 done

  2140

  2141

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

  2143

  2144 lemma mult_le_prts:

  2145   assumes

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

  2147   "a <= a2"

  2148   "b1 <= b"

  2149   "b <= b2"

  2150   shows

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

  2152 proof -

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

  2154     apply (subst prts[symmetric])+

  2155     apply simp

  2156     done

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

  2158     by (simp add: ring_simps)

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

  2160     by (simp_all add: prems mult_mono)

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

  2162   proof -

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

  2164       by (simp add: mult_left_mono prems)

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

  2166       by (simp add: mult_right_mono_neg prems)

  2167     ultimately show ?thesis

  2168       by simp

  2169   qed

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

  2171   proof -

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

  2173       by (simp add: mult_right_mono prems)

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

  2175       by (simp add: mult_left_mono_neg prems)

  2176     ultimately show ?thesis

  2177       by simp

  2178   qed

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

  2180   proof -

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

  2182       by (simp add: mult_left_mono_neg prems)

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

  2184       by (simp add: mult_right_mono_neg prems)

  2185     ultimately show ?thesis

  2186       by simp

  2187   qed

  2188   ultimately show ?thesis

  2189     by - (rule add_mono | simp)+

  2190 qed

  2191

  2192 lemma mult_ge_prts:

  2193   assumes

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

  2195   "a <= a2"

  2196   "b1 <= b"

  2197   "b <= b2"

  2198   shows

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

  2200 proof -

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

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

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

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

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

  2206     by (simp only: minus_le_iff)

  2207   then show ?thesis by simp

  2208 qed

  2209

  2210 end