src/HOL/Ring_and_Field.thy
 author haftmann Tue Nov 06 08:47:30 2007 +0100 (2007-11-06) changeset 25304 7491c00f0915 parent 25267 1f745c599b5c child 25450 c3b26e533b21 permissions -rw-r--r--
removed subclass edge ordered_ring < lordered_ring
     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 subclass pordered_comm_monoid_add by unfold_locales

   357

   358 lemma mult_left_less_imp_less:

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

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

   361

   362 lemma mult_right_less_imp_less:

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

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

   365

   366 end

   367

   368 class ordered_semiring_strict = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add +

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

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

   371 begin

   372

   373 subclass semiring_0_cancel by unfold_locales

   374

   375 subclass ordered_semiring

   376 proof unfold_locales

   377   fix a b c :: 'a

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

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

   380     unfolding le_less

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

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

   383     unfolding le_less

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

   385 qed

   386

   387 lemma mult_left_le_imp_le:

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

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

   390

   391 lemma mult_right_le_imp_le:

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

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

   394

   395 lemma mult_pos_pos:

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

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

   398

   399 lemma mult_pos_neg:

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

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

   402

   403 lemma mult_pos_neg2:

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

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

   406

   407 lemma zero_less_mult_pos:

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

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

   410  apply (auto simp add: le_less not_less)

   411 apply (drule_tac mult_pos_neg [of a b])

   412  apply (auto dest: less_not_sym)

   413 done

   414

   415 lemma zero_less_mult_pos2:

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

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

   418  apply (auto simp add: le_less not_less)

   419 apply (drule_tac mult_pos_neg2 [of a b])

   420  apply (auto dest: less_not_sym)

   421 done

   422

   423 end

   424

   425 class mult_mono1 = times + zero + ord +

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

   427

   428 class pordered_comm_semiring = comm_semiring_0

   429   + pordered_ab_semigroup_add + mult_mono1

   430 begin

   431

   432 subclass pordered_semiring

   433 proof unfold_locales

   434   fix a b c :: 'a

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

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

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

   438 qed

   439

   440 end

   441

   442 class pordered_cancel_comm_semiring = comm_semiring_0_cancel

   443   + pordered_ab_semigroup_add + mult_mono1

   444 begin

   445

   446 subclass pordered_comm_semiring by unfold_locales

   447 subclass pordered_cancel_semiring by unfold_locales

   448

   449 end

   450

   451 class ordered_comm_semiring_strict = comm_semiring_0 + ordered_cancel_ab_semigroup_add +

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

   453 begin

   454

   455 subclass ordered_semiring_strict

   456 proof unfold_locales

   457   fix a b c :: 'a

   458   assume "a < b" "0 < c"

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

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

   461 qed

   462

   463 subclass pordered_cancel_comm_semiring

   464 proof unfold_locales

   465   fix a b c :: 'a

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

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

   468     unfolding le_less

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

   470 qed

   471

   472 end

   473

   474 class pordered_ring = ring + pordered_cancel_semiring

   475 begin

   476

   477 subclass pordered_ab_group_add by unfold_locales

   478

   479 lemmas ring_simps = ring_simps group_simps

   480

   481 lemma less_add_iff1:

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

   483   by (simp add: ring_simps)

   484

   485 lemma less_add_iff2:

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

   487   by (simp add: ring_simps)

   488

   489 lemma le_add_iff1:

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

   491   by (simp add: ring_simps)

   492

   493 lemma le_add_iff2:

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

   495   by (simp add: ring_simps)

   496

   497 lemma mult_left_mono_neg:

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

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

   500   apply (simp_all add: minus_mult_left [symmetric])

   501   done

   502

   503 lemma mult_right_mono_neg:

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

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

   506   apply (simp_all add: minus_mult_right [symmetric])

   507   done

   508

   509 lemma mult_nonpos_nonpos:

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

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

   512

   513 lemma split_mult_pos_le:

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

   515   by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)

   516

   517 end

   518

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

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

   521

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

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

   524

   525 class ordered_ring = ring + ordered_semiring

   526   + ordered_ab_group_add + abs_if

   527 begin

   528

   529 subclass pordered_ring by unfold_locales

   530

   531 subclass pordered_ab_group_add_abs

   532 proof unfold_locales

   533   fix a b

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

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

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

   537      neg_less_eq_nonneg less_eq_neg_nonpos, auto intro: add_nonneg_nonneg,

   538       auto intro!: less_imp_le add_neg_neg)

   539 qed (auto simp add: abs_if less_eq_neg_nonpos neg_equal_zero)

   540

   541 end

   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   + ordered_ab_group_add + abs_if

   548 begin

   549

   550 subclass ordered_ring by unfold_locales

   551

   552 lemma mult_strict_left_mono_neg:

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

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

   555   apply (simp_all add: minus_mult_left [symmetric])

   556   done

   557

   558 lemma mult_strict_right_mono_neg:

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

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

   561   apply (simp_all add: minus_mult_right [symmetric])

   562   done

   563

   564 lemma mult_neg_neg:

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

   566   by (drule mult_strict_right_mono_neg, auto)

   567

   568 end

   569

   570 instance ordered_ring_strict \<subseteq> ring_no_zero_divisors

   571 apply intro_classes

   572 apply (auto simp add: linorder_not_less order_le_less linorder_neq_iff)

   573 apply (force dest: mult_strict_right_mono_neg mult_strict_right_mono)+

   574 done

   575

   576 lemma zero_less_mult_iff:

   577   fixes a :: "'a::ordered_ring_strict"

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

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

   580   apply (blast dest: zero_less_mult_pos)

   581   apply (blast dest: zero_less_mult_pos2)

   582   done

   583

   584 lemma zero_le_mult_iff:

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

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

   587                    zero_less_mult_iff)

   588

   589 lemma mult_less_0_iff:

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

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

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

   593 done

   594

   595 lemma mult_le_0_iff:

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

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

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

   599 done

   600

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

   602 by (simp add: zero_le_mult_iff linorder_linear)

   603

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

   605 by (simp add: not_less)

   606

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

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

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

   610 also helps with inequalities. *}

   611 lemmas ring_simps = group_simps ring_distribs

   612

   613

   614 class pordered_comm_ring = comm_ring + pordered_comm_semiring

   615 begin

   616

   617 subclass pordered_ring by unfold_locales

   618 subclass pordered_cancel_comm_semiring by unfold_locales

   619

   620 end

   621

   622 class ordered_semidom = comm_semiring_1_cancel + ordered_comm_semiring_strict +

   623   (*previously ordered_semiring*)

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

   625 begin

   626

   627 lemma pos_add_strict:

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

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

   630

   631 end

   632

   633 class ordered_idom =

   634   comm_ring_1 +

   635   ordered_comm_semiring_strict +

   636   ordered_ab_group_add +

   637   abs_if + sgn_if

   638   (*previously ordered_ring*)

   639

   640 instance ordered_idom \<subseteq> ordered_ring_strict ..

   641

   642 instance ordered_idom \<subseteq> pordered_comm_ring ..

   643

   644 class ordered_field = field + ordered_idom

   645

   646 lemma linorder_neqE_ordered_idom:

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

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

   649   using assms by (rule linorder_neqE)

   650

   651

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

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

   654

   655 instance ordered_idom \<subseteq> ordered_semidom

   656 proof

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

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

   659 qed

   660

   661 instance ordered_idom \<subseteq> idom ..

   662

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

   664

   665 lemmas one_neq_zero = zero_neq_one [THEN not_sym]

   666 declare one_neq_zero [simp]

   667

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

   669   by (rule zero_less_one [THEN order_less_imp_le])

   670

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

   672 by (simp add: linorder_not_le)

   673

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

   675 by (simp add: linorder_not_less)

   676

   677

   678 subsection{*More Monotonicity*}

   679

   680 text{*Strict monotonicity in both arguments*}

   681 lemma mult_strict_mono:

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

   683 apply (cases "c=0")

   684  apply (simp add: mult_pos_pos)

   685 apply (erule mult_strict_right_mono [THEN order_less_trans])

   686  apply (force simp add: order_le_less)

   687 apply (erule mult_strict_left_mono, assumption)

   688 done

   689

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

   691 lemma mult_strict_mono':

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

   693 apply (rule mult_strict_mono)

   694 apply (blast intro: order_le_less_trans)+

   695 done

   696

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

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

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

   700 done

   701

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

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

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

   705   apply (erule order_less_le_trans)

   706   apply (erule mult_left_mono)

   707   apply simp

   708   apply (erule mult_strict_right_mono)

   709   apply assumption

   710 done

   711

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

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

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

   715   apply (erule order_le_less_trans)

   716   apply (erule mult_strict_left_mono)

   717   apply simp

   718   apply (erule mult_right_mono)

   719   apply simp

   720 done

   721

   722

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

   724

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

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

   727

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

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

   730

   731 lemma mult_less_cancel_right_disj:

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

   733 apply (cases "c = 0")

   734 apply (auto simp add: linorder_neq_iff mult_strict_right_mono

   735                       mult_strict_right_mono_neg)

   736 apply (auto simp add: linorder_not_less

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

   738                       linorder_not_le [symmetric, of a])

   739 apply (erule_tac [!] notE)

   740 apply (auto simp add: order_less_imp_le mult_right_mono

   741                       mult_right_mono_neg)

   742 done

   743

   744 lemma mult_less_cancel_left_disj:

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

   746 apply (cases "c = 0")

   747 apply (auto simp add: linorder_neq_iff mult_strict_left_mono

   748                       mult_strict_left_mono_neg)

   749 apply (auto simp add: linorder_not_less

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

   751                       linorder_not_le [symmetric, of a])

   752 apply (erule_tac [!] notE)

   753 apply (auto simp add: order_less_imp_le mult_left_mono

   754                       mult_left_mono_neg)

   755 done

   756

   757

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

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

   760

   761 lemma mult_less_cancel_right:

   762   fixes c :: "'a :: ordered_ring_strict"

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

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

   765

   766 lemma mult_less_cancel_left:

   767   fixes c :: "'a :: ordered_ring_strict"

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

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

   770

   771 lemma mult_le_cancel_right:

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

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

   774

   775 lemma mult_le_cancel_left:

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

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

   778

   779 lemma mult_less_imp_less_left:

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

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

   782 proof (rule ccontr)

   783   assume "~ a < b"

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

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

   786   with this and less show False

   787     by (simp add: linorder_not_less [symmetric])

   788 qed

   789

   790 lemma mult_less_imp_less_right:

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

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

   793 proof (rule ccontr)

   794   assume "~ a < b"

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

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

   797   with this and less show False

   798     by (simp add: linorder_not_less [symmetric])

   799 qed

   800

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

   802 lemma mult_cancel_right [simp,noatp]:

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

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

   805 proof -

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

   807     by (simp add: ring_distribs)

   808   thus ?thesis

   809     by (simp add: disj_commute)

   810 qed

   811

   812 lemma mult_cancel_left [simp,noatp]:

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

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

   815 proof -

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

   817     by (simp add: ring_distribs)

   818   thus ?thesis

   819     by simp

   820 qed

   821

   822

   823 subsubsection{*Special Cancellation Simprules for Multiplication*}

   824

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

   826

   827 lemma mult_le_cancel_right1:

   828   fixes c :: "'a :: ordered_idom"

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

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

   831

   832 lemma mult_le_cancel_right2:

   833   fixes c :: "'a :: ordered_idom"

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

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

   836

   837 lemma mult_le_cancel_left1:

   838   fixes c :: "'a :: ordered_idom"

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

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

   841

   842 lemma mult_le_cancel_left2:

   843   fixes c :: "'a :: ordered_idom"

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

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

   846

   847 lemma mult_less_cancel_right1:

   848   fixes c :: "'a :: ordered_idom"

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

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

   851

   852 lemma mult_less_cancel_right2:

   853   fixes c :: "'a :: ordered_idom"

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

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

   856

   857 lemma mult_less_cancel_left1:

   858   fixes c :: "'a :: ordered_idom"

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

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

   861

   862 lemma mult_less_cancel_left2:

   863   fixes c :: "'a :: ordered_idom"

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

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

   866

   867 lemma mult_cancel_right1 [simp]:

   868   fixes c :: "'a :: ring_1_no_zero_divisors"

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

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

   871

   872 lemma mult_cancel_right2 [simp]:

   873   fixes c :: "'a :: ring_1_no_zero_divisors"

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

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

   876

   877 lemma mult_cancel_left1 [simp]:

   878   fixes c :: "'a :: ring_1_no_zero_divisors"

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

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

   881

   882 lemma mult_cancel_left2 [simp]:

   883   fixes c :: "'a :: ring_1_no_zero_divisors"

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

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

   886

   887

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

   889 lemmas mult_compare_simps =

   890     mult_le_cancel_right mult_le_cancel_left

   891     mult_le_cancel_right1 mult_le_cancel_right2

   892     mult_le_cancel_left1 mult_le_cancel_left2

   893     mult_less_cancel_right mult_less_cancel_left

   894     mult_less_cancel_right1 mult_less_cancel_right2

   895     mult_less_cancel_left1 mult_less_cancel_left2

   896     mult_cancel_right mult_cancel_left

   897     mult_cancel_right1 mult_cancel_right2

   898     mult_cancel_left1 mult_cancel_left2

   899

   900

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

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

   903       of an ordering.*}

   904 lemma field_mult_eq_0_iff [simp]:

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

   906 by simp

   907 *)

   908 (* subsumed by mult_cancel lemmas on ring_no_zero_divisors

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

   910 lemma field_mult_cancel_right_lemma:

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

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

   913         shows "a=b"

   914 proof -

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

   916     by (simp add: eq)

   917   thus "a=b"

   918     by (simp add: mult_assoc cnz)

   919 qed

   920

   921 lemma field_mult_cancel_right [simp]:

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

   923 by simp

   924

   925 lemma field_mult_cancel_left [simp]:

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

   927 by simp

   928 *)

   929 lemma nonzero_imp_inverse_nonzero:

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

   931 proof

   932   assume ianz: "inverse a = 0"

   933   assume "a \<noteq> 0"

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

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

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

   937   thus False by (simp add: eq_commute)

   938 qed

   939

   940

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

   942

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

   944 apply (rule ccontr)

   945 apply (blast dest: nonzero_imp_inverse_nonzero)

   946 done

   947

   948 lemma inverse_nonzero_imp_nonzero:

   949    "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_iff_nonzero [simp]:

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

   956 by (force dest: inverse_nonzero_imp_nonzero)

   957

   958 lemma nonzero_inverse_minus_eq:

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

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

   961 proof -

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

   963     by simp

   964   thus ?thesis

   965     by (simp only: mult_cancel_left, simp)

   966 qed

   967

   968 lemma inverse_minus_eq [simp]:

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

   970 proof cases

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

   972 next

   973   assume "a\<noteq>0"

   974   thus ?thesis by (simp add: nonzero_inverse_minus_eq)

   975 qed

   976

   977 lemma nonzero_inverse_eq_imp_eq:

   978       assumes inveq: "inverse a = inverse b"

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

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

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

   982 proof -

   983   have "a * inverse b = a * inverse a"

   984     by (simp add: inveq)

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

   986     by simp

   987   thus "a = b"

   988     by (simp add: mult_assoc anz bnz)

   989 qed

   990

   991 lemma inverse_eq_imp_eq:

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

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

   994  apply (force dest!: inverse_zero_imp_zero

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

   996 apply (force dest!: nonzero_inverse_eq_imp_eq)

   997 done

   998

   999 lemma inverse_eq_iff_eq [simp]:

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

  1001 by (force dest!: inverse_eq_imp_eq)

  1002

  1003 lemma nonzero_inverse_inverse_eq:

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

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

  1006   proof -

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

  1008     by (simp add: nonzero_imp_inverse_nonzero)

  1009   thus ?thesis

  1010     by (simp add: mult_assoc)

  1011   qed

  1012

  1013 lemma inverse_inverse_eq [simp]:

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

  1015   proof cases

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

  1017   next

  1018     assume "a\<noteq>0"

  1019     thus ?thesis by (simp add: nonzero_inverse_inverse_eq)

  1020   qed

  1021

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

  1023   proof -

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

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

  1026   thus ?thesis  by simp

  1027   qed

  1028

  1029 lemma inverse_unique:

  1030   assumes ab: "a*b = 1"

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

  1032 proof -

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

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

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

  1036 qed

  1037

  1038 lemma nonzero_inverse_mult_distrib:

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

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

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

  1042   proof -

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

  1044     by (simp add: anz bnz)

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

  1046     by (simp add: mult_assoc bnz)

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

  1048     by simp

  1049   thus ?thesis

  1050     by (simp add: mult_assoc anz)

  1051   qed

  1052

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

  1054       the right-hand side.*}

  1055 lemma inverse_mult_distrib [simp]:

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

  1057   proof cases

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

  1059     thus ?thesis

  1060       by (simp add: nonzero_inverse_mult_distrib mult_commute)

  1061   next

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

  1063     thus ?thesis

  1064       by force

  1065   qed

  1066

  1067 lemma division_ring_inverse_add:

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

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

  1070 by (simp add: ring_simps)

  1071

  1072 lemma division_ring_inverse_diff:

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

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

  1075 by (simp add: ring_simps)

  1076

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

  1078 lemma inverse_add:

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

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

  1081 by (simp add: division_ring_inverse_add mult_ac)

  1082

  1083 lemma inverse_divide [simp]:

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

  1085 by (simp add: divide_inverse mult_commute)

  1086

  1087

  1088 subsection {* Calculations with fractions *}

  1089

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

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

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

  1093

  1094 lemma nonzero_mult_divide_mult_cancel_left[simp,noatp]:

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

  1096 proof -

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

  1098     by (simp add: divide_inverse nonzero_inverse_mult_distrib)

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

  1100     by (simp only: mult_ac)

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

  1102     by simp

  1103     finally show ?thesis

  1104     by (simp add: divide_inverse)

  1105 qed

  1106

  1107 lemma mult_divide_mult_cancel_left:

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

  1109 apply (cases "b = 0")

  1110 apply (simp_all add: nonzero_mult_divide_mult_cancel_left)

  1111 done

  1112

  1113 lemma nonzero_mult_divide_mult_cancel_right [noatp]:

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

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

  1116

  1117 lemma mult_divide_mult_cancel_right:

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

  1119 apply (cases "b = 0")

  1120 apply (simp_all add: nonzero_mult_divide_mult_cancel_right)

  1121 done

  1122

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

  1124 by (simp add: divide_inverse)

  1125

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

  1127 by (simp add: divide_inverse mult_assoc)

  1128

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

  1130 by (simp add: divide_inverse mult_ac)

  1131

  1132 lemmas times_divide_eq = times_divide_eq_right times_divide_eq_left

  1133

  1134 lemma divide_divide_eq_right [simp,noatp]:

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

  1136 by (simp add: divide_inverse mult_ac)

  1137

  1138 lemma divide_divide_eq_left [simp,noatp]:

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

  1140 by (simp add: divide_inverse mult_assoc)

  1141

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

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

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

  1145 apply (erule ssubst)

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

  1147 apply (erule ssubst)

  1148 apply (rule add_divide_distrib [THEN sym])

  1149 apply (subst mult_commute)

  1150 apply (erule nonzero_mult_divide_mult_cancel_left [THEN sym])

  1151 apply assumption

  1152 apply (erule nonzero_mult_divide_mult_cancel_right [THEN sym])

  1153 apply assumption

  1154 done

  1155

  1156

  1157 subsubsection{*Special Cancellation Simprules for Division*}

  1158

  1159 lemma mult_divide_mult_cancel_left_if[simp,noatp]:

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

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

  1162 by (simp add: mult_divide_mult_cancel_left)

  1163

  1164 lemma nonzero_mult_divide_cancel_right[simp,noatp]:

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

  1166 using nonzero_mult_divide_mult_cancel_right[of 1 b a] by simp

  1167

  1168 lemma nonzero_mult_divide_cancel_left[simp,noatp]:

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

  1170 using nonzero_mult_divide_mult_cancel_left[of 1 a b] by simp

  1171

  1172

  1173 lemma nonzero_divide_mult_cancel_right[simp,noatp]:

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

  1175 using nonzero_mult_divide_mult_cancel_right[of a b 1] by simp

  1176

  1177 lemma nonzero_divide_mult_cancel_left[simp,noatp]:

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

  1179 using nonzero_mult_divide_mult_cancel_left[of b a 1] by simp

  1180

  1181

  1182 lemma nonzero_mult_divide_mult_cancel_left2[simp,noatp]:

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

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

  1185

  1186 lemma nonzero_mult_divide_mult_cancel_right2[simp,noatp]:

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

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

  1189

  1190

  1191 subsection {* Division and Unary Minus *}

  1192

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

  1194 by (simp add: divide_inverse minus_mult_left)

  1195

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

  1197 by (simp add: divide_inverse nonzero_inverse_minus_eq minus_mult_right)

  1198

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

  1200 by (simp add: divide_inverse nonzero_inverse_minus_eq)

  1201

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

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

  1204

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

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

  1207

  1208

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

  1210 lemmas divide_minus_left = minus_divide_left [symmetric]

  1211 lemmas divide_minus_right = minus_divide_right [symmetric]

  1212 declare divide_minus_left [simp]   divide_minus_right [simp]

  1213

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

  1215 lemmas mult_minus_left = minus_mult_left [symmetric]

  1216 lemmas mult_minus_right = minus_mult_right [symmetric]

  1217 declare mult_minus_left [simp]   mult_minus_right [simp]

  1218

  1219 lemma minus_divide_divide [simp]:

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

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

  1222 apply (simp add: nonzero_minus_divide_divide)

  1223 done

  1224

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

  1226 by (simp add: diff_minus add_divide_distrib)

  1227

  1228 lemma add_divide_eq_iff:

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

  1230 by(simp add:add_divide_distrib nonzero_mult_divide_cancel_left)

  1231

  1232 lemma divide_add_eq_iff:

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

  1234 by(simp add:add_divide_distrib nonzero_mult_divide_cancel_left)

  1235

  1236 lemma diff_divide_eq_iff:

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

  1238 by(simp add:diff_divide_distrib nonzero_mult_divide_cancel_left)

  1239

  1240 lemma divide_diff_eq_iff:

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

  1242 by(simp add:diff_divide_distrib nonzero_mult_divide_cancel_left)

  1243

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

  1245 proof -

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

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

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

  1249   finally show ?thesis .

  1250 qed

  1251

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

  1253 proof -

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

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

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

  1257   finally show ?thesis .

  1258 qed

  1259

  1260 lemma eq_divide_eq:

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

  1262 by (simp add: nonzero_eq_divide_eq)

  1263

  1264 lemma divide_eq_eq:

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

  1266 by (force simp add: nonzero_divide_eq_eq)

  1267

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

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

  1270   by (subst divide_eq_eq, simp)

  1271

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

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

  1274   by (subst eq_divide_eq, simp)

  1275

  1276

  1277 lemmas field_eq_simps = ring_simps

  1278   (* pull / out*)

  1279   add_divide_eq_iff divide_add_eq_iff

  1280   diff_divide_eq_iff divide_diff_eq_iff

  1281   (* multiply eqn *)

  1282   nonzero_eq_divide_eq nonzero_divide_eq_eq

  1283 (* is added later:

  1284   times_divide_eq_left times_divide_eq_right

  1285 *)

  1286

  1287 text{*An example:*}

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

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

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

  1291  apply(simp add:field_eq_simps)

  1292 apply(simp)

  1293 done

  1294

  1295

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

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

  1298 by (simp add:field_eq_simps times_divide_eq)

  1299

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

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

  1302 by (simp add:field_eq_simps times_divide_eq)

  1303

  1304

  1305 subsection {* Ordered Fields *}

  1306

  1307 lemma positive_imp_inverse_positive:

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

  1309 proof -

  1310   have "0 < a * inverse a"

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

  1312   thus "0 < inverse a"

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

  1314 qed

  1315

  1316 lemma negative_imp_inverse_negative:

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

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

  1319     simp add: nonzero_inverse_minus_eq order_less_imp_not_eq)

  1320

  1321 lemma inverse_le_imp_le:

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

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

  1324 proof (rule classical)

  1325   assume "~ b \<le> a"

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

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

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

  1329     by (simp add: apos invle order_less_imp_le mult_left_mono)

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

  1331     by (simp add: bpos order_less_imp_le mult_right_mono)

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

  1333 qed

  1334

  1335 lemma inverse_positive_imp_positive:

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

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

  1338 proof -

  1339   have "0 < inverse (inverse a)"

  1340     using inv_gt_0 by (rule positive_imp_inverse_positive)

  1341   thus "0 < a"

  1342     using nz by (simp add: nonzero_inverse_inverse_eq)

  1343 qed

  1344

  1345 lemma inverse_positive_iff_positive [simp]:

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

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

  1348 apply (blast intro: inverse_positive_imp_positive positive_imp_inverse_positive)

  1349 done

  1350

  1351 lemma inverse_negative_imp_negative:

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

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

  1354 proof -

  1355   have "inverse (inverse a) < 0"

  1356     using inv_less_0 by (rule negative_imp_inverse_negative)

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

  1358 qed

  1359

  1360 lemma inverse_negative_iff_negative [simp]:

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

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

  1363 apply (blast intro: inverse_negative_imp_negative negative_imp_inverse_negative)

  1364 done

  1365

  1366 lemma inverse_nonnegative_iff_nonnegative [simp]:

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

  1368 by (simp add: linorder_not_less [symmetric])

  1369

  1370 lemma inverse_nonpositive_iff_nonpositive [simp]:

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

  1372 by (simp add: linorder_not_less [symmetric])

  1373

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

  1375 proof

  1376   fix x::'a

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

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

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

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

  1381 qed

  1382

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

  1384 proof

  1385   fix x::'a

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

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

  1388   have "1 + x > x" by simp

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

  1390 qed

  1391

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

  1393

  1394 lemma less_imp_inverse_less:

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

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

  1397 proof (rule ccontr)

  1398   assume "~ inverse b < inverse a"

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

  1400     by (simp add: linorder_not_less)

  1401   hence "~ (a < b)"

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

  1403   thus False

  1404     by (rule notE [OF _ less])

  1405 qed

  1406

  1407 lemma inverse_less_imp_less:

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

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

  1410 apply (force dest!: inverse_le_imp_le nonzero_inverse_eq_imp_eq)

  1411 done

  1412

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

  1414 lemma inverse_less_iff_less [simp,noatp]:

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

  1416 by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less)

  1417

  1418 lemma le_imp_inverse_le:

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

  1420 by (force simp add: order_le_less less_imp_inverse_less)

  1421

  1422 lemma inverse_le_iff_le [simp,noatp]:

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

  1424 by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le)

  1425

  1426

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

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

  1429 lemma inverse_le_imp_le_neg:

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

  1431 apply (rule classical)

  1432 apply (subgoal_tac "a < 0")

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

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

  1435 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)

  1436 done

  1437

  1438 lemma less_imp_inverse_less_neg:

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

  1440 apply (subgoal_tac "a < 0")

  1441  prefer 2 apply (blast intro: order_less_trans)

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

  1443 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)

  1444 done

  1445

  1446 lemma inverse_less_imp_less_neg:

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

  1448 apply (rule classical)

  1449 apply (subgoal_tac "a < 0")

  1450  prefer 2

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

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

  1453 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)

  1454 done

  1455

  1456 lemma inverse_less_iff_less_neg [simp,noatp]:

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

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

  1459 apply (simp del: inverse_less_iff_less

  1460             add: order_less_imp_not_eq nonzero_inverse_minus_eq)

  1461 done

  1462

  1463 lemma le_imp_inverse_le_neg:

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

  1465 by (force simp add: order_le_less less_imp_inverse_less_neg)

  1466

  1467 lemma inverse_le_iff_le_neg [simp,noatp]:

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

  1469 by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg)

  1470

  1471

  1472 subsection{*Inverses and the Number One*}

  1473

  1474 lemma one_less_inverse_iff:

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

  1476 proof cases

  1477   assume "0 < x"

  1478     with inverse_less_iff_less [OF zero_less_one, of x]

  1479     show ?thesis by simp

  1480 next

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

  1482   have "~ (1 < inverse x)"

  1483   proof

  1484     assume "1 < inverse x"

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

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

  1487     finally show False by auto

  1488   qed

  1489   with notless show ?thesis by simp

  1490 qed

  1491

  1492 lemma inverse_eq_1_iff [simp]:

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

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

  1495

  1496 lemma one_le_inverse_iff:

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

  1498 by (force simp add: order_le_less one_less_inverse_iff zero_less_one

  1499                     eq_commute [of 1])

  1500

  1501 lemma inverse_less_1_iff:

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

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

  1504

  1505 lemma inverse_le_1_iff:

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

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

  1508

  1509

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

  1511

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

  1513 proof -

  1514   assume less: "0<c"

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

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

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

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

  1519   finally show ?thesis .

  1520 qed

  1521

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

  1523 proof -

  1524   assume less: "c<0"

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

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

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

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

  1529   finally show ?thesis .

  1530 qed

  1531

  1532 lemma le_divide_eq:

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

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

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

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

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

  1538 apply (force simp add: pos_le_divide_eq neg_le_divide_eq linorder_neq_iff)

  1539 done

  1540

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

  1542 proof -

  1543   assume less: "0<c"

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

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

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

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

  1548   finally show ?thesis .

  1549 qed

  1550

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

  1552 proof -

  1553   assume less: "c<0"

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

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

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

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

  1558   finally show ?thesis .

  1559 qed

  1560

  1561 lemma divide_le_eq:

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

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

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

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

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

  1567 apply (force simp add: pos_divide_le_eq neg_divide_le_eq linorder_neq_iff)

  1568 done

  1569

  1570 lemma pos_less_divide_eq:

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

  1572 proof -

  1573   assume less: "0<c"

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

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

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

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

  1578   finally show ?thesis .

  1579 qed

  1580

  1581 lemma neg_less_divide_eq:

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

  1583 proof -

  1584   assume less: "c<0"

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

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

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

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

  1589   finally show ?thesis .

  1590 qed

  1591

  1592 lemma less_divide_eq:

  1593   "(a < b/c) =

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

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

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

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

  1598 apply (force simp add: pos_less_divide_eq neg_less_divide_eq linorder_neq_iff)

  1599 done

  1600

  1601 lemma pos_divide_less_eq:

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

  1603 proof -

  1604   assume less: "0<c"

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

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

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

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

  1609   finally show ?thesis .

  1610 qed

  1611

  1612 lemma neg_divide_less_eq:

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

  1614 proof -

  1615   assume less: "c<0"

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

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

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

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

  1620   finally show ?thesis .

  1621 qed

  1622

  1623 lemma divide_less_eq:

  1624   "(b/c < a) =

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

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

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

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

  1629 apply (force simp add: pos_divide_less_eq neg_divide_less_eq linorder_neq_iff)

  1630 done

  1631

  1632

  1633 subsection{*Field simplification*}

  1634

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

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

  1637 positive/negative (for inequations). *}

  1638

  1639 lemmas field_simps = field_eq_simps

  1640   (* multiply ineqn *)

  1641   pos_divide_less_eq neg_divide_less_eq

  1642   pos_less_divide_eq neg_less_divide_eq

  1643   pos_divide_le_eq neg_divide_le_eq

  1644   pos_le_divide_eq neg_le_divide_eq

  1645

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

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

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

  1649 explosions. *}

  1650

  1651 lemmas sign_simps = group_simps

  1652   zero_less_mult_iff  mult_less_0_iff

  1653

  1654 (* Only works once linear arithmetic is installed:

  1655 text{*An example:*}

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

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

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

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

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

  1661  prefer 2 apply(simp add:sign_simps)

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

  1663  prefer 2 apply(simp add:sign_simps)

  1664 apply(simp add:field_simps)

  1665 done

  1666 *)

  1667

  1668

  1669 subsection{*Division and Signs*}

  1670

  1671 lemma zero_less_divide_iff:

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

  1673 by (simp add: divide_inverse zero_less_mult_iff)

  1674

  1675 lemma divide_less_0_iff:

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

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

  1678 by (simp add: divide_inverse mult_less_0_iff)

  1679

  1680 lemma zero_le_divide_iff:

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

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

  1683 by (simp add: divide_inverse zero_le_mult_iff)

  1684

  1685 lemma divide_le_0_iff:

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

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

  1688 by (simp add: divide_inverse mult_le_0_iff)

  1689

  1690 lemma divide_eq_0_iff [simp,noatp]:

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

  1692 by (simp add: divide_inverse)

  1693

  1694 lemma divide_pos_pos:

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

  1696 by(simp add:field_simps)

  1697

  1698

  1699 lemma divide_nonneg_pos:

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

  1701 by(simp add:field_simps)

  1702

  1703 lemma divide_neg_pos:

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

  1705 by(simp add:field_simps)

  1706

  1707 lemma divide_nonpos_pos:

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

  1709 by(simp add:field_simps)

  1710

  1711 lemma divide_pos_neg:

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

  1713 by(simp add:field_simps)

  1714

  1715 lemma divide_nonneg_neg:

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

  1717 by(simp add:field_simps)

  1718

  1719 lemma divide_neg_neg:

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

  1721 by(simp add:field_simps)

  1722

  1723 lemma divide_nonpos_neg:

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

  1725 by(simp add:field_simps)

  1726

  1727

  1728 subsection{*Cancellation Laws for Division*}

  1729

  1730 lemma divide_cancel_right [simp,noatp]:

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

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

  1733 apply (simp add: divide_inverse)

  1734 done

  1735

  1736 lemma divide_cancel_left [simp,noatp]:

  1737      "(c/a = c/b) = (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

  1743 subsection {* Division and the Number One *}

  1744

  1745 text{*Simplify expressions equated with 1*}

  1746 lemma divide_eq_1_iff [simp,noatp]:

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

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

  1749 apply (simp add: right_inverse_eq)

  1750 done

  1751

  1752 lemma one_eq_divide_iff [simp,noatp]:

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

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

  1755

  1756 lemma zero_eq_1_divide_iff [simp,noatp]:

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

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

  1759 apply (auto simp add: nonzero_eq_divide_eq)

  1760 done

  1761

  1762 lemma one_divide_eq_0_iff [simp,noatp]:

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

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

  1765 apply (insert zero_neq_one [THEN not_sym])

  1766 apply (auto simp add: nonzero_divide_eq_eq)

  1767 done

  1768

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

  1770 lemmas zero_less_divide_1_iff = zero_less_divide_iff [of 1, simplified]

  1771 lemmas divide_less_0_1_iff = divide_less_0_iff [of 1, simplified]

  1772 lemmas zero_le_divide_1_iff = zero_le_divide_iff [of 1, simplified]

  1773 lemmas divide_le_0_1_iff = divide_le_0_iff [of 1, simplified]

  1774

  1775 declare zero_less_divide_1_iff [simp]

  1776 declare divide_less_0_1_iff [simp,noatp]

  1777 declare zero_le_divide_1_iff [simp]

  1778 declare divide_le_0_1_iff [simp,noatp]

  1779

  1780

  1781 subsection {* Ordering Rules for Division *}

  1782

  1783 lemma divide_strict_right_mono:

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

  1785 by (simp add: order_less_imp_not_eq2 divide_inverse mult_strict_right_mono

  1786               positive_imp_inverse_positive)

  1787

  1788 lemma divide_right_mono:

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

  1790 by (force simp add: divide_strict_right_mono order_le_less)

  1791

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

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

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

  1795 apply auto

  1796 done

  1797

  1798 lemma divide_strict_right_mono_neg:

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

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

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

  1802 done

  1803

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

  1805       have the same sign*}

  1806 lemma divide_strict_left_mono:

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

  1808 by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono)

  1809

  1810 lemma divide_left_mono:

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

  1812 by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_right_mono)

  1813

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

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

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

  1817   apply (auto simp add: mult_commute)

  1818 done

  1819

  1820 lemma divide_strict_left_mono_neg:

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

  1822 by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono_neg)

  1823

  1824

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

  1826

  1827 lemma le_divide_eq_1 [noatp]:

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

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

  1830 by (auto simp add: le_divide_eq)

  1831

  1832 lemma divide_le_eq_1 [noatp]:

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

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

  1835 by (auto simp add: divide_le_eq)

  1836

  1837 lemma less_divide_eq_1 [noatp]:

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

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

  1840 by (auto simp add: less_divide_eq)

  1841

  1842 lemma divide_less_eq_1 [noatp]:

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

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

  1845 by (auto simp add: divide_less_eq)

  1846

  1847

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

  1849

  1850 lemma le_divide_eq_1_pos [simp,noatp]:

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

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

  1853 by (auto simp add: le_divide_eq)

  1854

  1855 lemma le_divide_eq_1_neg [simp,noatp]:

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

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

  1858 by (auto simp add: le_divide_eq)

  1859

  1860 lemma divide_le_eq_1_pos [simp,noatp]:

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

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

  1863 by (auto simp add: divide_le_eq)

  1864

  1865 lemma divide_le_eq_1_neg [simp,noatp]:

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

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

  1868 by (auto simp add: divide_le_eq)

  1869

  1870 lemma less_divide_eq_1_pos [simp,noatp]:

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

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

  1873 by (auto simp add: less_divide_eq)

  1874

  1875 lemma less_divide_eq_1_neg [simp,noatp]:

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

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

  1878 by (auto simp add: less_divide_eq)

  1879

  1880 lemma divide_less_eq_1_pos [simp,noatp]:

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

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

  1883 by (auto simp add: divide_less_eq)

  1884

  1885 lemma divide_less_eq_1_neg [simp,noatp]:

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

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

  1888 by (auto simp add: divide_less_eq)

  1889

  1890 lemma eq_divide_eq_1 [simp,noatp]:

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

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

  1893 by (auto simp add: eq_divide_eq)

  1894

  1895 lemma divide_eq_eq_1 [simp,noatp]:

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

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

  1898 by (auto simp add: divide_eq_eq)

  1899

  1900

  1901 subsection {* Reasoning about inequalities with division *}

  1902

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

  1904     ==> x * y <= x"

  1905   by (auto simp add: mult_compare_simps);

  1906

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

  1908     ==> y * x <= x"

  1909   by (auto simp add: mult_compare_simps);

  1910

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

  1912     x / y <= z";

  1913   by (subst pos_divide_le_eq, assumption+);

  1914

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

  1916     z <= x / y"

  1917 by(simp add:field_simps)

  1918

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

  1920     x / y < z"

  1921 by(simp add:field_simps)

  1922

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

  1924     z < x / y"

  1925 by(simp add:field_simps)

  1926

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

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

  1929   apply (rule mult_imp_div_pos_le)

  1930   apply simp

  1931   apply (subst times_divide_eq_left)

  1932   apply (rule mult_imp_le_div_pos, assumption)

  1933   thm mult_mono

  1934   thm mult_mono'

  1935   apply (rule mult_mono)

  1936   apply simp_all

  1937 done

  1938

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

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

  1941   apply (rule mult_imp_div_pos_less)

  1942   apply simp;

  1943   apply (subst times_divide_eq_left);

  1944   apply (rule mult_imp_less_div_pos, assumption)

  1945   apply (erule mult_less_le_imp_less)

  1946   apply simp_all

  1947 done

  1948

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

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

  1951   apply (rule mult_imp_div_pos_less)

  1952   apply simp_all

  1953   apply (subst times_divide_eq_left);

  1954   apply (rule mult_imp_less_div_pos, assumption)

  1955   apply (erule mult_le_less_imp_less)

  1956   apply simp_all

  1957 done

  1958

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

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

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

  1962   seem to need them.*}

  1963

  1964 declare times_divide_eq [simp]

  1965

  1966

  1967 subsection {* Ordered Fields are Dense *}

  1968

  1969 context ordered_semidom

  1970 begin

  1971

  1972 lemma less_add_one: "a < a + 1"

  1973 proof -

  1974   have "a + 0 < a + 1"

  1975     by (blast intro: zero_less_one add_strict_left_mono)

  1976   thus ?thesis by simp

  1977 qed

  1978

  1979 lemma zero_less_two: "0 < 1 + 1"

  1980   by (blast intro: less_trans zero_less_one less_add_one)

  1981

  1982 end

  1983

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

  1985 by (simp add: field_simps zero_less_two)

  1986

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

  1988 by (simp add: field_simps zero_less_two)

  1989

  1990 instance ordered_field < dense_linear_order

  1991 proof

  1992   fix x y :: 'a

  1993   have "x < x + 1" by simp

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

  1995   have "x - 1 < x" by simp

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

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

  1998 qed

  1999

  2000

  2001 subsection {* Absolute Value *}

  2002

  2003 context ordered_idom

  2004 begin

  2005

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

  2007   unfolding abs_if sgn_if by auto

  2008

  2009 end

  2010

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

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

  2013

  2014 class pordered_ring_abs = pordered_ring + pordered_ab_group_add_abs +

  2015   assumes abs_eq_mult:

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

  2017

  2018

  2019 class lordered_ring = pordered_ring + lordered_ab_group_add_abs

  2020 begin

  2021

  2022 subclass lordered_ab_group_add_meet by unfold_locales

  2023 subclass lordered_ab_group_add_join by unfold_locales

  2024

  2025 end

  2026

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

  2028 proof -

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

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

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

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

  2033   {

  2034     fix u v :: 'a

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

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

  2037                       nprt a * pprt b + nprt a * nprt b"

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

  2039       apply (simp add: ring_simps)

  2040       done

  2041   }

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

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

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

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

  2046     apply (simp)

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

  2048     apply (rule addm2)

  2049     apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)

  2050     apply (rule addm)

  2051     apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)

  2052     done

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

  2054     apply (simp add:diff_def)

  2055     apply (rule_tac y=0 in order_trans)

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

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

  2058     done

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

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

  2061   show ?thesis

  2062     apply (rule abs_leI)

  2063     apply (simp add: i1)

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

  2065     done

  2066 qed

  2067

  2068 instance lordered_ring \<subseteq> pordered_ring_abs

  2069 proof

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

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

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

  2073 proof -

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

  2075     apply (auto)

  2076     apply (rule_tac split_mult_pos_le)

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

  2078     apply (simp)

  2079     apply (rule_tac split_mult_neg_le)

  2080     apply (insert prems)

  2081     apply (blast)

  2082     done

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

  2084     by (simp add: prts[symmetric])

  2085   show ?thesis

  2086   proof cases

  2087     assume "0 <= a * b"

  2088     then show ?thesis

  2089       apply (simp_all add: mulprts abs_prts)

  2090       apply (insert prems)

  2091       apply (auto simp add:

  2092 	ring_simps

  2093 	iffD1[OF zero_le_iff_zero_nprt] iffD1[OF le_zero_iff_zero_pprt]

  2094 	iffD1[OF le_zero_iff_pprt_id] iffD1[OF zero_le_iff_nprt_id])

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

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

  2097       done

  2098   next

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

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

  2101     then show ?thesis

  2102       apply (simp_all add: mulprts abs_prts)

  2103       apply (insert prems)

  2104       apply (auto simp add: ring_simps)

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

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

  2107       done

  2108   qed

  2109 qed

  2110 qed

  2111

  2112 instance ordered_idom \<subseteq> pordered_ring_abs

  2113 by default (auto simp add: abs_if not_less

  2114   equal_neg_zero neg_equal_zero mult_less_0_iff)

  2115

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

  2117   by (simp add: abs_eq_mult linorder_linear)

  2118

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

  2120   by (simp add: abs_if)

  2121

  2122 lemma nonzero_abs_inverse:

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

  2124 apply (auto simp add: linorder_neq_iff abs_if nonzero_inverse_minus_eq

  2125                       negative_imp_inverse_negative)

  2126 apply (blast intro: positive_imp_inverse_positive elim: order_less_asym)

  2127 done

  2128

  2129 lemma abs_inverse [simp]:

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

  2131       inverse (abs a)"

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

  2133 apply (simp add: nonzero_abs_inverse)

  2134 done

  2135

  2136 lemma nonzero_abs_divide:

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

  2138 by (simp add: divide_inverse abs_mult nonzero_abs_inverse)

  2139

  2140 lemma abs_divide [simp]:

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

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

  2143 apply (simp add: nonzero_abs_divide)

  2144 done

  2145

  2146 lemma abs_mult_less:

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

  2148 proof -

  2149   assume ac: "abs a < c"

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

  2151   assume "abs b < d"

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

  2153 qed

  2154

  2155 lemmas eq_minus_self_iff = equal_neg_zero

  2156

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

  2158   unfolding order_less_le less_eq_neg_nonpos equal_neg_zero ..

  2159

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

  2161 apply (simp add: order_less_le abs_le_iff)

  2162 apply (auto simp add: abs_if neg_less_eq_nonneg less_eq_neg_nonpos)

  2163 done

  2164

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

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

  2167   apply (subst abs_mult)

  2168   apply simp

  2169 done

  2170

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

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

  2173   apply (subst abs_divide)

  2174   apply (simp add: order_less_imp_le)

  2175 done

  2176

  2177

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

  2179

  2180 lemma mult_le_prts:

  2181   assumes

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

  2183   "a <= a2"

  2184   "b1 <= b"

  2185   "b <= b2"

  2186   shows

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

  2188 proof -

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

  2190     apply (subst prts[symmetric])+

  2191     apply simp

  2192     done

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

  2194     by (simp add: ring_simps)

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

  2196     by (simp_all add: prems mult_mono)

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

  2198   proof -

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

  2200       by (simp add: mult_left_mono prems)

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

  2202       by (simp add: mult_right_mono_neg prems)

  2203     ultimately show ?thesis

  2204       by simp

  2205   qed

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

  2207   proof -

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

  2209       by (simp add: mult_right_mono prems)

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

  2211       by (simp add: mult_left_mono_neg prems)

  2212     ultimately show ?thesis

  2213       by simp

  2214   qed

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

  2216   proof -

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

  2218       by (simp add: mult_left_mono_neg prems)

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

  2220       by (simp add: mult_right_mono_neg prems)

  2221     ultimately show ?thesis

  2222       by simp

  2223   qed

  2224   ultimately show ?thesis

  2225     by - (rule add_mono | simp)+

  2226 qed

  2227

  2228 lemma mult_ge_prts:

  2229   assumes

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

  2231   "a <= a2"

  2232   "b1 <= b"

  2233   "b <= b2"

  2234   shows

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

  2236 proof -

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

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

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

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

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

  2242     by (simp only: minus_le_iff)

  2243   then show ?thesis by simp

  2244 qed

  2245

  2246 end