src/HOL/Ring_and_Field.thy
 author wenzelm Wed Sep 17 21:27:14 2008 +0200 (2008-09-17) changeset 28263 69eaa97e7e96 parent 28141 193c3ea0f63b child 28559 55c003a5600a permissions -rw-r--r--
moved global ML bindings to global place;
     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 ..

    84

    85 end

    86

    87 class comm_semiring_0_cancel = comm_semiring + comm_monoid_add + cancel_ab_semigroup_add

    88 begin

    89

    90 subclass semiring_0_cancel ..

    91

    92 subclass comm_semiring_0 ..

    93

    94 end

    95

    96 class zero_neq_one = zero + one +

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

    98 begin

    99

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

   101   by (rule not_sym) (rule zero_neq_one)

   102

   103 end

   104

   105 class semiring_1 = zero_neq_one + semiring_0 + monoid_mult

   106

   107 text {* Abstract divisibility *}

   108

   109 class dvd = times

   110 begin

   111

   112 definition

   113   dvd  :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "dvd" 50)

   114 where

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

   116

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

   118   unfolding dvd_def ..

   119

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

   121   unfolding dvd_def by blast

   122

   123 end

   124

   125 class comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult + dvd

   126   (*previously almost_semiring*)

   127 begin

   128

   129 subclass semiring_1 ..

   130

   131 lemma dvd_refl: "a dvd a"

   132 proof -

   133   have "a = a * 1" by simp

   134   then show ?thesis unfolding dvd_def ..

   135 qed

   136

   137 lemma dvd_trans:

   138   assumes "a dvd b" and "b dvd c"

   139   shows "a dvd c"

   140 proof -

   141   from assms obtain v where "b = a * v" unfolding dvd_def by auto

   142   moreover from assms obtain w where "c = b * w" unfolding dvd_def by auto

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

   144   then show ?thesis unfolding dvd_def ..

   145 qed

   146

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

   148   unfolding dvd_def by simp

   149

   150 lemma dvd_0 [simp]: "a dvd 0"

   151 unfolding dvd_def proof

   152   show "0 = a * 0" by simp

   153 qed

   154

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

   156   unfolding dvd_def by simp

   157

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

   159   unfolding dvd_def by (blast intro: mult_left_commute)

   160

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

   162   apply (subst mult_commute)

   163   apply (erule dvd_mult)

   164   done

   165

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

   167   by (rule dvd_mult) (rule dvd_refl)

   168

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

   170   by (rule dvd_mult2) (rule dvd_refl)

   171

   172 lemma mult_dvd_mono:

   173   assumes ab: "a dvd b"

   174     and "cd": "c dvd d"

   175   shows "a * c dvd b * d"

   176 proof -

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

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

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

   180   then show ?thesis ..

   181 qed

   182

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

   184   by (simp add: dvd_def mult_assoc, blast)

   185

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

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

   188

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

   190 proof -

   191   have "0 = a * 0" by simp

   192   then show ?thesis unfolding dvd_def ..

   193 qed

   194

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

   196   by simp

   197

   198 lemma dvd_add:

   199   assumes ab: "a dvd b"

   200     and ac: "a dvd c"

   201     shows "a dvd (b + c)"

   202 proof -

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

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

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

   206   then show ?thesis ..

   207 qed

   208

   209 end

   210

   211 class no_zero_divisors = zero + times +

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

   213

   214 class semiring_1_cancel = semiring + comm_monoid_add + zero_neq_one

   215   + cancel_ab_semigroup_add + monoid_mult

   216 begin

   217

   218 subclass semiring_0_cancel ..

   219

   220 subclass semiring_1 ..

   221

   222 end

   223

   224 class comm_semiring_1_cancel = comm_semiring + comm_monoid_add + comm_monoid_mult

   225   + zero_neq_one + cancel_ab_semigroup_add

   226 begin

   227

   228 subclass semiring_1_cancel ..

   229 subclass comm_semiring_0_cancel ..

   230 subclass comm_semiring_1 ..

   231

   232 end

   233

   234 class ring = semiring + ab_group_add

   235 begin

   236

   237 subclass semiring_0_cancel ..

   238

   239 text {* Distribution rules *}

   240

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

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

   243

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

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

   246

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

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

   249

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

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

   252

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

   254   by (simp add: right_distrib diff_minus

   255     minus_mult_left [symmetric] minus_mult_right [symmetric])

   256

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

   258   by (simp add: left_distrib diff_minus

   259     minus_mult_left [symmetric] minus_mult_right [symmetric])

   260

   261 lemmas ring_distribs =

   262   right_distrib left_distrib left_diff_distrib right_diff_distrib

   263

   264 lemmas ring_simps =

   265   add_ac

   266   add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2

   267   diff_eq_eq eq_diff_eq diff_minus [symmetric] uminus_add_conv_diff

   268   ring_distribs

   269

   270 lemma eq_add_iff1:

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

   272   by (simp add: ring_simps)

   273

   274 lemma eq_add_iff2:

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

   276   by (simp add: ring_simps)

   277

   278 end

   279

   280 lemmas ring_distribs =

   281   right_distrib left_distrib left_diff_distrib right_diff_distrib

   282

   283 class comm_ring = comm_semiring + ab_group_add

   284 begin

   285

   286 subclass ring ..

   287 subclass comm_semiring_0_cancel ..

   288

   289 end

   290

   291 class ring_1 = ring + zero_neq_one + monoid_mult

   292 begin

   293

   294 subclass semiring_1_cancel ..

   295

   296 end

   297

   298 class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult

   299   (*previously ring*)

   300 begin

   301

   302 subclass ring_1 ..

   303 subclass comm_semiring_1_cancel ..

   304

   305 end

   306

   307 class ring_no_zero_divisors = ring + no_zero_divisors

   308 begin

   309

   310 lemma mult_eq_0_iff [simp]:

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

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

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

   314     then show ?thesis using no_zero_divisors by simp

   315 next

   316   case True then show ?thesis by auto

   317 qed

   318

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

   320 lemma mult_cancel_right [simp, noatp]:

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

   322 proof -

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

   324     by (simp add: ring_distribs right_minus_eq)

   325   thus ?thesis

   326     by (simp add: disj_commute right_minus_eq)

   327 qed

   328

   329 lemma mult_cancel_left [simp, noatp]:

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

   331 proof -

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

   333     by (simp add: ring_distribs right_minus_eq)

   334   thus ?thesis

   335     by (simp add: right_minus_eq)

   336 qed

   337

   338 end

   339

   340 class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors

   341 begin

   342

   343 lemma mult_cancel_right1 [simp]:

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

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

   346

   347 lemma mult_cancel_right2 [simp]:

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

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

   350

   351 lemma mult_cancel_left1 [simp]:

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

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

   354

   355 lemma mult_cancel_left2 [simp]:

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

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

   358

   359 end

   360

   361 class idom = comm_ring_1 + no_zero_divisors

   362 begin

   363

   364 subclass ring_1_no_zero_divisors ..

   365

   366 end

   367

   368 class division_ring = ring_1 + inverse +

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

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

   371 begin

   372

   373 subclass ring_1_no_zero_divisors

   374 proof unfold_locales

   375   fix a b :: 'a

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

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

   378   proof

   379     assume ab: "a * b = 0"

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

   381       by simp

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

   383       by (simp only: mult_assoc)

   384     also have "\<dots> = 1"

   385       using a b by simp

   386     finally show False

   387       by simp

   388   qed

   389 qed

   390

   391 lemma nonzero_imp_inverse_nonzero:

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

   393 proof

   394   assume ianz: "inverse a = 0"

   395   assume "a \<noteq> 0"

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

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

   398   finally have "1 = 0" .

   399   thus False by (simp add: eq_commute)

   400 qed

   401

   402 lemma inverse_zero_imp_zero:

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

   404 apply (rule classical)

   405 apply (drule nonzero_imp_inverse_nonzero)

   406 apply auto

   407 done

   408

   409 lemma nonzero_inverse_minus_eq:

   410   assumes "a \<noteq> 0"

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

   412 proof -

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

   414     using assms by simp

   415   then show ?thesis unfolding mult_cancel_left using assms by simp

   416 qed

   417

   418 lemma nonzero_inverse_inverse_eq:

   419   assumes "a \<noteq> 0"

   420   shows "inverse (inverse a) = a"

   421 proof -

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

   423     using assms by (simp add: nonzero_imp_inverse_nonzero)

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

   425 qed

   426

   427 lemma nonzero_inverse_eq_imp_eq:

   428   assumes inveq: "inverse a = inverse b"

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

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

   431   shows "a = b"

   432 proof -

   433   have "a * inverse b = a * inverse a"

   434     by (simp add: inveq)

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

   436     by simp

   437   then show "a = b"

   438     by (simp add: mult_assoc anz bnz)

   439 qed

   440

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

   442 proof -

   443   have "inverse 1 * 1 = 1"

   444     by (rule left_inverse) (rule one_neq_zero)

   445   then show ?thesis by simp

   446 qed

   447

   448 lemma inverse_unique:

   449   assumes ab: "a * b = 1"

   450   shows "inverse a = b"

   451 proof -

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

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

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

   455 qed

   456

   457 lemma nonzero_inverse_mult_distrib:

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

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

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

   461 proof -

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

   463     by (simp add: anz bnz)

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

   465     by (simp add: mult_assoc bnz)

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

   467     by simp

   468   thus ?thesis

   469     by (simp add: mult_assoc anz)

   470 qed

   471

   472 lemma division_ring_inverse_add:

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

   474   by (simp add: ring_simps mult_assoc)

   475

   476 lemma division_ring_inverse_diff:

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

   478   by (simp add: ring_simps mult_assoc)

   479

   480 end

   481

   482 class field = comm_ring_1 + inverse +

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

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

   485 begin

   486

   487 subclass division_ring

   488 proof unfold_locales

   489   fix a :: 'a

   490   assume "a \<noteq> 0"

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

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

   493 qed

   494

   495 subclass idom ..

   496

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

   498 proof

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

   500   {

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

   502     also assume "a / b = 1"

   503     finally show "a = b" by simp

   504   next

   505     assume "a = b"

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

   507   }

   508 qed

   509

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

   511   by (simp add: divide_inverse)

   512

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

   514   by (simp add: divide_inverse)

   515

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

   517   by (simp add: divide_inverse)

   518

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

   520   by (simp add: divide_inverse)

   521

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

   523   by (simp add: divide_inverse ring_distribs)

   524

   525 end

   526

   527 class division_by_zero = zero + inverse +

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

   529

   530 lemma divide_zero [simp]:

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

   532   by (simp add: divide_inverse)

   533

   534 lemma divide_self_if [simp]:

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

   536   by (simp add: divide_self)

   537

   538 class mult_mono = times + zero + ord +

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

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

   541

   542 class pordered_semiring = mult_mono + semiring_0 + pordered_ab_semigroup_add

   543 begin

   544

   545 lemma mult_mono:

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

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

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

   549 apply (erule mult_left_mono, assumption)

   550 done

   551

   552 lemma mult_mono':

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

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

   555 apply (rule mult_mono)

   556 apply (fast intro: order_trans)+

   557 done

   558

   559 end

   560

   561 class pordered_cancel_semiring = mult_mono + pordered_ab_semigroup_add

   562   + semiring + comm_monoid_add + cancel_ab_semigroup_add

   563 begin

   564

   565 subclass semiring_0_cancel ..

   566 subclass pordered_semiring ..

   567

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

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

   570

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

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

   573

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

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

   576

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

   578   by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)

   579

   580 end

   581

   582 class ordered_semiring = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add + mult_mono

   583 begin

   584

   585 subclass pordered_cancel_semiring ..

   586

   587 subclass pordered_comm_monoid_add ..

   588

   589 lemma mult_left_less_imp_less:

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

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

   592

   593 lemma mult_right_less_imp_less:

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

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

   596

   597 end

   598

   599 class ordered_semiring_strict = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add +

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

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

   602 begin

   603

   604 subclass semiring_0_cancel ..

   605

   606 subclass ordered_semiring

   607 proof unfold_locales

   608   fix a b c :: 'a

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

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

   611     unfolding le_less

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

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

   614     unfolding le_less

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

   616 qed

   617

   618 lemma mult_left_le_imp_le:

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

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

   621

   622 lemma mult_right_le_imp_le:

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

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

   625

   626 lemma mult_pos_pos:

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

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

   629

   630 lemma mult_pos_neg:

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

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

   633

   634 lemma mult_pos_neg2:

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

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

   637

   638 lemma zero_less_mult_pos:

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

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

   641  apply (auto simp add: le_less not_less)

   642 apply (drule_tac mult_pos_neg [of a b])

   643  apply (auto dest: less_not_sym)

   644 done

   645

   646 lemma zero_less_mult_pos2:

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

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

   649  apply (auto simp add: le_less not_less)

   650 apply (drule_tac mult_pos_neg2 [of a b])

   651  apply (auto dest: less_not_sym)

   652 done

   653

   654 text{*Strict monotonicity in both arguments*}

   655 lemma mult_strict_mono:

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

   657   shows "a * c < b * d"

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

   659   apply (simp add: mult_pos_pos)

   660   apply (erule mult_strict_right_mono [THEN less_trans])

   661   apply (force simp add: le_less)

   662   apply (erule mult_strict_left_mono, assumption)

   663   done

   664

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

   666 lemma mult_strict_mono':

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

   668   shows "a * c < b * d"

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

   670

   671 lemma mult_less_le_imp_less:

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

   673   shows "a * c < b * d"

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

   675   apply (erule less_le_trans)

   676   apply (erule mult_left_mono)

   677   apply simp

   678   apply (erule mult_strict_right_mono)

   679   apply assumption

   680   done

   681

   682 lemma mult_le_less_imp_less:

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

   684   shows "a * c < b * d"

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

   686   apply (erule le_less_trans)

   687   apply (erule mult_strict_left_mono)

   688   apply simp

   689   apply (erule mult_right_mono)

   690   apply simp

   691   done

   692

   693 lemma mult_less_imp_less_left:

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

   695   shows "a < b"

   696 proof (rule ccontr)

   697   assume "\<not>  a < b"

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

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

   700   with this and less show False

   701     by (simp add: not_less [symmetric])

   702 qed

   703

   704 lemma mult_less_imp_less_right:

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

   706   shows "a < b"

   707 proof (rule ccontr)

   708   assume "\<not> a < b"

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

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

   711   with this and less show False

   712     by (simp add: not_less [symmetric])

   713 qed

   714

   715 end

   716

   717 class mult_mono1 = times + zero + ord +

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

   719

   720 class pordered_comm_semiring = comm_semiring_0

   721   + pordered_ab_semigroup_add + mult_mono1

   722 begin

   723

   724 subclass pordered_semiring

   725 proof unfold_locales

   726   fix a b c :: 'a

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

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

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

   730 qed

   731

   732 end

   733

   734 class pordered_cancel_comm_semiring = comm_semiring_0_cancel

   735   + pordered_ab_semigroup_add + mult_mono1

   736 begin

   737

   738 subclass pordered_comm_semiring ..

   739 subclass pordered_cancel_semiring ..

   740

   741 end

   742

   743 class ordered_comm_semiring_strict = comm_semiring_0 + ordered_cancel_ab_semigroup_add +

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

   745 begin

   746

   747 subclass ordered_semiring_strict

   748 proof unfold_locales

   749   fix a b c :: 'a

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

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

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

   753 qed

   754

   755 subclass pordered_cancel_comm_semiring

   756 proof unfold_locales

   757   fix a b c :: 'a

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

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

   760     unfolding le_less

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

   762 qed

   763

   764 end

   765

   766 class pordered_ring = ring + pordered_cancel_semiring

   767 begin

   768

   769 subclass pordered_ab_group_add ..

   770

   771 lemmas ring_simps = ring_simps group_simps

   772

   773 lemma less_add_iff1:

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

   775   by (simp add: ring_simps)

   776

   777 lemma less_add_iff2:

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

   779   by (simp add: ring_simps)

   780

   781 lemma le_add_iff1:

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

   783   by (simp add: ring_simps)

   784

   785 lemma le_add_iff2:

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

   787   by (simp add: ring_simps)

   788

   789 lemma mult_left_mono_neg:

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

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

   792   apply (simp_all add: minus_mult_left [symmetric])

   793   done

   794

   795 lemma mult_right_mono_neg:

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

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

   798   apply (simp_all add: minus_mult_right [symmetric])

   799   done

   800

   801 lemma mult_nonpos_nonpos:

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

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

   804

   805 lemma split_mult_pos_le:

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

   807   by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)

   808

   809 end

   810

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

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

   813

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

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

   816

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

   818 by(simp add:sgn_if)

   819

   820 class ordered_ring = ring + ordered_semiring

   821   + ordered_ab_group_add + abs_if

   822 begin

   823

   824 subclass pordered_ring ..

   825

   826 subclass pordered_ab_group_add_abs

   827 proof unfold_locales

   828   fix a b

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

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

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

   832      neg_less_eq_nonneg less_eq_neg_nonpos, auto intro: add_nonneg_nonneg,

   833       auto intro!: less_imp_le add_neg_neg)

   834 qed (auto simp add: abs_if less_eq_neg_nonpos neg_equal_zero)

   835

   836 end

   837

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

   839    Basically, ordered_ring + no_zero_divisors = ordered_ring_strict.

   840  *)

   841 class ordered_ring_strict = ring + ordered_semiring_strict

   842   + ordered_ab_group_add + abs_if

   843 begin

   844

   845 subclass ordered_ring ..

   846

   847 lemma mult_strict_left_mono_neg:

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

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

   850   apply (simp_all add: minus_mult_left [symmetric])

   851   done

   852

   853 lemma mult_strict_right_mono_neg:

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

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

   856   apply (simp_all add: minus_mult_right [symmetric])

   857   done

   858

   859 lemma mult_neg_neg:

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

   861   by (drule mult_strict_right_mono_neg, auto)

   862

   863 subclass ring_no_zero_divisors

   864 proof unfold_locales

   865   fix a b

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

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

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

   869   proof (cases "a < 0")

   870     case True note A' = this

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

   872       case True with A'

   873       show ?thesis by (auto dest: mult_neg_neg)

   874     next

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

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

   877     qed

   878   next

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

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

   881       case True with A'

   882       show ?thesis by (auto dest: mult_strict_right_mono_neg)

   883     next

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

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

   886     qed

   887   qed

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

   889 qed

   890

   891 lemma zero_less_mult_iff:

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

   893   apply (auto simp add: mult_pos_pos mult_neg_neg)

   894   apply (simp_all add: not_less le_less)

   895   apply (erule disjE) apply assumption defer

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

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

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

   899   apply (drule sym) apply simp

   900   apply (blast dest: zero_less_mult_pos)

   901   apply (blast dest: zero_less_mult_pos2)

   902   done

   903

   904 lemma zero_le_mult_iff:

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

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

   907

   908 lemma mult_less_0_iff:

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

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

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

   912   done

   913

   914 lemma mult_le_0_iff:

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

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

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

   918   done

   919

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

   921   by (simp add: zero_le_mult_iff linear)

   922

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

   924   by (simp add: not_less)

   925

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

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

   928

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

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

   931

   932 lemma mult_less_cancel_right_disj:

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

   934   apply (cases "c = 0")

   935   apply (auto simp add: neq_iff mult_strict_right_mono

   936                       mult_strict_right_mono_neg)

   937   apply (auto simp add: not_less

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

   939                       not_le [symmetric, of a])

   940   apply (erule_tac [!] notE)

   941   apply (auto simp add: less_imp_le mult_right_mono

   942                       mult_right_mono_neg)

   943   done

   944

   945 lemma mult_less_cancel_left_disj:

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

   947   apply (cases "c = 0")

   948   apply (auto simp add: neq_iff mult_strict_left_mono

   949                       mult_strict_left_mono_neg)

   950   apply (auto simp add: not_less

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

   952                       not_le [symmetric, of a])

   953   apply (erule_tac [!] notE)

   954   apply (auto simp add: less_imp_le mult_left_mono

   955                       mult_left_mono_neg)

   956   done

   957

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

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

   960

   961 lemma mult_less_cancel_right:

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

   963   using mult_less_cancel_right_disj [of a c b] by auto

   964

   965 lemma mult_less_cancel_left:

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

   967   using mult_less_cancel_left_disj [of c a b] by auto

   968

   969 lemma mult_le_cancel_right:

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

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

   972

   973 lemma mult_le_cancel_left:

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

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

   976

   977 end

   978

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

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

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

   982 also helps with inequalities. *}

   983 lemmas ring_simps = group_simps ring_distribs

   984

   985

   986 class pordered_comm_ring = comm_ring + pordered_comm_semiring

   987 begin

   988

   989 subclass pordered_ring ..

   990 subclass pordered_cancel_comm_semiring ..

   991

   992 end

   993

   994 class ordered_semidom = comm_semiring_1_cancel + ordered_comm_semiring_strict +

   995   (*previously ordered_semiring*)

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

   997 begin

   998

   999 lemma pos_add_strict:

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

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

  1002

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

  1004   by (rule zero_less_one [THEN less_imp_le])

  1005

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

  1007   by (simp add: not_le)

  1008

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

  1010   by (simp add: not_less)

  1011

  1012 lemma less_1_mult:

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

  1014   shows "1 < m * n"

  1015   using assms mult_strict_mono [of 1 m 1 n]

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

  1017

  1018 end

  1019

  1020 class ordered_idom = comm_ring_1 +

  1021   ordered_comm_semiring_strict + ordered_ab_group_add +

  1022   abs_if + sgn_if

  1023   (*previously ordered_ring*)

  1024 begin

  1025

  1026 subclass ordered_ring_strict ..

  1027 subclass pordered_comm_ring ..

  1028 subclass idom ..

  1029

  1030 subclass ordered_semidom

  1031 proof unfold_locales

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

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

  1034 qed

  1035

  1036 lemma linorder_neqE_ordered_idom:

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

  1038   using assms by (rule neqE)

  1039

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

  1041

  1042 lemma mult_le_cancel_right1:

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

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

  1045

  1046 lemma mult_le_cancel_right2:

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

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

  1049

  1050 lemma mult_le_cancel_left1:

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

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

  1053

  1054 lemma mult_le_cancel_left2:

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

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

  1057

  1058 lemma mult_less_cancel_right1:

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

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

  1061

  1062 lemma mult_less_cancel_right2:

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

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

  1065

  1066 lemma mult_less_cancel_left1:

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

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

  1069

  1070 lemma mult_less_cancel_left2:

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

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

  1073

  1074 lemma sgn_sgn [simp]:

  1075   "sgn (sgn a) = sgn a"

  1076   unfolding sgn_if by simp

  1077

  1078 lemma sgn_0_0:

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

  1080   unfolding sgn_if by simp

  1081

  1082 lemma sgn_1_pos:

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

  1084   unfolding sgn_if by (simp add: neg_equal_zero)

  1085

  1086 lemma sgn_1_neg:

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

  1088   unfolding sgn_if by (auto simp add: equal_neg_zero)

  1089

  1090 lemma sgn_times:

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

  1092   by (auto simp add: sgn_if zero_less_mult_iff)

  1093

  1094 end

  1095

  1096 class ordered_field = field + ordered_idom

  1097

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

  1099

  1100 lemmas mult_compare_simps =

  1101     mult_le_cancel_right mult_le_cancel_left

  1102     mult_le_cancel_right1 mult_le_cancel_right2

  1103     mult_le_cancel_left1 mult_le_cancel_left2

  1104     mult_less_cancel_right mult_less_cancel_left

  1105     mult_less_cancel_right1 mult_less_cancel_right2

  1106     mult_less_cancel_left1 mult_less_cancel_left2

  1107     mult_cancel_right mult_cancel_left

  1108     mult_cancel_right1 mult_cancel_right2

  1109     mult_cancel_left1 mult_cancel_left2

  1110

  1111 -- {* FIXME continue localization here *}

  1112

  1113 lemma inverse_nonzero_iff_nonzero [simp]:

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

  1115 by (force dest: inverse_zero_imp_zero)

  1116

  1117 lemma inverse_minus_eq [simp]:

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

  1119 proof cases

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

  1121 next

  1122   assume "a\<noteq>0"

  1123   thus ?thesis by (simp add: nonzero_inverse_minus_eq)

  1124 qed

  1125

  1126 lemma inverse_eq_imp_eq:

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

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

  1129  apply (force dest!: inverse_zero_imp_zero

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

  1131 apply (force dest!: nonzero_inverse_eq_imp_eq)

  1132 done

  1133

  1134 lemma inverse_eq_iff_eq [simp]:

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

  1136 by (force dest!: inverse_eq_imp_eq)

  1137

  1138 lemma inverse_inverse_eq [simp]:

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

  1140   proof cases

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

  1142   next

  1143     assume "a\<noteq>0"

  1144     thus ?thesis by (simp add: nonzero_inverse_inverse_eq)

  1145   qed

  1146

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

  1148       the right-hand side.*}

  1149 lemma inverse_mult_distrib [simp]:

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

  1151   proof cases

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

  1153     thus ?thesis

  1154       by (simp add: nonzero_inverse_mult_distrib mult_commute)

  1155   next

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

  1157     thus ?thesis

  1158       by force

  1159   qed

  1160

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

  1162 lemma inverse_add:

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

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

  1165 by (simp add: division_ring_inverse_add mult_ac)

  1166

  1167 lemma inverse_divide [simp]:

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

  1169 by (simp add: divide_inverse mult_commute)

  1170

  1171

  1172 subsection {* Calculations with fractions *}

  1173

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

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

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

  1177

  1178 lemma nonzero_mult_divide_mult_cancel_left[simp,noatp]:

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

  1180 proof -

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

  1182     by (simp add: divide_inverse nonzero_inverse_mult_distrib)

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

  1184     by (simp only: mult_ac)

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

  1186     by simp

  1187     finally show ?thesis

  1188     by (simp add: divide_inverse)

  1189 qed

  1190

  1191 lemma mult_divide_mult_cancel_left:

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

  1193 apply (cases "b = 0")

  1194 apply (simp_all add: nonzero_mult_divide_mult_cancel_left)

  1195 done

  1196

  1197 lemma nonzero_mult_divide_mult_cancel_right [noatp]:

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

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

  1200

  1201 lemma mult_divide_mult_cancel_right:

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

  1203 apply (cases "b = 0")

  1204 apply (simp_all add: nonzero_mult_divide_mult_cancel_right)

  1205 done

  1206

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

  1208 by (simp add: divide_inverse)

  1209

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

  1211 by (simp add: divide_inverse mult_assoc)

  1212

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

  1214 by (simp add: divide_inverse mult_ac)

  1215

  1216 lemmas times_divide_eq = times_divide_eq_right times_divide_eq_left

  1217

  1218 lemma divide_divide_eq_right [simp,noatp]:

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

  1220 by (simp add: divide_inverse mult_ac)

  1221

  1222 lemma divide_divide_eq_left [simp,noatp]:

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

  1224 by (simp add: divide_inverse mult_assoc)

  1225

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

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

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

  1229 apply (erule ssubst)

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

  1231 apply (erule ssubst)

  1232 apply (rule add_divide_distrib [THEN sym])

  1233 apply (subst mult_commute)

  1234 apply (erule nonzero_mult_divide_mult_cancel_left [THEN sym])

  1235 apply assumption

  1236 apply (erule nonzero_mult_divide_mult_cancel_right [THEN sym])

  1237 apply assumption

  1238 done

  1239

  1240

  1241 subsubsection{*Special Cancellation Simprules for Division*}

  1242

  1243 lemma mult_divide_mult_cancel_left_if[simp,noatp]:

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

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

  1246 by (simp add: mult_divide_mult_cancel_left)

  1247

  1248 lemma nonzero_mult_divide_cancel_right[simp,noatp]:

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

  1250 using nonzero_mult_divide_mult_cancel_right[of 1 b a] by simp

  1251

  1252 lemma nonzero_mult_divide_cancel_left[simp,noatp]:

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

  1254 using nonzero_mult_divide_mult_cancel_left[of 1 a b] by simp

  1255

  1256

  1257 lemma nonzero_divide_mult_cancel_right[simp,noatp]:

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

  1259 using nonzero_mult_divide_mult_cancel_right[of a b 1] by simp

  1260

  1261 lemma nonzero_divide_mult_cancel_left[simp,noatp]:

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

  1263 using nonzero_mult_divide_mult_cancel_left[of b a 1] by simp

  1264

  1265

  1266 lemma nonzero_mult_divide_mult_cancel_left2[simp,noatp]:

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

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

  1269

  1270 lemma nonzero_mult_divide_mult_cancel_right2[simp,noatp]:

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

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

  1273

  1274

  1275 subsection {* Division and Unary Minus *}

  1276

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

  1278 by (simp add: divide_inverse minus_mult_left)

  1279

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

  1281 by (simp add: divide_inverse nonzero_inverse_minus_eq minus_mult_right)

  1282

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

  1284 by (simp add: divide_inverse nonzero_inverse_minus_eq)

  1285

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

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

  1288

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

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

  1291

  1292

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

  1294 lemmas divide_minus_left = minus_divide_left [symmetric]

  1295 lemmas divide_minus_right = minus_divide_right [symmetric]

  1296 declare divide_minus_left [simp]   divide_minus_right [simp]

  1297

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

  1299 lemmas mult_minus_left = minus_mult_left [symmetric]

  1300 lemmas mult_minus_right = minus_mult_right [symmetric]

  1301 declare mult_minus_left [simp]   mult_minus_right [simp]

  1302

  1303 lemma minus_divide_divide [simp]:

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

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

  1306 apply (simp add: nonzero_minus_divide_divide)

  1307 done

  1308

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

  1310 by (simp add: diff_minus add_divide_distrib)

  1311

  1312 lemma add_divide_eq_iff:

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

  1314 by(simp add:add_divide_distrib nonzero_mult_divide_cancel_left)

  1315

  1316 lemma divide_add_eq_iff:

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

  1318 by(simp add:add_divide_distrib nonzero_mult_divide_cancel_left)

  1319

  1320 lemma diff_divide_eq_iff:

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

  1322 by(simp add:diff_divide_distrib nonzero_mult_divide_cancel_left)

  1323

  1324 lemma divide_diff_eq_iff:

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

  1326 by(simp add:diff_divide_distrib nonzero_mult_divide_cancel_left)

  1327

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

  1329 proof -

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

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

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

  1333   finally show ?thesis .

  1334 qed

  1335

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

  1337 proof -

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

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

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

  1341   finally show ?thesis .

  1342 qed

  1343

  1344 lemma eq_divide_eq:

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

  1346 by (simp add: nonzero_eq_divide_eq)

  1347

  1348 lemma divide_eq_eq:

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

  1350 by (force simp add: nonzero_divide_eq_eq)

  1351

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

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

  1354   by (subst divide_eq_eq, simp)

  1355

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

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

  1358   by (subst eq_divide_eq, simp)

  1359

  1360

  1361 lemmas field_eq_simps = ring_simps

  1362   (* pull / out*)

  1363   add_divide_eq_iff divide_add_eq_iff

  1364   diff_divide_eq_iff divide_diff_eq_iff

  1365   (* multiply eqn *)

  1366   nonzero_eq_divide_eq nonzero_divide_eq_eq

  1367 (* is added later:

  1368   times_divide_eq_left times_divide_eq_right

  1369 *)

  1370

  1371 text{*An example:*}

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

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

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

  1375  apply(simp add:field_eq_simps)

  1376 apply(simp)

  1377 done

  1378

  1379

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

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

  1382 by (simp add:field_eq_simps times_divide_eq)

  1383

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

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

  1386 by (simp add:field_eq_simps times_divide_eq)

  1387

  1388

  1389 subsection {* Ordered Fields *}

  1390

  1391 lemma positive_imp_inverse_positive:

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

  1393 proof -

  1394   have "0 < a * inverse a"

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

  1396   thus "0 < inverse a"

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

  1398 qed

  1399

  1400 lemma negative_imp_inverse_negative:

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

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

  1403     simp add: nonzero_inverse_minus_eq order_less_imp_not_eq)

  1404

  1405 lemma inverse_le_imp_le:

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

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

  1408 proof (rule classical)

  1409   assume "~ b \<le> a"

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

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

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

  1413     by (simp add: apos invle order_less_imp_le mult_left_mono)

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

  1415     by (simp add: bpos order_less_imp_le mult_right_mono)

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

  1417 qed

  1418

  1419 lemma inverse_positive_imp_positive:

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

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

  1422 proof -

  1423   have "0 < inverse (inverse a)"

  1424     using inv_gt_0 by (rule positive_imp_inverse_positive)

  1425   thus "0 < a"

  1426     using nz by (simp add: nonzero_inverse_inverse_eq)

  1427 qed

  1428

  1429 lemma inverse_positive_iff_positive [simp]:

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

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

  1432 apply (blast intro: inverse_positive_imp_positive positive_imp_inverse_positive)

  1433 done

  1434

  1435 lemma inverse_negative_imp_negative:

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

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

  1438 proof -

  1439   have "inverse (inverse a) < 0"

  1440     using inv_less_0 by (rule negative_imp_inverse_negative)

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

  1442 qed

  1443

  1444 lemma inverse_negative_iff_negative [simp]:

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

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

  1447 apply (blast intro: inverse_negative_imp_negative negative_imp_inverse_negative)

  1448 done

  1449

  1450 lemma inverse_nonnegative_iff_nonnegative [simp]:

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

  1452 by (simp add: linorder_not_less [symmetric])

  1453

  1454 lemma inverse_nonpositive_iff_nonpositive [simp]:

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

  1456 by (simp add: linorder_not_less [symmetric])

  1457

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

  1459 proof

  1460   fix x::'a

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

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

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

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

  1465 qed

  1466

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

  1468 proof

  1469   fix x::'a

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

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

  1472   have "1 + x > x" by simp

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

  1474 qed

  1475

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

  1477

  1478 lemma less_imp_inverse_less:

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

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

  1481 proof (rule ccontr)

  1482   assume "~ inverse b < inverse a"

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

  1484     by (simp add: linorder_not_less)

  1485   hence "~ (a < b)"

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

  1487   thus False

  1488     by (rule notE [OF _ less])

  1489 qed

  1490

  1491 lemma inverse_less_imp_less:

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

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

  1494 apply (force dest!: inverse_le_imp_le nonzero_inverse_eq_imp_eq)

  1495 done

  1496

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

  1498 lemma inverse_less_iff_less [simp,noatp]:

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

  1500 by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less)

  1501

  1502 lemma le_imp_inverse_le:

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

  1504 by (force simp add: order_le_less less_imp_inverse_less)

  1505

  1506 lemma inverse_le_iff_le [simp,noatp]:

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

  1508 by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le)

  1509

  1510

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

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

  1513 lemma inverse_le_imp_le_neg:

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

  1515 apply (rule classical)

  1516 apply (subgoal_tac "a < 0")

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

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

  1519 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)

  1520 done

  1521

  1522 lemma less_imp_inverse_less_neg:

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

  1524 apply (subgoal_tac "a < 0")

  1525  prefer 2 apply (blast intro: order_less_trans)

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

  1527 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)

  1528 done

  1529

  1530 lemma inverse_less_imp_less_neg:

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

  1532 apply (rule classical)

  1533 apply (subgoal_tac "a < 0")

  1534  prefer 2

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

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

  1537 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)

  1538 done

  1539

  1540 lemma inverse_less_iff_less_neg [simp,noatp]:

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

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

  1543 apply (simp del: inverse_less_iff_less

  1544             add: order_less_imp_not_eq nonzero_inverse_minus_eq)

  1545 done

  1546

  1547 lemma le_imp_inverse_le_neg:

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

  1549 by (force simp add: order_le_less less_imp_inverse_less_neg)

  1550

  1551 lemma inverse_le_iff_le_neg [simp,noatp]:

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

  1553 by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg)

  1554

  1555

  1556 subsection{*Inverses and the Number One*}

  1557

  1558 lemma one_less_inverse_iff:

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

  1560 proof cases

  1561   assume "0 < x"

  1562     with inverse_less_iff_less [OF zero_less_one, of x]

  1563     show ?thesis by simp

  1564 next

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

  1566   have "~ (1 < inverse x)"

  1567   proof

  1568     assume "1 < inverse x"

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

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

  1571     finally show False by auto

  1572   qed

  1573   with notless show ?thesis by simp

  1574 qed

  1575

  1576 lemma inverse_eq_1_iff [simp]:

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

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

  1579

  1580 lemma one_le_inverse_iff:

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

  1582 by (force simp add: order_le_less one_less_inverse_iff zero_less_one

  1583                     eq_commute [of 1])

  1584

  1585 lemma inverse_less_1_iff:

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

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

  1588

  1589 lemma inverse_le_1_iff:

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

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

  1592

  1593

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

  1595

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

  1597 proof -

  1598   assume less: "0<c"

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

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

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

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

  1603   finally show ?thesis .

  1604 qed

  1605

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

  1607 proof -

  1608   assume less: "c<0"

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

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

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

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

  1613   finally show ?thesis .

  1614 qed

  1615

  1616 lemma le_divide_eq:

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

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

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

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

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

  1622 apply (force simp add: pos_le_divide_eq neg_le_divide_eq linorder_neq_iff)

  1623 done

  1624

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

  1626 proof -

  1627   assume less: "0<c"

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

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

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

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

  1632   finally show ?thesis .

  1633 qed

  1634

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

  1636 proof -

  1637   assume less: "c<0"

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

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

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

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

  1642   finally show ?thesis .

  1643 qed

  1644

  1645 lemma divide_le_eq:

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

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

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

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

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

  1651 apply (force simp add: pos_divide_le_eq neg_divide_le_eq linorder_neq_iff)

  1652 done

  1653

  1654 lemma pos_less_divide_eq:

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

  1656 proof -

  1657   assume less: "0<c"

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

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

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

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

  1662   finally show ?thesis .

  1663 qed

  1664

  1665 lemma neg_less_divide_eq:

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

  1667 proof -

  1668   assume less: "c<0"

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

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

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

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

  1673   finally show ?thesis .

  1674 qed

  1675

  1676 lemma less_divide_eq:

  1677   "(a < b/c) =

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

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

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

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

  1682 apply (force simp add: pos_less_divide_eq neg_less_divide_eq linorder_neq_iff)

  1683 done

  1684

  1685 lemma pos_divide_less_eq:

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

  1687 proof -

  1688   assume less: "0<c"

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

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

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

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

  1693   finally show ?thesis .

  1694 qed

  1695

  1696 lemma neg_divide_less_eq:

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

  1698 proof -

  1699   assume less: "c<0"

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

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

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

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

  1704   finally show ?thesis .

  1705 qed

  1706

  1707 lemma divide_less_eq:

  1708   "(b/c < a) =

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

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

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

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

  1713 apply (force simp add: pos_divide_less_eq neg_divide_less_eq linorder_neq_iff)

  1714 done

  1715

  1716

  1717 subsection{*Field simplification*}

  1718

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

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

  1721 positive/negative (for inequations). *}

  1722

  1723 lemmas field_simps = field_eq_simps

  1724   (* multiply ineqn *)

  1725   pos_divide_less_eq neg_divide_less_eq

  1726   pos_less_divide_eq neg_less_divide_eq

  1727   pos_divide_le_eq neg_divide_le_eq

  1728   pos_le_divide_eq neg_le_divide_eq

  1729

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

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

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

  1733 explosions. *}

  1734

  1735 lemmas sign_simps = group_simps

  1736   zero_less_mult_iff  mult_less_0_iff

  1737

  1738 (* Only works once linear arithmetic is installed:

  1739 text{*An example:*}

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

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

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

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

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

  1745  prefer 2 apply(simp add:sign_simps)

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

  1747  prefer 2 apply(simp add:sign_simps)

  1748 apply(simp add:field_simps)

  1749 done

  1750 *)

  1751

  1752

  1753 subsection{*Division and Signs*}

  1754

  1755 lemma zero_less_divide_iff:

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

  1757 by (simp add: divide_inverse zero_less_mult_iff)

  1758

  1759 lemma divide_less_0_iff:

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

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

  1762 by (simp add: divide_inverse mult_less_0_iff)

  1763

  1764 lemma zero_le_divide_iff:

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

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

  1767 by (simp add: divide_inverse zero_le_mult_iff)

  1768

  1769 lemma divide_le_0_iff:

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

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

  1772 by (simp add: divide_inverse mult_le_0_iff)

  1773

  1774 lemma divide_eq_0_iff [simp,noatp]:

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

  1776 by (simp add: divide_inverse)

  1777

  1778 lemma divide_pos_pos:

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

  1780 by(simp add:field_simps)

  1781

  1782

  1783 lemma divide_nonneg_pos:

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

  1785 by(simp add:field_simps)

  1786

  1787 lemma divide_neg_pos:

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

  1789 by(simp add:field_simps)

  1790

  1791 lemma divide_nonpos_pos:

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

  1793 by(simp add:field_simps)

  1794

  1795 lemma divide_pos_neg:

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

  1797 by(simp add:field_simps)

  1798

  1799 lemma divide_nonneg_neg:

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

  1801 by(simp add:field_simps)

  1802

  1803 lemma divide_neg_neg:

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

  1805 by(simp add:field_simps)

  1806

  1807 lemma divide_nonpos_neg:

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

  1809 by(simp add:field_simps)

  1810

  1811

  1812 subsection{*Cancellation Laws for Division*}

  1813

  1814 lemma divide_cancel_right [simp,noatp]:

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

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

  1817 apply (simp add: divide_inverse)

  1818 done

  1819

  1820 lemma divide_cancel_left [simp,noatp]:

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

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

  1823 apply (simp add: divide_inverse)

  1824 done

  1825

  1826

  1827 subsection {* Division and the Number One *}

  1828

  1829 text{*Simplify expressions equated with 1*}

  1830 lemma divide_eq_1_iff [simp,noatp]:

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

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

  1833 apply (simp add: right_inverse_eq)

  1834 done

  1835

  1836 lemma one_eq_divide_iff [simp,noatp]:

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

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

  1839

  1840 lemma zero_eq_1_divide_iff [simp,noatp]:

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

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

  1843 apply (auto simp add: nonzero_eq_divide_eq)

  1844 done

  1845

  1846 lemma one_divide_eq_0_iff [simp,noatp]:

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

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

  1849 apply (insert zero_neq_one [THEN not_sym])

  1850 apply (auto simp add: nonzero_divide_eq_eq)

  1851 done

  1852

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

  1854 lemmas zero_less_divide_1_iff = zero_less_divide_iff [of 1, simplified]

  1855 lemmas divide_less_0_1_iff = divide_less_0_iff [of 1, simplified]

  1856 lemmas zero_le_divide_1_iff = zero_le_divide_iff [of 1, simplified]

  1857 lemmas divide_le_0_1_iff = divide_le_0_iff [of 1, simplified]

  1858

  1859 declare zero_less_divide_1_iff [simp]

  1860 declare divide_less_0_1_iff [simp,noatp]

  1861 declare zero_le_divide_1_iff [simp]

  1862 declare divide_le_0_1_iff [simp,noatp]

  1863

  1864

  1865 subsection {* Ordering Rules for Division *}

  1866

  1867 lemma divide_strict_right_mono:

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

  1869 by (simp add: order_less_imp_not_eq2 divide_inverse mult_strict_right_mono

  1870               positive_imp_inverse_positive)

  1871

  1872 lemma divide_right_mono:

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

  1874 by (force simp add: divide_strict_right_mono order_le_less)

  1875

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

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

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

  1879 apply auto

  1880 done

  1881

  1882 lemma divide_strict_right_mono_neg:

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

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

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

  1886 done

  1887

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

  1889       have the same sign*}

  1890 lemma divide_strict_left_mono:

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

  1892 by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono)

  1893

  1894 lemma divide_left_mono:

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

  1896 by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_right_mono)

  1897

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

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

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

  1901   apply (auto simp add: mult_commute)

  1902 done

  1903

  1904 lemma divide_strict_left_mono_neg:

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

  1906 by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono_neg)

  1907

  1908

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

  1910

  1911 lemma le_divide_eq_1 [noatp]:

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

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

  1914 by (auto simp add: le_divide_eq)

  1915

  1916 lemma divide_le_eq_1 [noatp]:

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

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

  1919 by (auto simp add: divide_le_eq)

  1920

  1921 lemma less_divide_eq_1 [noatp]:

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

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

  1924 by (auto simp add: less_divide_eq)

  1925

  1926 lemma divide_less_eq_1 [noatp]:

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

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

  1929 by (auto simp add: divide_less_eq)

  1930

  1931

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

  1933

  1934 lemma le_divide_eq_1_pos [simp,noatp]:

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

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

  1937 by (auto simp add: le_divide_eq)

  1938

  1939 lemma le_divide_eq_1_neg [simp,noatp]:

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

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

  1942 by (auto simp add: le_divide_eq)

  1943

  1944 lemma divide_le_eq_1_pos [simp,noatp]:

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

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

  1947 by (auto simp add: divide_le_eq)

  1948

  1949 lemma divide_le_eq_1_neg [simp,noatp]:

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

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

  1952 by (auto simp add: divide_le_eq)

  1953

  1954 lemma less_divide_eq_1_pos [simp,noatp]:

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

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

  1957 by (auto simp add: less_divide_eq)

  1958

  1959 lemma less_divide_eq_1_neg [simp,noatp]:

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

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

  1962 by (auto simp add: less_divide_eq)

  1963

  1964 lemma divide_less_eq_1_pos [simp,noatp]:

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

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

  1967 by (auto simp add: divide_less_eq)

  1968

  1969 lemma divide_less_eq_1_neg [simp,noatp]:

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

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

  1972 by (auto simp add: divide_less_eq)

  1973

  1974 lemma eq_divide_eq_1 [simp,noatp]:

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

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

  1977 by (auto simp add: eq_divide_eq)

  1978

  1979 lemma divide_eq_eq_1 [simp,noatp]:

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

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

  1982 by (auto simp add: divide_eq_eq)

  1983

  1984

  1985 subsection {* Reasoning about inequalities with division *}

  1986

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

  1988     ==> x * y <= x"

  1989   by (auto simp add: mult_compare_simps);

  1990

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

  1992     ==> y * x <= x"

  1993   by (auto simp add: mult_compare_simps);

  1994

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

  1996     x / y <= z";

  1997   by (subst pos_divide_le_eq, assumption+);

  1998

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

  2000     z <= x / y"

  2001 by(simp add:field_simps)

  2002

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

  2004     x / y < z"

  2005 by(simp add:field_simps)

  2006

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

  2008     z < x / y"

  2009 by(simp add:field_simps)

  2010

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

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

  2013   apply (rule mult_imp_div_pos_le)

  2014   apply simp

  2015   apply (subst times_divide_eq_left)

  2016   apply (rule mult_imp_le_div_pos, assumption)

  2017   apply (rule mult_mono)

  2018   apply simp_all

  2019 done

  2020

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

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

  2023   apply (rule mult_imp_div_pos_less)

  2024   apply simp;

  2025   apply (subst times_divide_eq_left);

  2026   apply (rule mult_imp_less_div_pos, assumption)

  2027   apply (erule mult_less_le_imp_less)

  2028   apply simp_all

  2029 done

  2030

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

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

  2033   apply (rule mult_imp_div_pos_less)

  2034   apply simp_all

  2035   apply (subst times_divide_eq_left);

  2036   apply (rule mult_imp_less_div_pos, assumption)

  2037   apply (erule mult_le_less_imp_less)

  2038   apply simp_all

  2039 done

  2040

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

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

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

  2044   seem to need them.*}

  2045

  2046 declare times_divide_eq [simp]

  2047

  2048

  2049 subsection {* Ordered Fields are Dense *}

  2050

  2051 context ordered_semidom

  2052 begin

  2053

  2054 lemma less_add_one: "a < a + 1"

  2055 proof -

  2056   have "a + 0 < a + 1"

  2057     by (blast intro: zero_less_one add_strict_left_mono)

  2058   thus ?thesis by simp

  2059 qed

  2060

  2061 lemma zero_less_two: "0 < 1 + 1"

  2062   by (blast intro: less_trans zero_less_one less_add_one)

  2063

  2064 end

  2065

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

  2067 by (simp add: field_simps zero_less_two)

  2068

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

  2070 by (simp add: field_simps zero_less_two)

  2071

  2072 instance ordered_field < dense_linear_order

  2073 proof

  2074   fix x y :: 'a

  2075   have "x < x + 1" by simp

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

  2077   have "x - 1 < x" by simp

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

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

  2080 qed

  2081

  2082

  2083 subsection {* Absolute Value *}

  2084

  2085 context ordered_idom

  2086 begin

  2087

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

  2089   unfolding abs_if sgn_if by auto

  2090

  2091 end

  2092

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

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

  2095

  2096 class pordered_ring_abs = pordered_ring + pordered_ab_group_add_abs +

  2097   assumes abs_eq_mult:

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

  2099

  2100

  2101 class lordered_ring = pordered_ring + lordered_ab_group_add_abs

  2102 begin

  2103

  2104 subclass lordered_ab_group_add_meet ..

  2105 subclass lordered_ab_group_add_join ..

  2106

  2107 end

  2108

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

  2110 proof -

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

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

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

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

  2115   {

  2116     fix u v :: 'a

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

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

  2119                       nprt a * pprt b + nprt a * nprt b"

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

  2121       apply (simp add: ring_simps)

  2122       done

  2123   }

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

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

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

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

  2128     apply (simp)

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

  2130     apply (rule addm2)

  2131     apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)

  2132     apply (rule addm)

  2133     apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)

  2134     done

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

  2136     apply (simp add:diff_def)

  2137     apply (rule_tac y=0 in order_trans)

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

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

  2140     done

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

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

  2143   show ?thesis

  2144     apply (rule abs_leI)

  2145     apply (simp add: i1)

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

  2147     done

  2148 qed

  2149

  2150 instance lordered_ring \<subseteq> pordered_ring_abs

  2151 proof

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

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

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

  2155 proof -

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

  2157     apply (auto)

  2158     apply (rule_tac split_mult_pos_le)

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

  2160     apply (simp)

  2161     apply (rule_tac split_mult_neg_le)

  2162     apply (insert prems)

  2163     apply (blast)

  2164     done

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

  2166     by (simp add: prts[symmetric])

  2167   show ?thesis

  2168   proof cases

  2169     assume "0 <= a * b"

  2170     then show ?thesis

  2171       apply (simp_all add: mulprts abs_prts)

  2172       apply (insert prems)

  2173       apply (auto simp add:

  2174 	ring_simps

  2175 	iffD1[OF zero_le_iff_zero_nprt] iffD1[OF le_zero_iff_zero_pprt]

  2176 	iffD1[OF le_zero_iff_pprt_id] iffD1[OF zero_le_iff_nprt_id])

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

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

  2179       done

  2180   next

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

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

  2183     then show ?thesis

  2184       apply (simp_all add: mulprts abs_prts)

  2185       apply (insert prems)

  2186       apply (auto simp add: ring_simps)

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

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

  2189       done

  2190   qed

  2191 qed

  2192 qed

  2193

  2194 instance ordered_idom \<subseteq> pordered_ring_abs

  2195 by default (auto simp add: abs_if not_less

  2196   equal_neg_zero neg_equal_zero mult_less_0_iff)

  2197

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

  2199   by (simp add: abs_eq_mult linorder_linear)

  2200

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

  2202   by (simp add: abs_if)

  2203

  2204 lemma nonzero_abs_inverse:

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

  2206 apply (auto simp add: linorder_neq_iff abs_if nonzero_inverse_minus_eq

  2207                       negative_imp_inverse_negative)

  2208 apply (blast intro: positive_imp_inverse_positive elim: order_less_asym)

  2209 done

  2210

  2211 lemma abs_inverse [simp]:

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

  2213       inverse (abs a)"

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

  2215 apply (simp add: nonzero_abs_inverse)

  2216 done

  2217

  2218 lemma nonzero_abs_divide:

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

  2220 by (simp add: divide_inverse abs_mult nonzero_abs_inverse)

  2221

  2222 lemma abs_divide [simp]:

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

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

  2225 apply (simp add: nonzero_abs_divide)

  2226 done

  2227

  2228 lemma abs_mult_less:

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

  2230 proof -

  2231   assume ac: "abs a < c"

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

  2233   assume "abs b < d"

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

  2235 qed

  2236

  2237 lemmas eq_minus_self_iff = equal_neg_zero

  2238

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

  2240   unfolding order_less_le less_eq_neg_nonpos equal_neg_zero ..

  2241

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

  2243 apply (simp add: order_less_le abs_le_iff)

  2244 apply (auto simp add: abs_if neg_less_eq_nonneg less_eq_neg_nonpos)

  2245 done

  2246

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

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

  2249   apply (subst abs_mult)

  2250   apply simp

  2251 done

  2252

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

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

  2255   apply (subst abs_divide)

  2256   apply (simp add: order_less_imp_le)

  2257 done

  2258

  2259

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

  2261

  2262 lemma mult_le_prts:

  2263   assumes

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

  2265   "a <= a2"

  2266   "b1 <= b"

  2267   "b <= b2"

  2268   shows

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

  2270 proof -

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

  2272     apply (subst prts[symmetric])+

  2273     apply simp

  2274     done

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

  2276     by (simp add: ring_simps)

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

  2278     by (simp_all add: prems mult_mono)

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

  2280   proof -

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

  2282       by (simp add: mult_left_mono prems)

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

  2284       by (simp add: mult_right_mono_neg prems)

  2285     ultimately show ?thesis

  2286       by simp

  2287   qed

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

  2289   proof -

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

  2291       by (simp add: mult_right_mono prems)

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

  2293       by (simp add: mult_left_mono_neg prems)

  2294     ultimately show ?thesis

  2295       by simp

  2296   qed

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

  2298   proof -

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

  2300       by (simp add: mult_left_mono_neg prems)

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

  2302       by (simp add: mult_right_mono_neg prems)

  2303     ultimately show ?thesis

  2304       by simp

  2305   qed

  2306   ultimately show ?thesis

  2307     by - (rule add_mono | simp)+

  2308 qed

  2309

  2310 lemma mult_ge_prts:

  2311   assumes

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

  2313   "a <= a2"

  2314   "b1 <= b"

  2315   "b <= b2"

  2316   shows

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

  2318 proof -

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

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

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

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

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

  2324     by (simp only: minus_le_iff)

  2325   then show ?thesis by simp

  2326 qed

  2327

  2328 end