src/HOL/Ring_and_Field.thy
 author haftmann Fri Nov 02 18:52:58 2007 +0100 (2007-11-02) changeset 25267 1f745c599b5c parent 25238 ee73d4c33a88 child 25304 7491c00f0915 permissions -rw-r--r--
proper reinitialisation after subclass
     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 unfold_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 unfold_locales

    91

    92 end

    93

    94 class zero_neq_one = zero + one +

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

    96

    97 class semiring_1 = zero_neq_one + semiring_0 + monoid_mult

    98

    99 class comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult

   100   (*previously almost_semiring*)

   101 begin

   102

   103 subclass semiring_1 by unfold_locales

   104

   105 end

   106

   107 class no_zero_divisors = zero + times +

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

   109

   110 class semiring_1_cancel = semiring + comm_monoid_add + zero_neq_one

   111   + cancel_ab_semigroup_add + monoid_mult

   112 begin

   113

   114 subclass semiring_0_cancel by unfold_locales

   115

   116 subclass semiring_1 by unfold_locales

   117

   118 end

   119

   120 class comm_semiring_1_cancel = comm_semiring + comm_monoid_add + comm_monoid_mult

   121   + zero_neq_one + cancel_ab_semigroup_add

   122 begin

   123

   124 subclass semiring_1_cancel by unfold_locales

   125 subclass comm_semiring_0_cancel by unfold_locales

   126 subclass comm_semiring_1 by unfold_locales

   127

   128 end

   129

   130 class ring = semiring + ab_group_add

   131 begin

   132

   133 subclass semiring_0_cancel by unfold_locales

   134

   135 text {* Distribution rules *}

   136

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

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

   139

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

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

   142

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

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

   145

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

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

   148

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

   150   by (simp add: right_distrib diff_minus

   151     minus_mult_left [symmetric] minus_mult_right [symmetric])

   152

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

   154   by (simp add: left_distrib diff_minus

   155     minus_mult_left [symmetric] minus_mult_right [symmetric])

   156

   157 lemmas ring_distribs =

   158   right_distrib left_distrib left_diff_distrib right_diff_distrib

   159

   160 lemmas ring_simps =

   161   add_ac

   162   add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2

   163   diff_eq_eq eq_diff_eq diff_minus [symmetric] uminus_add_conv_diff

   164   ring_distribs

   165

   166 lemma eq_add_iff1:

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

   168   by (simp add: ring_simps)

   169

   170 lemma eq_add_iff2:

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

   172   by (simp add: ring_simps)

   173

   174 end

   175

   176 lemmas ring_distribs =

   177   right_distrib left_distrib left_diff_distrib right_diff_distrib

   178

   179 class comm_ring = comm_semiring + ab_group_add

   180 begin

   181

   182 subclass ring by unfold_locales

   183 subclass comm_semiring_0 by unfold_locales

   184

   185 end

   186

   187 class ring_1 = ring + zero_neq_one + monoid_mult

   188 begin

   189

   190 subclass semiring_1_cancel by unfold_locales

   191

   192 end

   193

   194 class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult

   195   (*previously ring*)

   196 begin

   197

   198 subclass ring_1 by unfold_locales

   199 subclass comm_semiring_1_cancel by unfold_locales

   200

   201 end

   202

   203 class ring_no_zero_divisors = ring + no_zero_divisors

   204 begin

   205

   206 lemma mult_eq_0_iff [simp]:

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

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

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

   210     then show ?thesis using no_zero_divisors by simp

   211 next

   212   case True then show ?thesis by auto

   213 qed

   214

   215 end

   216

   217 class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors

   218

   219 class idom = comm_ring_1 + no_zero_divisors

   220 begin

   221

   222 subclass ring_1_no_zero_divisors by unfold_locales

   223

   224 end

   225

   226 class division_ring = ring_1 + inverse +

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

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

   229 begin

   230

   231 subclass ring_1_no_zero_divisors

   232 proof unfold_locales

   233   fix a b :: 'a

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

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

   236   proof

   237     assume ab: "a * b = 0"

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

   239       by simp

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

   241       by (simp only: mult_assoc)

   242     also have "\<dots> = 1"

   243       using a b by simp

   244     finally show False

   245       by simp

   246   qed

   247 qed

   248

   249 end

   250

   251 class field = comm_ring_1 + inverse +

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

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

   254 begin

   255

   256 subclass division_ring

   257 proof unfold_locales

   258   fix a :: 'a

   259   assume "a \<noteq> 0"

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

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

   262 qed

   263

   264 subclass idom by unfold_locales

   265

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

   267 proof

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

   269   {

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

   271     also assume "a / b = 1"

   272     finally show "a = b" by simp

   273   next

   274     assume "a = b"

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

   276   }

   277 qed

   278

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

   280   by (simp add: divide_inverse)

   281

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

   283   by (simp add: divide_inverse)

   284

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

   286   by (simp add: divide_inverse)

   287

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

   289   by (simp add: divide_inverse)

   290

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

   292   by (simp add: divide_inverse ring_distribs)

   293

   294 end

   295

   296 class division_by_zero = zero + inverse +

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

   298

   299 lemma divide_zero [simp]:

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

   301   by (simp add: divide_inverse)

   302

   303 lemma divide_self_if [simp]:

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

   305   by (simp add: divide_self)

   306

   307 class mult_mono = times + zero + ord +

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

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

   310

   311 class pordered_semiring = mult_mono + semiring_0 + pordered_ab_semigroup_add

   312 begin

   313

   314 lemma mult_mono:

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

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

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

   318 apply (erule mult_left_mono, assumption)

   319 done

   320

   321 lemma mult_mono':

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

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

   324 apply (rule mult_mono)

   325 apply (fast intro: order_trans)+

   326 done

   327

   328 end

   329

   330 class pordered_cancel_semiring = mult_mono + pordered_ab_semigroup_add

   331   + semiring + comm_monoid_add + cancel_ab_semigroup_add

   332 begin

   333

   334 subclass semiring_0_cancel by unfold_locales

   335 subclass pordered_semiring by unfold_locales

   336

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

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

   339

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

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

   342

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

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

   345

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

   347   by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)

   348

   349 end

   350

   351 class ordered_semiring = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add + mult_mono

   352 begin

   353

   354 subclass pordered_cancel_semiring by unfold_locales

   355

   356 lemma mult_left_less_imp_less:

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

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

   359

   360 lemma mult_right_less_imp_less:

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

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

   363

   364 end

   365

   366 class ordered_semiring_strict = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add +

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

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

   369 begin

   370

   371 subclass semiring_0_cancel by unfold_locales

   372

   373 subclass ordered_semiring

   374 proof unfold_locales

   375   fix a b c :: 'a

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

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

   378     unfolding le_less

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

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

   381     unfolding le_less

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

   383 qed

   384

   385 lemma mult_left_le_imp_le:

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

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

   388

   389 lemma mult_right_le_imp_le:

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

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

   392

   393 lemma mult_pos_pos:

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

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

   396

   397 lemma mult_pos_neg:

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

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

   400

   401 lemma mult_pos_neg2:

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

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

   404

   405 lemma zero_less_mult_pos:

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

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

   408  apply (auto simp add: le_less not_less)

   409 apply (drule_tac mult_pos_neg [of a b])

   410  apply (auto dest: less_not_sym)

   411 done

   412

   413 lemma zero_less_mult_pos2:

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

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

   416  apply (auto simp add: le_less not_less)

   417 apply (drule_tac mult_pos_neg2 [of a b])

   418  apply (auto dest: less_not_sym)

   419 done

   420

   421 end

   422

   423 class mult_mono1 = times + zero + ord +

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

   425

   426 class pordered_comm_semiring = comm_semiring_0

   427   + pordered_ab_semigroup_add + mult_mono1

   428 begin

   429

   430 subclass pordered_semiring

   431 proof unfold_locales

   432   fix a b c :: 'a

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

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

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

   436 qed

   437

   438 end

   439

   440 class pordered_cancel_comm_semiring = comm_semiring_0_cancel

   441   + pordered_ab_semigroup_add + mult_mono1

   442 begin

   443

   444 subclass pordered_comm_semiring by unfold_locales

   445 subclass pordered_cancel_semiring by unfold_locales

   446

   447 end

   448

   449 class ordered_comm_semiring_strict = comm_semiring_0 + ordered_cancel_ab_semigroup_add +

   450   assumes mult_strict_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"

   451 begin

   452

   453 subclass ordered_semiring_strict

   454 proof unfold_locales

   455   fix a b c :: 'a

   456   assume "a < b" "0 < c"

   457   thus "c * a < c * b" by (rule mult_strict_mono)

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

   459 qed

   460

   461 subclass pordered_cancel_comm_semiring

   462 proof unfold_locales

   463   fix a b c :: 'a

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

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

   466     unfolding le_less

   467     using mult_strict_mono by (cases "c = 0") auto

   468 qed

   469

   470 end

   471

   472 class pordered_ring = ring + pordered_cancel_semiring

   473 begin

   474

   475 subclass pordered_ab_group_add by unfold_locales

   476

   477 lemmas ring_simps = ring_simps group_simps

   478

   479 lemma less_add_iff1:

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

   481   by (simp add: ring_simps)

   482

   483 lemma less_add_iff2:

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

   485   by (simp add: ring_simps)

   486

   487 lemma le_add_iff1:

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

   489   by (simp add: ring_simps)

   490

   491 lemma le_add_iff2:

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

   493   by (simp add: ring_simps)

   494

   495 lemma mult_left_mono_neg:

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

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

   498   apply (simp_all add: minus_mult_left [symmetric])

   499   done

   500

   501 lemma mult_right_mono_neg:

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

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

   504   apply (simp_all add: minus_mult_right [symmetric])

   505   done

   506

   507 lemma mult_nonpos_nonpos:

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

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

   510

   511 lemma split_mult_pos_le:

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

   513   by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)

   514

   515 end

   516

   517 class lordered_ring = pordered_ring + lordered_ab_group_abs

   518 begin

   519

   520 subclass lordered_ab_group_meet by unfold_locales

   521 subclass lordered_ab_group_join by unfold_locales

   522

   523 end

   524

   525 class abs_if = minus + ord + zero + abs +

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

   527

   528 class sgn_if = sgn + zero + one + minus + ord +

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

   530

   531 class ordered_ring = ring + ordered_semiring

   532   + lordered_ab_group + abs_if

   533   -- {*FIXME: should inherit from @{text ordered_ab_group_add} rather than

   534          @{text lordered_ab_group}*}

   535

   536 instance ordered_ring \<subseteq> lordered_ring

   537 proof

   538   fix x :: 'a

   539   show "\<bar>x\<bar> = sup x (- x)"

   540     by (simp only: abs_if sup_eq_if)

   541 qed

   542

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

   544    Basically, ordered_ring + no_zero_divisors = ordered_ring_strict.

   545  *)

   546 class ordered_ring_strict = ring + ordered_semiring_strict

   547   + lordered_ab_group + abs_if

   548   -- {*FIXME: should inherit from @{text ordered_ab_group_add} rather than

   549          @{text lordered_ab_group}*}

   550

   551 instance ordered_ring_strict \<subseteq> ordered_ring by intro_classes

   552

   553 context ordered_ring_strict

   554 begin

   555

   556 lemma mult_strict_left_mono_neg:

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

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

   559   apply (simp_all add: minus_mult_left [symmetric])

   560   done

   561

   562 lemma mult_strict_right_mono_neg:

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

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

   565   apply (simp_all add: minus_mult_right [symmetric])

   566   done

   567

   568 lemma mult_neg_neg:

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

   570   by (drule mult_strict_right_mono_neg, auto)

   571

   572 end

   573

   574 lemma zero_less_mult_iff:

   575   fixes a :: "'a::ordered_ring_strict"

   576   shows "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0"

   577   apply (auto simp add: le_less not_less mult_pos_pos mult_neg_neg)

   578   apply (blast dest: zero_less_mult_pos)

   579   apply (blast dest: zero_less_mult_pos2)

   580   done

   581

   582 instance ordered_ring_strict \<subseteq> ring_no_zero_divisors

   583 apply intro_classes

   584 apply (auto simp add: linorder_not_less order_le_less linorder_neq_iff)

   585 apply (force dest: mult_strict_right_mono_neg mult_strict_right_mono)+

   586 done

   587

   588 lemma zero_le_mult_iff:

   589      "((0::'a::ordered_ring_strict) \<le> a*b) = (0 \<le> a & 0 \<le> b | a \<le> 0 & b \<le> 0)"

   590 by (auto simp add: eq_commute [of 0] order_le_less linorder_not_less

   591                    zero_less_mult_iff)

   592

   593 lemma mult_less_0_iff:

   594      "(a*b < (0::'a::ordered_ring_strict)) = (0 < a & b < 0 | a < 0 & 0 < b)"

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

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

   597 done

   598

   599 lemma mult_le_0_iff:

   600      "(a*b \<le> (0::'a::ordered_ring_strict)) = (0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> b)"

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

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

   603 done

   604

   605 lemma zero_le_square[simp]: "(0::'a::ordered_ring_strict) \<le> a*a"

   606 by (simp add: zero_le_mult_iff linorder_linear)

   607

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

   609 by (simp add: not_less)

   610

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

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

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

   614 also helps with inequalities. *}

   615 lemmas ring_simps = group_simps ring_distribs

   616

   617

   618 class pordered_comm_ring = comm_ring + pordered_comm_semiring

   619 begin

   620

   621 subclass pordered_ring by unfold_locales

   622 subclass pordered_cancel_comm_semiring by unfold_locales

   623

   624 end

   625

   626 class ordered_semidom = comm_semiring_1_cancel + ordered_comm_semiring_strict +

   627   (*previously ordered_semiring*)

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

   629 begin

   630

   631 lemma pos_add_strict:

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

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

   634

   635 end

   636

   637 class ordered_idom =

   638   comm_ring_1 +

   639   ordered_comm_semiring_strict +

   640   lordered_ab_group +

   641   abs_if + sgn_if

   642   (*previously ordered_ring*)

   643

   644 instance ordered_idom \<subseteq> ordered_ring_strict ..

   645

   646 instance ordered_idom \<subseteq> pordered_comm_ring ..

   647

   648 class ordered_field = field + ordered_idom

   649

   650 lemma linorder_neqE_ordered_idom:

   651   fixes x y :: "'a :: ordered_idom"

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

   653   using assms by (rule linorder_neqE)

   654

   655 -- {* FIXME continue localization here *}

   656

   657

   658 text{*Proving axiom @{text zero_less_one} makes all @{text ordered_semidom}

   659       theorems available to members of @{term ordered_idom} *}

   660

   661 instance ordered_idom \<subseteq> ordered_semidom

   662 proof

   663   have "(0::'a) \<le> 1*1" by (rule zero_le_square)

   664   thus "(0::'a) < 1" by (simp add: order_le_less)

   665 qed

   666

   667 instance ordered_idom \<subseteq> idom ..

   668

   669 text{*All three types of comparision involving 0 and 1 are covered.*}

   670

   671 lemmas one_neq_zero = zero_neq_one [THEN not_sym]

   672 declare one_neq_zero [simp]

   673

   674 lemma zero_le_one [simp]: "(0::'a::ordered_semidom) \<le> 1"

   675   by (rule zero_less_one [THEN order_less_imp_le])

   676

   677 lemma not_one_le_zero [simp]: "~ (1::'a::ordered_semidom) \<le> 0"

   678 by (simp add: linorder_not_le)

   679

   680 lemma not_one_less_zero [simp]: "~ (1::'a::ordered_semidom) < 0"

   681 by (simp add: linorder_not_less)

   682

   683

   684 subsection{*More Monotonicity*}

   685

   686 text{*Strict monotonicity in both arguments*}

   687 lemma mult_strict_mono:

   688      "[|a<b; c<d; 0<b; 0\<le>c|] ==> a * c < b * (d::'a::ordered_semiring_strict)"

   689 apply (cases "c=0")

   690  apply (simp add: mult_pos_pos)

   691 apply (erule mult_strict_right_mono [THEN order_less_trans])

   692  apply (force simp add: order_le_less)

   693 apply (erule mult_strict_left_mono, assumption)

   694 done

   695

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

   697 lemma mult_strict_mono':

   698      "[| a<b; c<d; 0 \<le> a; 0 \<le> c|] ==> a * c < b * (d::'a::ordered_semiring_strict)"

   699 apply (rule mult_strict_mono)

   700 apply (blast intro: order_le_less_trans)+

   701 done

   702

   703 lemma less_1_mult: "[| 1 < m; 1 < n |] ==> 1 < m*(n::'a::ordered_semidom)"

   704 apply (insert mult_strict_mono [of 1 m 1 n])

   705 apply (simp add:  order_less_trans [OF zero_less_one])

   706 done

   707

   708 lemma mult_less_le_imp_less: "(a::'a::ordered_semiring_strict) < b ==>

   709     c <= d ==> 0 <= a ==> 0 < c ==> a * c < b * d"

   710   apply (subgoal_tac "a * c < b * c")

   711   apply (erule order_less_le_trans)

   712   apply (erule mult_left_mono)

   713   apply simp

   714   apply (erule mult_strict_right_mono)

   715   apply assumption

   716 done

   717

   718 lemma mult_le_less_imp_less: "(a::'a::ordered_semiring_strict) <= b ==>

   719     c < d ==> 0 < a ==> 0 <= c ==> a * c < b * d"

   720   apply (subgoal_tac "a * c <= b * c")

   721   apply (erule order_le_less_trans)

   722   apply (erule mult_strict_left_mono)

   723   apply simp

   724   apply (erule mult_right_mono)

   725   apply simp

   726 done

   727

   728

   729 subsection{*Cancellation Laws for Relationships With a Common Factor*}

   730

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

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

   733

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

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

   736

   737 lemma mult_less_cancel_right_disj:

   738     "(a*c < b*c) = ((0 < c & a < b) | (c < 0 & b < (a::'a::ordered_ring_strict)))"

   739 apply (cases "c = 0")

   740 apply (auto simp add: linorder_neq_iff mult_strict_right_mono

   741                       mult_strict_right_mono_neg)

   742 apply (auto simp add: linorder_not_less

   743                       linorder_not_le [symmetric, of "a*c"]

   744                       linorder_not_le [symmetric, of a])

   745 apply (erule_tac [!] notE)

   746 apply (auto simp add: order_less_imp_le mult_right_mono

   747                       mult_right_mono_neg)

   748 done

   749

   750 lemma mult_less_cancel_left_disj:

   751     "(c*a < c*b) = ((0 < c & a < b) | (c < 0 & b < (a::'a::ordered_ring_strict)))"

   752 apply (cases "c = 0")

   753 apply (auto simp add: linorder_neq_iff mult_strict_left_mono

   754                       mult_strict_left_mono_neg)

   755 apply (auto simp add: linorder_not_less

   756                       linorder_not_le [symmetric, of "c*a"]

   757                       linorder_not_le [symmetric, of a])

   758 apply (erule_tac [!] notE)

   759 apply (auto simp add: order_less_imp_le mult_left_mono

   760                       mult_left_mono_neg)

   761 done

   762

   763

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

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

   766

   767 lemma mult_less_cancel_right:

   768   fixes c :: "'a :: ordered_ring_strict"

   769   shows      "(a*c < b*c) = ((0 \<le> c --> a < b) & (c \<le> 0 --> b < a))"

   770 by (insert mult_less_cancel_right_disj [of a c b], auto)

   771

   772 lemma mult_less_cancel_left:

   773   fixes c :: "'a :: ordered_ring_strict"

   774   shows      "(c*a < c*b) = ((0 \<le> c --> a < b) & (c \<le> 0 --> b < a))"

   775 by (insert mult_less_cancel_left_disj [of c a b], auto)

   776

   777 lemma mult_le_cancel_right:

   778      "(a*c \<le> b*c) = ((0<c --> a\<le>b) & (c<0 --> b \<le> (a::'a::ordered_ring_strict)))"

   779 by (simp add: linorder_not_less [symmetric] mult_less_cancel_right_disj)

   780

   781 lemma mult_le_cancel_left:

   782      "(c*a \<le> c*b) = ((0<c --> a\<le>b) & (c<0 --> b \<le> (a::'a::ordered_ring_strict)))"

   783 by (simp add: linorder_not_less [symmetric] mult_less_cancel_left_disj)

   784

   785 lemma mult_less_imp_less_left:

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

   787       shows "a < (b::'a::ordered_semiring_strict)"

   788 proof (rule ccontr)

   789   assume "~ a < b"

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

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

   792   with this and less show False

   793     by (simp add: linorder_not_less [symmetric])

   794 qed

   795

   796 lemma mult_less_imp_less_right:

   797   assumes less: "a*c < b*c" and nonneg: "0 <= c"

   798   shows "a < (b::'a::ordered_semiring_strict)"

   799 proof (rule ccontr)

   800   assume "~ a < b"

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

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

   803   with this and less show False

   804     by (simp add: linorder_not_less [symmetric])

   805 qed

   806

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

   808 lemma mult_cancel_right [simp,noatp]:

   809   fixes a b c :: "'a::ring_no_zero_divisors"

   810   shows "(a * c = b * c) = (c = 0 \<or> a = b)"

   811 proof -

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

   813     by (simp add: ring_distribs)

   814   thus ?thesis

   815     by (simp add: disj_commute)

   816 qed

   817

   818 lemma mult_cancel_left [simp,noatp]:

   819   fixes a b c :: "'a::ring_no_zero_divisors"

   820   shows "(c * a = c * b) = (c = 0 \<or> a = b)"

   821 proof -

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

   823     by (simp add: ring_distribs)

   824   thus ?thesis

   825     by simp

   826 qed

   827

   828

   829 subsubsection{*Special Cancellation Simprules for Multiplication*}

   830

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

   832

   833 lemma mult_le_cancel_right1:

   834   fixes c :: "'a :: ordered_idom"

   835   shows "(c \<le> b*c) = ((0<c --> 1\<le>b) & (c<0 --> b \<le> 1))"

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

   837

   838 lemma mult_le_cancel_right2:

   839   fixes c :: "'a :: ordered_idom"

   840   shows "(a*c \<le> c) = ((0<c --> a\<le>1) & (c<0 --> 1 \<le> a))"

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

   842

   843 lemma mult_le_cancel_left1:

   844   fixes c :: "'a :: ordered_idom"

   845   shows "(c \<le> c*b) = ((0<c --> 1\<le>b) & (c<0 --> b \<le> 1))"

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

   847

   848 lemma mult_le_cancel_left2:

   849   fixes c :: "'a :: ordered_idom"

   850   shows "(c*a \<le> c) = ((0<c --> a\<le>1) & (c<0 --> 1 \<le> a))"

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

   852

   853 lemma mult_less_cancel_right1:

   854   fixes c :: "'a :: ordered_idom"

   855   shows "(c < b*c) = ((0 \<le> c --> 1<b) & (c \<le> 0 --> b < 1))"

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

   857

   858 lemma mult_less_cancel_right2:

   859   fixes c :: "'a :: ordered_idom"

   860   shows "(a*c < c) = ((0 \<le> c --> a<1) & (c \<le> 0 --> 1 < a))"

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

   862

   863 lemma mult_less_cancel_left1:

   864   fixes c :: "'a :: ordered_idom"

   865   shows "(c < c*b) = ((0 \<le> c --> 1<b) & (c \<le> 0 --> b < 1))"

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

   867

   868 lemma mult_less_cancel_left2:

   869   fixes c :: "'a :: ordered_idom"

   870   shows "(c*a < c) = ((0 \<le> c --> a<1) & (c \<le> 0 --> 1 < a))"

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

   872

   873 lemma mult_cancel_right1 [simp]:

   874   fixes c :: "'a :: ring_1_no_zero_divisors"

   875   shows "(c = b*c) = (c = 0 | b=1)"

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

   877

   878 lemma mult_cancel_right2 [simp]:

   879   fixes c :: "'a :: ring_1_no_zero_divisors"

   880   shows "(a*c = c) = (c = 0 | a=1)"

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

   882

   883 lemma mult_cancel_left1 [simp]:

   884   fixes c :: "'a :: ring_1_no_zero_divisors"

   885   shows "(c = c*b) = (c = 0 | b=1)"

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

   887

   888 lemma mult_cancel_left2 [simp]:

   889   fixes c :: "'a :: ring_1_no_zero_divisors"

   890   shows "(c*a = c) = (c = 0 | a=1)"

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

   892

   893

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

   895 lemmas mult_compare_simps =

   896     mult_le_cancel_right mult_le_cancel_left

   897     mult_le_cancel_right1 mult_le_cancel_right2

   898     mult_le_cancel_left1 mult_le_cancel_left2

   899     mult_less_cancel_right mult_less_cancel_left

   900     mult_less_cancel_right1 mult_less_cancel_right2

   901     mult_less_cancel_left1 mult_less_cancel_left2

   902     mult_cancel_right mult_cancel_left

   903     mult_cancel_right1 mult_cancel_right2

   904     mult_cancel_left1 mult_cancel_left2

   905

   906

   907 (* what ordering?? this is a straight instance of mult_eq_0_iff

   908 text{*Compared with @{text mult_eq_0_iff}, this version removes the requirement

   909       of an ordering.*}

   910 lemma field_mult_eq_0_iff [simp]:

   911   "(a*b = (0::'a::division_ring)) = (a = 0 | b = 0)"

   912 by simp

   913 *)

   914 (* subsumed by mult_cancel lemmas on ring_no_zero_divisors

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

   916 lemma field_mult_cancel_right_lemma:

   917       assumes cnz: "c \<noteq> (0::'a::division_ring)"

   918          and eq:  "a*c = b*c"

   919         shows "a=b"

   920 proof -

   921   have "(a * c) * inverse c = (b * c) * inverse c"

   922     by (simp add: eq)

   923   thus "a=b"

   924     by (simp add: mult_assoc cnz)

   925 qed

   926

   927 lemma field_mult_cancel_right [simp]:

   928      "(a*c = b*c) = (c = (0::'a::division_ring) | a=b)"

   929 by simp

   930

   931 lemma field_mult_cancel_left [simp]:

   932      "(c*a = c*b) = (c = (0::'a::division_ring) | a=b)"

   933 by simp

   934 *)

   935 lemma nonzero_imp_inverse_nonzero:

   936   "a \<noteq> 0 ==> inverse a \<noteq> (0::'a::division_ring)"

   937 proof

   938   assume ianz: "inverse a = 0"

   939   assume "a \<noteq> 0"

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

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

   942   finally have "1 = (0::'a::division_ring)" .

   943   thus False by (simp add: eq_commute)

   944 qed

   945

   946

   947 subsection{*Basic Properties of @{term inverse}*}

   948

   949 lemma inverse_zero_imp_zero: "inverse a = 0 ==> a = (0::'a::division_ring)"

   950 apply (rule ccontr)

   951 apply (blast dest: nonzero_imp_inverse_nonzero)

   952 done

   953

   954 lemma inverse_nonzero_imp_nonzero:

   955    "inverse a = 0 ==> a = (0::'a::division_ring)"

   956 apply (rule ccontr)

   957 apply (blast dest: nonzero_imp_inverse_nonzero)

   958 done

   959

   960 lemma inverse_nonzero_iff_nonzero [simp]:

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

   962 by (force dest: inverse_nonzero_imp_nonzero)

   963

   964 lemma nonzero_inverse_minus_eq:

   965       assumes [simp]: "a\<noteq>0"

   966       shows "inverse(-a) = -inverse(a::'a::division_ring)"

   967 proof -

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

   969     by simp

   970   thus ?thesis

   971     by (simp only: mult_cancel_left, simp)

   972 qed

   973

   974 lemma inverse_minus_eq [simp]:

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

   976 proof cases

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

   978 next

   979   assume "a\<noteq>0"

   980   thus ?thesis by (simp add: nonzero_inverse_minus_eq)

   981 qed

   982

   983 lemma nonzero_inverse_eq_imp_eq:

   984       assumes inveq: "inverse a = inverse b"

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

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

   987 	 shows "a = (b::'a::division_ring)"

   988 proof -

   989   have "a * inverse b = a * inverse a"

   990     by (simp add: inveq)

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

   992     by simp

   993   thus "a = b"

   994     by (simp add: mult_assoc anz bnz)

   995 qed

   996

   997 lemma inverse_eq_imp_eq:

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

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

  1000  apply (force dest!: inverse_zero_imp_zero

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

  1002 apply (force dest!: nonzero_inverse_eq_imp_eq)

  1003 done

  1004

  1005 lemma inverse_eq_iff_eq [simp]:

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

  1007 by (force dest!: inverse_eq_imp_eq)

  1008

  1009 lemma nonzero_inverse_inverse_eq:

  1010       assumes [simp]: "a \<noteq> 0"

  1011       shows "inverse(inverse (a::'a::division_ring)) = a"

  1012   proof -

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

  1014     by (simp add: nonzero_imp_inverse_nonzero)

  1015   thus ?thesis

  1016     by (simp add: mult_assoc)

  1017   qed

  1018

  1019 lemma inverse_inverse_eq [simp]:

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

  1021   proof cases

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

  1023   next

  1024     assume "a\<noteq>0"

  1025     thus ?thesis by (simp add: nonzero_inverse_inverse_eq)

  1026   qed

  1027

  1028 lemma inverse_1 [simp]: "inverse 1 = (1::'a::division_ring)"

  1029   proof -

  1030   have "inverse 1 * 1 = (1::'a::division_ring)"

  1031     by (rule left_inverse [OF zero_neq_one [symmetric]])

  1032   thus ?thesis  by simp

  1033   qed

  1034

  1035 lemma inverse_unique:

  1036   assumes ab: "a*b = 1"

  1037   shows "inverse a = (b::'a::division_ring)"

  1038 proof -

  1039   have "a \<noteq> 0" using ab by auto

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

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

  1042 qed

  1043

  1044 lemma nonzero_inverse_mult_distrib:

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

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

  1047       shows "inverse(a*b) = inverse(b) * inverse(a::'a::division_ring)"

  1048   proof -

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

  1050     by (simp add: anz bnz)

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

  1052     by (simp add: mult_assoc bnz)

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

  1054     by simp

  1055   thus ?thesis

  1056     by (simp add: mult_assoc anz)

  1057   qed

  1058

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

  1060       the right-hand side.*}

  1061 lemma inverse_mult_distrib [simp]:

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

  1063   proof cases

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

  1065     thus ?thesis

  1066       by (simp add: nonzero_inverse_mult_distrib mult_commute)

  1067   next

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

  1069     thus ?thesis

  1070       by force

  1071   qed

  1072

  1073 lemma division_ring_inverse_add:

  1074   "[|(a::'a::division_ring) \<noteq> 0; b \<noteq> 0|]

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

  1076 by (simp add: ring_simps)

  1077

  1078 lemma division_ring_inverse_diff:

  1079   "[|(a::'a::division_ring) \<noteq> 0; b \<noteq> 0|]

  1080    ==> inverse a - inverse b = inverse a * (b-a) * inverse b"

  1081 by (simp add: ring_simps)

  1082

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

  1084 lemma inverse_add:

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

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

  1087 by (simp add: division_ring_inverse_add mult_ac)

  1088

  1089 lemma inverse_divide [simp]:

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

  1091 by (simp add: divide_inverse mult_commute)

  1092

  1093

  1094 subsection {* Calculations with fractions *}

  1095

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

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

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

  1099

  1100 lemma nonzero_mult_divide_mult_cancel_left[simp,noatp]:

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

  1102 proof -

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

  1104     by (simp add: divide_inverse nonzero_inverse_mult_distrib)

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

  1106     by (simp only: mult_ac)

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

  1108     by simp

  1109     finally show ?thesis

  1110     by (simp add: divide_inverse)

  1111 qed

  1112

  1113 lemma mult_divide_mult_cancel_left:

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

  1115 apply (cases "b = 0")

  1116 apply (simp_all add: nonzero_mult_divide_mult_cancel_left)

  1117 done

  1118

  1119 lemma nonzero_mult_divide_mult_cancel_right [noatp]:

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

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

  1122

  1123 lemma mult_divide_mult_cancel_right:

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

  1125 apply (cases "b = 0")

  1126 apply (simp_all add: nonzero_mult_divide_mult_cancel_right)

  1127 done

  1128

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

  1130 by (simp add: divide_inverse)

  1131

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

  1133 by (simp add: divide_inverse mult_assoc)

  1134

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

  1136 by (simp add: divide_inverse mult_ac)

  1137

  1138 lemmas times_divide_eq = times_divide_eq_right times_divide_eq_left

  1139

  1140 lemma divide_divide_eq_right [simp,noatp]:

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

  1142 by (simp add: divide_inverse mult_ac)

  1143

  1144 lemma divide_divide_eq_left [simp,noatp]:

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

  1146 by (simp add: divide_inverse mult_assoc)

  1147

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

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

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

  1151 apply (erule ssubst)

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

  1153 apply (erule ssubst)

  1154 apply (rule add_divide_distrib [THEN sym])

  1155 apply (subst mult_commute)

  1156 apply (erule nonzero_mult_divide_mult_cancel_left [THEN sym])

  1157 apply assumption

  1158 apply (erule nonzero_mult_divide_mult_cancel_right [THEN sym])

  1159 apply assumption

  1160 done

  1161

  1162

  1163 subsubsection{*Special Cancellation Simprules for Division*}

  1164

  1165 lemma mult_divide_mult_cancel_left_if[simp,noatp]:

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

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

  1168 by (simp add: mult_divide_mult_cancel_left)

  1169

  1170 lemma nonzero_mult_divide_cancel_right[simp,noatp]:

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

  1172 using nonzero_mult_divide_mult_cancel_right[of 1 b a] by simp

  1173

  1174 lemma nonzero_mult_divide_cancel_left[simp,noatp]:

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

  1176 using nonzero_mult_divide_mult_cancel_left[of 1 a b] by simp

  1177

  1178

  1179 lemma nonzero_divide_mult_cancel_right[simp,noatp]:

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

  1181 using nonzero_mult_divide_mult_cancel_right[of a b 1] by simp

  1182

  1183 lemma nonzero_divide_mult_cancel_left[simp,noatp]:

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

  1185 using nonzero_mult_divide_mult_cancel_left[of b a 1] by simp

  1186

  1187

  1188 lemma nonzero_mult_divide_mult_cancel_left2[simp,noatp]:

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

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

  1191

  1192 lemma nonzero_mult_divide_mult_cancel_right2[simp,noatp]:

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

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

  1195

  1196

  1197 subsection {* Division and Unary Minus *}

  1198

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

  1200 by (simp add: divide_inverse minus_mult_left)

  1201

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

  1203 by (simp add: divide_inverse nonzero_inverse_minus_eq minus_mult_right)

  1204

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

  1206 by (simp add: divide_inverse nonzero_inverse_minus_eq)

  1207

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

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

  1210

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

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

  1213

  1214

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

  1216 lemmas divide_minus_left = minus_divide_left [symmetric]

  1217 lemmas divide_minus_right = minus_divide_right [symmetric]

  1218 declare divide_minus_left [simp]   divide_minus_right [simp]

  1219

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

  1221 lemmas mult_minus_left = minus_mult_left [symmetric]

  1222 lemmas mult_minus_right = minus_mult_right [symmetric]

  1223 declare mult_minus_left [simp]   mult_minus_right [simp]

  1224

  1225 lemma minus_divide_divide [simp]:

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

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

  1228 apply (simp add: nonzero_minus_divide_divide)

  1229 done

  1230

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

  1232 by (simp add: diff_minus add_divide_distrib)

  1233

  1234 lemma add_divide_eq_iff:

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

  1236 by(simp add:add_divide_distrib nonzero_mult_divide_cancel_left)

  1237

  1238 lemma divide_add_eq_iff:

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

  1240 by(simp add:add_divide_distrib nonzero_mult_divide_cancel_left)

  1241

  1242 lemma diff_divide_eq_iff:

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

  1244 by(simp add:diff_divide_distrib nonzero_mult_divide_cancel_left)

  1245

  1246 lemma divide_diff_eq_iff:

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

  1248 by(simp add:diff_divide_distrib nonzero_mult_divide_cancel_left)

  1249

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

  1251 proof -

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

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

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

  1255   finally show ?thesis .

  1256 qed

  1257

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

  1259 proof -

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

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

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

  1263   finally show ?thesis .

  1264 qed

  1265

  1266 lemma eq_divide_eq:

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

  1268 by (simp add: nonzero_eq_divide_eq)

  1269

  1270 lemma divide_eq_eq:

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

  1272 by (force simp add: nonzero_divide_eq_eq)

  1273

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

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

  1276   by (subst divide_eq_eq, simp)

  1277

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

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

  1280   by (subst eq_divide_eq, simp)

  1281

  1282

  1283 lemmas field_eq_simps = ring_simps

  1284   (* pull / out*)

  1285   add_divide_eq_iff divide_add_eq_iff

  1286   diff_divide_eq_iff divide_diff_eq_iff

  1287   (* multiply eqn *)

  1288   nonzero_eq_divide_eq nonzero_divide_eq_eq

  1289 (* is added later:

  1290   times_divide_eq_left times_divide_eq_right

  1291 *)

  1292

  1293 text{*An example:*}

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

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

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

  1297  apply(simp add:field_eq_simps)

  1298 apply(simp)

  1299 done

  1300

  1301

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

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

  1304 by (simp add:field_eq_simps times_divide_eq)

  1305

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

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

  1308 by (simp add:field_eq_simps times_divide_eq)

  1309

  1310

  1311 subsection {* Ordered Fields *}

  1312

  1313 lemma positive_imp_inverse_positive:

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

  1315 proof -

  1316   have "0 < a * inverse a"

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

  1318   thus "0 < inverse a"

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

  1320 qed

  1321

  1322 lemma negative_imp_inverse_negative:

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

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

  1325     simp add: nonzero_inverse_minus_eq order_less_imp_not_eq)

  1326

  1327 lemma inverse_le_imp_le:

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

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

  1330 proof (rule classical)

  1331   assume "~ b \<le> a"

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

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

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

  1335     by (simp add: apos invle order_less_imp_le mult_left_mono)

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

  1337     by (simp add: bpos order_less_imp_le mult_right_mono)

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

  1339 qed

  1340

  1341 lemma inverse_positive_imp_positive:

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

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

  1344 proof -

  1345   have "0 < inverse (inverse a)"

  1346     using inv_gt_0 by (rule positive_imp_inverse_positive)

  1347   thus "0 < a"

  1348     using nz by (simp add: nonzero_inverse_inverse_eq)

  1349 qed

  1350

  1351 lemma inverse_positive_iff_positive [simp]:

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

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

  1354 apply (blast intro: inverse_positive_imp_positive positive_imp_inverse_positive)

  1355 done

  1356

  1357 lemma inverse_negative_imp_negative:

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

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

  1360 proof -

  1361   have "inverse (inverse a) < 0"

  1362     using inv_less_0 by (rule negative_imp_inverse_negative)

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

  1364 qed

  1365

  1366 lemma inverse_negative_iff_negative [simp]:

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

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

  1369 apply (blast intro: inverse_negative_imp_negative negative_imp_inverse_negative)

  1370 done

  1371

  1372 lemma inverse_nonnegative_iff_nonnegative [simp]:

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

  1374 by (simp add: linorder_not_less [symmetric])

  1375

  1376 lemma inverse_nonpositive_iff_nonpositive [simp]:

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

  1378 by (simp add: linorder_not_less [symmetric])

  1379

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

  1381 proof

  1382   fix x::'a

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

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

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

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

  1387 qed

  1388

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

  1390 proof

  1391   fix x::'a

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

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

  1394   have "1 + x > x" by simp

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

  1396 qed

  1397

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

  1399

  1400 lemma less_imp_inverse_less:

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

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

  1403 proof (rule ccontr)

  1404   assume "~ inverse b < inverse a"

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

  1406     by (simp add: linorder_not_less)

  1407   hence "~ (a < b)"

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

  1409   thus False

  1410     by (rule notE [OF _ less])

  1411 qed

  1412

  1413 lemma inverse_less_imp_less:

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

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

  1416 apply (force dest!: inverse_le_imp_le nonzero_inverse_eq_imp_eq)

  1417 done

  1418

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

  1420 lemma inverse_less_iff_less [simp,noatp]:

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

  1422 by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less)

  1423

  1424 lemma le_imp_inverse_le:

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

  1426 by (force simp add: order_le_less less_imp_inverse_less)

  1427

  1428 lemma inverse_le_iff_le [simp,noatp]:

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

  1430 by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le)

  1431

  1432

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

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

  1435 lemma inverse_le_imp_le_neg:

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

  1437 apply (rule classical)

  1438 apply (subgoal_tac "a < 0")

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

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

  1441 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)

  1442 done

  1443

  1444 lemma less_imp_inverse_less_neg:

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

  1446 apply (subgoal_tac "a < 0")

  1447  prefer 2 apply (blast intro: order_less_trans)

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

  1449 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)

  1450 done

  1451

  1452 lemma inverse_less_imp_less_neg:

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

  1454 apply (rule classical)

  1455 apply (subgoal_tac "a < 0")

  1456  prefer 2

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

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

  1459 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)

  1460 done

  1461

  1462 lemma inverse_less_iff_less_neg [simp,noatp]:

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

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

  1465 apply (simp del: inverse_less_iff_less

  1466             add: order_less_imp_not_eq nonzero_inverse_minus_eq)

  1467 done

  1468

  1469 lemma le_imp_inverse_le_neg:

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

  1471 by (force simp add: order_le_less less_imp_inverse_less_neg)

  1472

  1473 lemma inverse_le_iff_le_neg [simp,noatp]:

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

  1475 by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg)

  1476

  1477

  1478 subsection{*Inverses and the Number One*}

  1479

  1480 lemma one_less_inverse_iff:

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

  1482 proof cases

  1483   assume "0 < x"

  1484     with inverse_less_iff_less [OF zero_less_one, of x]

  1485     show ?thesis by simp

  1486 next

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

  1488   have "~ (1 < inverse x)"

  1489   proof

  1490     assume "1 < inverse x"

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

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

  1493     finally show False by auto

  1494   qed

  1495   with notless show ?thesis by simp

  1496 qed

  1497

  1498 lemma inverse_eq_1_iff [simp]:

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

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

  1501

  1502 lemma one_le_inverse_iff:

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

  1504 by (force simp add: order_le_less one_less_inverse_iff zero_less_one

  1505                     eq_commute [of 1])

  1506

  1507 lemma inverse_less_1_iff:

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

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

  1510

  1511 lemma inverse_le_1_iff:

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

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

  1514

  1515

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

  1517

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

  1519 proof -

  1520   assume less: "0<c"

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

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

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

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

  1525   finally show ?thesis .

  1526 qed

  1527

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

  1529 proof -

  1530   assume less: "c<0"

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

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

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

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

  1535   finally show ?thesis .

  1536 qed

  1537

  1538 lemma le_divide_eq:

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

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

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

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

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

  1544 apply (force simp add: pos_le_divide_eq neg_le_divide_eq linorder_neq_iff)

  1545 done

  1546

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

  1548 proof -

  1549   assume less: "0<c"

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

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

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

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

  1554   finally show ?thesis .

  1555 qed

  1556

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

  1558 proof -

  1559   assume less: "c<0"

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

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

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

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

  1564   finally show ?thesis .

  1565 qed

  1566

  1567 lemma divide_le_eq:

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

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

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

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

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

  1573 apply (force simp add: pos_divide_le_eq neg_divide_le_eq linorder_neq_iff)

  1574 done

  1575

  1576 lemma pos_less_divide_eq:

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

  1578 proof -

  1579   assume less: "0<c"

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

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

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

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

  1584   finally show ?thesis .

  1585 qed

  1586

  1587 lemma neg_less_divide_eq:

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

  1589 proof -

  1590   assume less: "c<0"

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

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

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

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

  1595   finally show ?thesis .

  1596 qed

  1597

  1598 lemma less_divide_eq:

  1599   "(a < b/c) =

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

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

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

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

  1604 apply (force simp add: pos_less_divide_eq neg_less_divide_eq linorder_neq_iff)

  1605 done

  1606

  1607 lemma pos_divide_less_eq:

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

  1609 proof -

  1610   assume less: "0<c"

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

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

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

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

  1615   finally show ?thesis .

  1616 qed

  1617

  1618 lemma neg_divide_less_eq:

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

  1620 proof -

  1621   assume less: "c<0"

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

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

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

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

  1626   finally show ?thesis .

  1627 qed

  1628

  1629 lemma divide_less_eq:

  1630   "(b/c < a) =

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

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

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

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

  1635 apply (force simp add: pos_divide_less_eq neg_divide_less_eq linorder_neq_iff)

  1636 done

  1637

  1638

  1639 subsection{*Field simplification*}

  1640

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

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

  1643 positive/negative (for inequations). *}

  1644

  1645 lemmas field_simps = field_eq_simps

  1646   (* multiply ineqn *)

  1647   pos_divide_less_eq neg_divide_less_eq

  1648   pos_less_divide_eq neg_less_divide_eq

  1649   pos_divide_le_eq neg_divide_le_eq

  1650   pos_le_divide_eq neg_le_divide_eq

  1651

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

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

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

  1655 explosions. *}

  1656

  1657 lemmas sign_simps = group_simps

  1658   zero_less_mult_iff  mult_less_0_iff

  1659

  1660 (* Only works once linear arithmetic is installed:

  1661 text{*An example:*}

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

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

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

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

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

  1667  prefer 2 apply(simp add:sign_simps)

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

  1669  prefer 2 apply(simp add:sign_simps)

  1670 apply(simp add:field_simps)

  1671 done

  1672 *)

  1673

  1674

  1675 subsection{*Division and Signs*}

  1676

  1677 lemma zero_less_divide_iff:

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

  1679 by (simp add: divide_inverse zero_less_mult_iff)

  1680

  1681 lemma divide_less_0_iff:

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

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

  1684 by (simp add: divide_inverse mult_less_0_iff)

  1685

  1686 lemma zero_le_divide_iff:

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

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

  1689 by (simp add: divide_inverse zero_le_mult_iff)

  1690

  1691 lemma divide_le_0_iff:

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

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

  1694 by (simp add: divide_inverse mult_le_0_iff)

  1695

  1696 lemma divide_eq_0_iff [simp,noatp]:

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

  1698 by (simp add: divide_inverse)

  1699

  1700 lemma divide_pos_pos:

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

  1702 by(simp add:field_simps)

  1703

  1704

  1705 lemma divide_nonneg_pos:

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

  1707 by(simp add:field_simps)

  1708

  1709 lemma divide_neg_pos:

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

  1711 by(simp add:field_simps)

  1712

  1713 lemma divide_nonpos_pos:

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

  1715 by(simp add:field_simps)

  1716

  1717 lemma divide_pos_neg:

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

  1719 by(simp add:field_simps)

  1720

  1721 lemma divide_nonneg_neg:

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

  1723 by(simp add:field_simps)

  1724

  1725 lemma divide_neg_neg:

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

  1727 by(simp add:field_simps)

  1728

  1729 lemma divide_nonpos_neg:

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

  1731 by(simp add:field_simps)

  1732

  1733

  1734 subsection{*Cancellation Laws for Division*}

  1735

  1736 lemma divide_cancel_right [simp,noatp]:

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

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

  1739 apply (simp add: divide_inverse)

  1740 done

  1741

  1742 lemma divide_cancel_left [simp,noatp]:

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

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

  1745 apply (simp add: divide_inverse)

  1746 done

  1747

  1748

  1749 subsection {* Division and the Number One *}

  1750

  1751 text{*Simplify expressions equated with 1*}

  1752 lemma divide_eq_1_iff [simp,noatp]:

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

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

  1755 apply (simp add: right_inverse_eq)

  1756 done

  1757

  1758 lemma one_eq_divide_iff [simp,noatp]:

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

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

  1761

  1762 lemma zero_eq_1_divide_iff [simp,noatp]:

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

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

  1765 apply (auto simp add: nonzero_eq_divide_eq)

  1766 done

  1767

  1768 lemma one_divide_eq_0_iff [simp,noatp]:

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

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

  1771 apply (insert zero_neq_one [THEN not_sym])

  1772 apply (auto simp add: nonzero_divide_eq_eq)

  1773 done

  1774

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

  1776 lemmas zero_less_divide_1_iff = zero_less_divide_iff [of 1, simplified]

  1777 lemmas divide_less_0_1_iff = divide_less_0_iff [of 1, simplified]

  1778 lemmas zero_le_divide_1_iff = zero_le_divide_iff [of 1, simplified]

  1779 lemmas divide_le_0_1_iff = divide_le_0_iff [of 1, simplified]

  1780

  1781 declare zero_less_divide_1_iff [simp]

  1782 declare divide_less_0_1_iff [simp,noatp]

  1783 declare zero_le_divide_1_iff [simp]

  1784 declare divide_le_0_1_iff [simp,noatp]

  1785

  1786

  1787 subsection {* Ordering Rules for Division *}

  1788

  1789 lemma divide_strict_right_mono:

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

  1791 by (simp add: order_less_imp_not_eq2 divide_inverse mult_strict_right_mono

  1792               positive_imp_inverse_positive)

  1793

  1794 lemma divide_right_mono:

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

  1796 by (force simp add: divide_strict_right_mono order_le_less)

  1797

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

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

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

  1801 apply auto

  1802 done

  1803

  1804 lemma divide_strict_right_mono_neg:

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

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

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

  1808 done

  1809

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

  1811       have the same sign*}

  1812 lemma divide_strict_left_mono:

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

  1814 by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono)

  1815

  1816 lemma divide_left_mono:

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

  1818 by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_right_mono)

  1819

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

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

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

  1823   apply (auto simp add: mult_commute)

  1824 done

  1825

  1826 lemma divide_strict_left_mono_neg:

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

  1828 by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono_neg)

  1829

  1830

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

  1832

  1833 lemma le_divide_eq_1 [noatp]:

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

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

  1836 by (auto simp add: le_divide_eq)

  1837

  1838 lemma divide_le_eq_1 [noatp]:

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

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

  1841 by (auto simp add: divide_le_eq)

  1842

  1843 lemma less_divide_eq_1 [noatp]:

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

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

  1846 by (auto simp add: less_divide_eq)

  1847

  1848 lemma divide_less_eq_1 [noatp]:

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

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

  1851 by (auto simp add: divide_less_eq)

  1852

  1853

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

  1855

  1856 lemma le_divide_eq_1_pos [simp,noatp]:

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

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

  1859 by (auto simp add: le_divide_eq)

  1860

  1861 lemma le_divide_eq_1_neg [simp,noatp]:

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

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

  1864 by (auto simp add: le_divide_eq)

  1865

  1866 lemma divide_le_eq_1_pos [simp,noatp]:

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

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

  1869 by (auto simp add: divide_le_eq)

  1870

  1871 lemma divide_le_eq_1_neg [simp,noatp]:

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

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

  1874 by (auto simp add: divide_le_eq)

  1875

  1876 lemma less_divide_eq_1_pos [simp,noatp]:

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

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

  1879 by (auto simp add: less_divide_eq)

  1880

  1881 lemma less_divide_eq_1_neg [simp,noatp]:

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

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

  1884 by (auto simp add: less_divide_eq)

  1885

  1886 lemma divide_less_eq_1_pos [simp,noatp]:

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

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

  1889 by (auto simp add: divide_less_eq)

  1890

  1891 lemma divide_less_eq_1_neg [simp,noatp]:

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

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

  1894 by (auto simp add: divide_less_eq)

  1895

  1896 lemma eq_divide_eq_1 [simp,noatp]:

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

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

  1899 by (auto simp add: eq_divide_eq)

  1900

  1901 lemma divide_eq_eq_1 [simp,noatp]:

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

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

  1904 by (auto simp add: divide_eq_eq)

  1905

  1906

  1907 subsection {* Reasoning about inequalities with division *}

  1908

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

  1910     ==> x * y <= x"

  1911   by (auto simp add: mult_compare_simps);

  1912

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

  1914     ==> y * x <= x"

  1915   by (auto simp add: mult_compare_simps);

  1916

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

  1918     x / y <= z";

  1919   by (subst pos_divide_le_eq, assumption+);

  1920

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

  1922     z <= x / y"

  1923 by(simp add:field_simps)

  1924

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

  1926     x / y < z"

  1927 by(simp add:field_simps)

  1928

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

  1930     z < x / y"

  1931 by(simp add:field_simps)

  1932

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

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

  1935   apply (rule mult_imp_div_pos_le)

  1936   apply simp

  1937   apply (subst times_divide_eq_left)

  1938   apply (rule mult_imp_le_div_pos, assumption)

  1939   thm mult_mono

  1940   thm mult_mono'

  1941   apply (rule mult_mono)

  1942   apply simp_all

  1943 done

  1944

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

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

  1947   apply (rule mult_imp_div_pos_less)

  1948   apply simp;

  1949   apply (subst times_divide_eq_left);

  1950   apply (rule mult_imp_less_div_pos, assumption)

  1951   apply (erule mult_less_le_imp_less)

  1952   apply simp_all

  1953 done

  1954

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

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

  1957   apply (rule mult_imp_div_pos_less)

  1958   apply simp_all

  1959   apply (subst times_divide_eq_left);

  1960   apply (rule mult_imp_less_div_pos, assumption)

  1961   apply (erule mult_le_less_imp_less)

  1962   apply simp_all

  1963 done

  1964

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

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

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

  1968   seem to need them.*}

  1969

  1970 declare times_divide_eq [simp]

  1971

  1972

  1973 subsection {* Ordered Fields are Dense *}

  1974

  1975 context ordered_semidom

  1976 begin

  1977

  1978 lemma less_add_one: "a < a + 1"

  1979 proof -

  1980   have "a + 0 < a + 1"

  1981     by (blast intro: zero_less_one add_strict_left_mono)

  1982   thus ?thesis by simp

  1983 qed

  1984

  1985 lemma zero_less_two: "0 < 1 + 1"

  1986   by (blast intro: less_trans zero_less_one less_add_one)

  1987

  1988 end

  1989

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

  1991 by (simp add: field_simps zero_less_two)

  1992

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

  1994 by (simp add: field_simps zero_less_two)

  1995

  1996 instance ordered_field < dense_linear_order

  1997 proof

  1998   fix x y :: 'a

  1999   have "x < x + 1" by simp

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

  2001   have "x - 1 < x" by simp

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

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

  2004 qed

  2005

  2006

  2007 subsection {* Absolute Value *}

  2008

  2009 lemma mult_sgn_abs: "sgn x * abs x = (x::'a::{ordered_idom,linorder})"

  2010 using less_linear[of x 0]

  2011 by(auto simp: sgn_if abs_if)

  2012

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

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

  2015

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

  2017 proof -

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

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

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

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

  2022   {

  2023     fix u v :: 'a

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

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

  2026                       nprt a * pprt b + nprt a * nprt b"

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

  2028       apply (simp add: ring_simps)

  2029       done

  2030   }

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

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

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

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

  2035     apply (simp)

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

  2037     apply (rule addm2)

  2038     apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)

  2039     apply (rule addm)

  2040     apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)

  2041     done

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

  2043     apply (simp add:diff_def)

  2044     apply (rule_tac y=0 in order_trans)

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

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

  2047     done

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

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

  2050   show ?thesis

  2051     apply (rule abs_leI)

  2052     apply (simp add: i1)

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

  2054     done

  2055 qed

  2056

  2057 lemma abs_eq_mult:

  2058   assumes "(0 \<le> a \<or> a \<le> 0) \<and> (0 \<le> b \<or> b \<le> 0)"

  2059   shows "abs (a*b) = abs a * abs (b::'a::lordered_ring)"

  2060 proof -

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

  2062     apply (auto)

  2063     apply (rule_tac split_mult_pos_le)

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

  2065     apply (simp)

  2066     apply (rule_tac split_mult_neg_le)

  2067     apply (insert prems)

  2068     apply (blast)

  2069     done

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

  2071     by (simp add: prts[symmetric])

  2072   show ?thesis

  2073   proof cases

  2074     assume "0 <= a * b"

  2075     then show ?thesis

  2076       apply (simp_all add: mulprts abs_prts)

  2077       apply (insert prems)

  2078       apply (auto simp add:

  2079 	ring_simps

  2080 	iffD1[OF zero_le_iff_zero_nprt] iffD1[OF le_zero_iff_zero_pprt]

  2081 	iffD1[OF le_zero_iff_pprt_id] iffD1[OF zero_le_iff_nprt_id])

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

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

  2084       done

  2085   next

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

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

  2088     then show ?thesis

  2089       apply (simp_all add: mulprts abs_prts)

  2090       apply (insert prems)

  2091       apply (auto simp add: ring_simps)

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

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

  2094       done

  2095   qed

  2096 qed

  2097

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

  2099 by (simp add: abs_eq_mult linorder_linear)

  2100

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

  2102 by (simp add: abs_if)

  2103

  2104 lemma nonzero_abs_inverse:

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

  2106 apply (auto simp add: linorder_neq_iff abs_if nonzero_inverse_minus_eq

  2107                       negative_imp_inverse_negative)

  2108 apply (blast intro: positive_imp_inverse_positive elim: order_less_asym)

  2109 done

  2110

  2111 lemma abs_inverse [simp]:

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

  2113       inverse (abs a)"

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

  2115 apply (simp add: nonzero_abs_inverse)

  2116 done

  2117

  2118 lemma nonzero_abs_divide:

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

  2120 by (simp add: divide_inverse abs_mult nonzero_abs_inverse)

  2121

  2122 lemma abs_divide [simp]:

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

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

  2125 apply (simp add: nonzero_abs_divide)

  2126 done

  2127

  2128 lemma abs_mult_less:

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

  2130 proof -

  2131   assume ac: "abs a < c"

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

  2133   assume "abs b < d"

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

  2135 qed

  2136

  2137 lemma eq_minus_self_iff: "(a = -a) = (a = (0::'a::ordered_idom))"

  2138 by (force simp add: order_eq_iff le_minus_self_iff minus_le_self_iff)

  2139

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

  2141 by (simp add: order_less_le le_minus_self_iff eq_minus_self_iff)

  2142

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

  2144 apply (simp add: order_less_le abs_le_iff)

  2145 apply (auto simp add: abs_if minus_le_self_iff eq_minus_self_iff)

  2146 apply (simp add: le_minus_self_iff linorder_neq_iff)

  2147 done

  2148

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

  2150     (abs y) * x = abs (y * x)";

  2151   apply (subst abs_mult);

  2152   apply simp;

  2153 done;

  2154

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

  2156     abs x / y = abs (x / y)";

  2157   apply (subst abs_divide);

  2158   apply (simp add: order_less_imp_le);

  2159 done;

  2160

  2161

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

  2163

  2164 lemma mult_le_prts:

  2165   assumes

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

  2167   "a <= a2"

  2168   "b1 <= b"

  2169   "b <= b2"

  2170   shows

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

  2172 proof -

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

  2174     apply (subst prts[symmetric])+

  2175     apply simp

  2176     done

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

  2178     by (simp add: ring_simps)

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

  2180     by (simp_all add: prems mult_mono)

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

  2182   proof -

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

  2184       by (simp add: mult_left_mono prems)

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

  2186       by (simp add: mult_right_mono_neg prems)

  2187     ultimately show ?thesis

  2188       by simp

  2189   qed

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

  2191   proof -

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

  2193       by (simp add: mult_right_mono prems)

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

  2195       by (simp add: mult_left_mono_neg prems)

  2196     ultimately show ?thesis

  2197       by simp

  2198   qed

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

  2200   proof -

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

  2202       by (simp add: mult_left_mono_neg prems)

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

  2204       by (simp add: mult_right_mono_neg prems)

  2205     ultimately show ?thesis

  2206       by simp

  2207   qed

  2208   ultimately show ?thesis

  2209     by - (rule add_mono | simp)+

  2210 qed

  2211

  2212 lemma mult_ge_prts:

  2213   assumes

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

  2215   "a <= a2"

  2216   "b1 <= b"

  2217   "b <= b2"

  2218   shows

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

  2220 proof -

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

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

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

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

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

  2226     by (simp only: minus_le_iff)

  2227   then show ?thesis by simp

  2228 qed

  2229

  2230 end