src/HOL/Rings.thy
 author huffman Tue Mar 04 16:16:05 2014 -0800 (2014-03-04) changeset 55912 e12a0ab9917c parent 55187 6d0d93316daf child 56217 dc429a5b13c4 permissions -rw-r--r--
fix typo
     1 (*  Title:      HOL/Rings.thy

     2     Author:     Gertrud Bauer

     3     Author:     Steven Obua

     4     Author:     Tobias Nipkow

     5     Author:     Lawrence C Paulson

     6     Author:     Markus Wenzel

     7     Author:     Jeremy Avigad

     8 *)

     9

    10 header {* Rings *}

    11

    12 theory Rings

    13 imports Groups

    14 begin

    15

    16 class semiring = ab_semigroup_add + semigroup_mult +

    17   assumes distrib_right[algebra_simps, field_simps]: "(a + b) * c = a * c + b * c"

    18   assumes distrib_left[algebra_simps, field_simps]: "a * (b + c) = a * b + a * c"

    19 begin

    20

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

    22 lemma combine_common_factor:

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

    24 by (simp add: distrib_right add_ac)

    25

    26 end

    27

    28 class mult_zero = times + zero +

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

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

    31

    32 class semiring_0 = semiring + comm_monoid_add + mult_zero

    33

    34 class semiring_0_cancel = semiring + cancel_comm_monoid_add

    35 begin

    36

    37 subclass semiring_0

    38 proof

    39   fix a :: 'a

    40   have "0 * a + 0 * a = 0 * a + 0" by (simp add: distrib_right [symmetric])

    41   thus "0 * a = 0" by (simp only: add_left_cancel)

    42 next

    43   fix a :: 'a

    44   have "a * 0 + a * 0 = a * 0 + 0" by (simp add: distrib_left [symmetric])

    45   thus "a * 0 = 0" by (simp only: add_left_cancel)

    46 qed

    47

    48 end

    49

    50 class comm_semiring = ab_semigroup_add + ab_semigroup_mult +

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

    52 begin

    53

    54 subclass semiring

    55 proof

    56   fix a b c :: 'a

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

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

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

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

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

    62 qed

    63

    64 end

    65

    66 class comm_semiring_0 = comm_semiring + comm_monoid_add + mult_zero

    67 begin

    68

    69 subclass semiring_0 ..

    70

    71 end

    72

    73 class comm_semiring_0_cancel = comm_semiring + cancel_comm_monoid_add

    74 begin

    75

    76 subclass semiring_0_cancel ..

    77

    78 subclass comm_semiring_0 ..

    79

    80 end

    81

    82 class zero_neq_one = zero + one +

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

    84 begin

    85

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

    87 by (rule not_sym) (rule zero_neq_one)

    88

    89 definition of_bool :: "bool \<Rightarrow> 'a"

    90 where

    91   "of_bool p = (if p then 1 else 0)"

    92

    93 lemma of_bool_eq [simp, code]:

    94   "of_bool False = 0"

    95   "of_bool True = 1"

    96   by (simp_all add: of_bool_def)

    97

    98 lemma of_bool_eq_iff:

    99   "of_bool p = of_bool q \<longleftrightarrow> p = q"

   100   by (simp add: of_bool_def)

   101

   102 lemma split_of_bool [split]:

   103   "P (of_bool p) \<longleftrightarrow> (p \<longrightarrow> P 1) \<and> (\<not> p \<longrightarrow> P 0)"

   104   by (cases p) simp_all

   105

   106 lemma split_of_bool_asm:

   107   "P (of_bool p) \<longleftrightarrow> \<not> (p \<and> \<not> P 1 \<or> \<not> p \<and> \<not> P 0)"

   108   by (cases p) simp_all

   109

   110 end

   111

   112 class semiring_1 = zero_neq_one + semiring_0 + monoid_mult

   113

   114 text {* Abstract divisibility *}

   115

   116 class dvd = times

   117 begin

   118

   119 definition dvd :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "dvd" 50) where

   120   "b dvd a \<longleftrightarrow> (\<exists>k. a = b * k)"

   121

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

   123   unfolding dvd_def ..

   124

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

   126   unfolding dvd_def by blast

   127

   128 end

   129

   130 class comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult + dvd

   131   (*previously almost_semiring*)

   132 begin

   133

   134 subclass semiring_1 ..

   135

   136 lemma dvd_refl[simp]: "a dvd a"

   137 proof

   138   show "a = a * 1" by simp

   139 qed

   140

   141 lemma dvd_trans:

   142   assumes "a dvd b" and "b dvd c"

   143   shows "a dvd c"

   144 proof -

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

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

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

   148   then show ?thesis ..

   149 qed

   150

   151 lemma dvd_0_left_iff [simp]: "0 dvd a \<longleftrightarrow> a = 0"

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

   153

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

   155 proof

   156   show "0 = a * 0" by simp

   157 qed

   158

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

   160 by (auto intro!: dvdI)

   161

   162 lemma dvd_mult[simp]: "a dvd c \<Longrightarrow> a dvd (b * c)"

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

   164

   165 lemma dvd_mult2[simp]: "a dvd b \<Longrightarrow> a dvd (b * c)"

   166   apply (subst mult_commute)

   167   apply (erule dvd_mult)

   168   done

   169

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

   171 by (rule dvd_mult) (rule dvd_refl)

   172

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

   174 by (rule dvd_mult2) (rule dvd_refl)

   175

   176 lemma mult_dvd_mono:

   177   assumes "a dvd b"

   178     and "c dvd d"

   179   shows "a * c dvd b * d"

   180 proof -

   181   from a dvd b obtain b' where "b = a * b'" ..

   182   moreover from c dvd d obtain d' where "d = c * d'" ..

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

   184   then show ?thesis ..

   185 qed

   186

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

   188 by (simp add: dvd_def mult_assoc, blast)

   189

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

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

   192

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

   194 by simp

   195

   196 lemma dvd_add[simp]:

   197   assumes "a dvd b" and "a dvd c" shows "a dvd (b + c)"

   198 proof -

   199   from a dvd b obtain b' where "b = a * b'" ..

   200   moreover from a dvd c obtain c' where "c = a * c'" ..

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

   202   then show ?thesis ..

   203 qed

   204

   205 end

   206

   207 class no_zero_divisors = zero + times +

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

   209 begin

   210

   211 lemma divisors_zero:

   212   assumes "a * b = 0"

   213   shows "a = 0 \<or> b = 0"

   214 proof (rule classical)

   215   assume "\<not> (a = 0 \<or> b = 0)"

   216   then have "a \<noteq> 0" and "b \<noteq> 0" by auto

   217   with no_zero_divisors have "a * b \<noteq> 0" by blast

   218   with assms show ?thesis by simp

   219 qed

   220

   221 end

   222

   223 class semiring_1_cancel = semiring + cancel_comm_monoid_add

   224   + zero_neq_one + monoid_mult

   225 begin

   226

   227 subclass semiring_0_cancel ..

   228

   229 subclass semiring_1 ..

   230

   231 end

   232

   233 class comm_semiring_1_cancel = comm_semiring + cancel_comm_monoid_add

   234   + zero_neq_one + comm_monoid_mult

   235 begin

   236

   237 subclass semiring_1_cancel ..

   238 subclass comm_semiring_0_cancel ..

   239 subclass comm_semiring_1 ..

   240

   241 end

   242

   243 class ring = semiring + ab_group_add

   244 begin

   245

   246 subclass semiring_0_cancel ..

   247

   248 text {* Distribution rules *}

   249

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

   251 by (rule minus_unique) (simp add: distrib_right [symmetric])

   252

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

   254 by (rule minus_unique) (simp add: distrib_left [symmetric])

   255

   256 text{*Extract signs from products*}

   257 lemmas mult_minus_left [simp] = minus_mult_left [symmetric]

   258 lemmas mult_minus_right [simp] = minus_mult_right [symmetric]

   259

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

   261 by simp

   262

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

   264 by simp

   265

   266 lemma right_diff_distrib [algebra_simps, field_simps]:

   267   "a * (b - c) = a * b - a * c"

   268   using distrib_left [of a b "-c "] by simp

   269

   270 lemma left_diff_distrib [algebra_simps, field_simps]:

   271   "(a - b) * c = a * c - b * c"

   272   using distrib_right [of a "- b" c] by simp

   273

   274 lemmas ring_distribs =

   275   distrib_left distrib_right left_diff_distrib right_diff_distrib

   276

   277 lemma eq_add_iff1:

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

   279 by (simp add: algebra_simps)

   280

   281 lemma eq_add_iff2:

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

   283 by (simp add: algebra_simps)

   284

   285 end

   286

   287 lemmas ring_distribs =

   288   distrib_left distrib_right left_diff_distrib right_diff_distrib

   289

   290 class comm_ring = comm_semiring + ab_group_add

   291 begin

   292

   293 subclass ring ..

   294 subclass comm_semiring_0_cancel ..

   295

   296 lemma square_diff_square_factored:

   297   "x * x - y * y = (x + y) * (x - y)"

   298   by (simp add: algebra_simps)

   299

   300 end

   301

   302 class ring_1 = ring + zero_neq_one + monoid_mult

   303 begin

   304

   305 subclass semiring_1_cancel ..

   306

   307 lemma square_diff_one_factored:

   308   "x * x - 1 = (x + 1) * (x - 1)"

   309   by (simp add: algebra_simps)

   310

   311 end

   312

   313 class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult

   314   (*previously ring*)

   315 begin

   316

   317 subclass ring_1 ..

   318 subclass comm_semiring_1_cancel ..

   319

   320 lemma dvd_minus_iff [simp]: "x dvd - y \<longleftrightarrow> x dvd y"

   321 proof

   322   assume "x dvd - y"

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

   324   then show "x dvd y" by simp

   325 next

   326   assume "x dvd y"

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

   328   then show "x dvd - y" by simp

   329 qed

   330

   331 lemma minus_dvd_iff [simp]: "- x dvd y \<longleftrightarrow> x dvd y"

   332 proof

   333   assume "- x dvd y"

   334   then obtain k where "y = - x * k" ..

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

   336   then show "x dvd y" ..

   337 next

   338   assume "x dvd y"

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

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

   341   then show "- x dvd y" ..

   342 qed

   343

   344 lemma dvd_diff [simp]:

   345   "x dvd y \<Longrightarrow> x dvd z \<Longrightarrow> x dvd (y - z)"

   346   using dvd_add [of x y "- z"] by simp

   347

   348 end

   349

   350 class ring_no_zero_divisors = ring + no_zero_divisors

   351 begin

   352

   353 lemma mult_eq_0_iff [simp]:

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

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

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

   357     then show ?thesis using no_zero_divisors by simp

   358 next

   359   case True then show ?thesis by auto

   360 qed

   361

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

   363 lemma mult_cancel_right [simp]:

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

   365 proof -

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

   367     by (simp add: algebra_simps)

   368   thus ?thesis by (simp add: disj_commute)

   369 qed

   370

   371 lemma mult_cancel_left [simp]:

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

   373 proof -

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

   375     by (simp add: algebra_simps)

   376   thus ?thesis by simp

   377 qed

   378

   379 end

   380

   381 class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors

   382 begin

   383

   384 lemma square_eq_1_iff:

   385   "x * x = 1 \<longleftrightarrow> x = 1 \<or> x = - 1"

   386 proof -

   387   have "(x - 1) * (x + 1) = x * x - 1"

   388     by (simp add: algebra_simps)

   389   hence "x * x = 1 \<longleftrightarrow> (x - 1) * (x + 1) = 0"

   390     by simp

   391   thus ?thesis

   392     by (simp add: eq_neg_iff_add_eq_0)

   393 qed

   394

   395 lemma mult_cancel_right1 [simp]:

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

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

   398

   399 lemma mult_cancel_right2 [simp]:

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

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

   402

   403 lemma mult_cancel_left1 [simp]:

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

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

   406

   407 lemma mult_cancel_left2 [simp]:

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

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

   410

   411 end

   412

   413 class idom = comm_ring_1 + no_zero_divisors

   414 begin

   415

   416 subclass ring_1_no_zero_divisors ..

   417

   418 lemma square_eq_iff: "a * a = b * b \<longleftrightarrow> (a = b \<or> a = - b)"

   419 proof

   420   assume "a * a = b * b"

   421   then have "(a - b) * (a + b) = 0"

   422     by (simp add: algebra_simps)

   423   then show "a = b \<or> a = - b"

   424     by (simp add: eq_neg_iff_add_eq_0)

   425 next

   426   assume "a = b \<or> a = - b"

   427   then show "a * a = b * b" by auto

   428 qed

   429

   430 lemma dvd_mult_cancel_right [simp]:

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

   432 proof -

   433   have "a * c dvd b * c \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)"

   434     unfolding dvd_def by (simp add: mult_ac)

   435   also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b"

   436     unfolding dvd_def by simp

   437   finally show ?thesis .

   438 qed

   439

   440 lemma dvd_mult_cancel_left [simp]:

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

   442 proof -

   443   have "c * a dvd c * b \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)"

   444     unfolding dvd_def by (simp add: mult_ac)

   445   also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b"

   446     unfolding dvd_def by simp

   447   finally show ?thesis .

   448 qed

   449

   450 end

   451

   452 text {*

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

   454   \begin{itemize}

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

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

   457   \end{itemize}

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

   459   \begin{itemize}

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

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

   462   \end{itemize}

   463 *}

   464

   465 class ordered_semiring = semiring + comm_monoid_add + ordered_ab_semigroup_add +

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

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

   468 begin

   469

   470 lemma mult_mono:

   471   "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * d"

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

   473 apply (erule mult_left_mono, assumption)

   474 done

   475

   476 lemma mult_mono':

   477   "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * d"

   478 apply (rule mult_mono)

   479 apply (fast intro: order_trans)+

   480 done

   481

   482 end

   483

   484 class ordered_cancel_semiring = ordered_semiring + cancel_comm_monoid_add

   485 begin

   486

   487 subclass semiring_0_cancel ..

   488

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

   490 using mult_left_mono [of 0 b a] by simp

   491

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

   493 using mult_left_mono [of b 0 a] by simp

   494

   495 lemma mult_nonpos_nonneg: "a \<le> 0 \<Longrightarrow> 0 \<le> b \<Longrightarrow> a * b \<le> 0"

   496 using mult_right_mono [of a 0 b] by simp

   497

   498 text {* Legacy - use @{text mult_nonpos_nonneg} *}

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

   500 by (drule mult_right_mono [of b 0], auto)

   501

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

   503 by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)

   504

   505 end

   506

   507 class linordered_semiring = ordered_semiring + linordered_cancel_ab_semigroup_add

   508 begin

   509

   510 subclass ordered_cancel_semiring ..

   511

   512 subclass ordered_comm_monoid_add ..

   513

   514 lemma mult_left_less_imp_less:

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

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

   517

   518 lemma mult_right_less_imp_less:

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

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

   521

   522 end

   523

   524 class linordered_semiring_1 = linordered_semiring + semiring_1

   525 begin

   526

   527 lemma convex_bound_le:

   528   assumes "x \<le> a" "y \<le> a" "0 \<le> u" "0 \<le> v" "u + v = 1"

   529   shows "u * x + v * y \<le> a"

   530 proof-

   531   from assms have "u * x + v * y \<le> u * a + v * a"

   532     by (simp add: add_mono mult_left_mono)

   533   thus ?thesis using assms unfolding distrib_right[symmetric] by simp

   534 qed

   535

   536 end

   537

   538 class linordered_semiring_strict = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add +

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

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

   541 begin

   542

   543 subclass semiring_0_cancel ..

   544

   545 subclass linordered_semiring

   546 proof

   547   fix a b c :: 'a

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

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

   550     unfolding le_less

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

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

   553     unfolding le_less

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

   555 qed

   556

   557 lemma mult_left_le_imp_le:

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

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

   560

   561 lemma mult_right_le_imp_le:

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

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

   564

   565 lemma mult_pos_pos: "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a * b"

   566 using mult_strict_left_mono [of 0 b a] by simp

   567

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

   569 using mult_strict_left_mono [of b 0 a] by simp

   570

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

   572 using mult_strict_right_mono [of a 0 b] by simp

   573

   574 text {* Legacy - use @{text mult_neg_pos} *}

   575 lemma mult_pos_neg2: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> b * a < 0"

   576 by (drule mult_strict_right_mono [of b 0], auto)

   577

   578 lemma zero_less_mult_pos:

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

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

   581  apply (auto simp add: le_less not_less)

   582 apply (drule_tac mult_pos_neg [of a b])

   583  apply (auto dest: less_not_sym)

   584 done

   585

   586 lemma zero_less_mult_pos2:

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

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

   589  apply (auto simp add: le_less not_less)

   590 apply (drule_tac mult_pos_neg2 [of a b])

   591  apply (auto dest: less_not_sym)

   592 done

   593

   594 text{*Strict monotonicity in both arguments*}

   595 lemma mult_strict_mono:

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

   597   shows "a * c < b * d"

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

   599   apply (simp add: mult_pos_pos)

   600   apply (erule mult_strict_right_mono [THEN less_trans])

   601   apply (force simp add: le_less)

   602   apply (erule mult_strict_left_mono, assumption)

   603   done

   604

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

   606 lemma mult_strict_mono':

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

   608   shows "a * c < b * d"

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

   610

   611 lemma mult_less_le_imp_less:

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

   613   shows "a * c < b * d"

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

   615   apply (erule less_le_trans)

   616   apply (erule mult_left_mono)

   617   apply simp

   618   apply (erule mult_strict_right_mono)

   619   apply assumption

   620   done

   621

   622 lemma mult_le_less_imp_less:

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

   624   shows "a * c < b * d"

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

   626   apply (erule le_less_trans)

   627   apply (erule mult_strict_left_mono)

   628   apply simp

   629   apply (erule mult_right_mono)

   630   apply simp

   631   done

   632

   633 lemma mult_less_imp_less_left:

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

   635   shows "a < b"

   636 proof (rule ccontr)

   637   assume "\<not>  a < b"

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

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

   640   with this and less show False by (simp add: not_less [symmetric])

   641 qed

   642

   643 lemma mult_less_imp_less_right:

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

   645   shows "a < b"

   646 proof (rule ccontr)

   647   assume "\<not> a < b"

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

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

   650   with this and less show False by (simp add: not_less [symmetric])

   651 qed

   652

   653 end

   654

   655 class linordered_semiring_1_strict = linordered_semiring_strict + semiring_1

   656 begin

   657

   658 subclass linordered_semiring_1 ..

   659

   660 lemma convex_bound_lt:

   661   assumes "x < a" "y < a" "0 \<le> u" "0 \<le> v" "u + v = 1"

   662   shows "u * x + v * y < a"

   663 proof -

   664   from assms have "u * x + v * y < u * a + v * a"

   665     by (cases "u = 0")

   666        (auto intro!: add_less_le_mono mult_strict_left_mono mult_left_mono)

   667   thus ?thesis using assms unfolding distrib_right[symmetric] by simp

   668 qed

   669

   670 end

   671

   672 class ordered_comm_semiring = comm_semiring_0 + ordered_ab_semigroup_add +

   673   assumes comm_mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"

   674 begin

   675

   676 subclass ordered_semiring

   677 proof

   678   fix a b c :: 'a

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

   680   thus "c * a \<le> c * b" by (rule comm_mult_left_mono)

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

   682 qed

   683

   684 end

   685

   686 class ordered_cancel_comm_semiring = ordered_comm_semiring + cancel_comm_monoid_add

   687 begin

   688

   689 subclass comm_semiring_0_cancel ..

   690 subclass ordered_comm_semiring ..

   691 subclass ordered_cancel_semiring ..

   692

   693 end

   694

   695 class linordered_comm_semiring_strict = comm_semiring_0 + linordered_cancel_ab_semigroup_add +

   696   assumes comm_mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"

   697 begin

   698

   699 subclass linordered_semiring_strict

   700 proof

   701   fix a b c :: 'a

   702   assume "a < b" "0 < c"

   703   thus "c * a < c * b" by (rule comm_mult_strict_left_mono)

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

   705 qed

   706

   707 subclass ordered_cancel_comm_semiring

   708 proof

   709   fix a b c :: 'a

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

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

   712     unfolding le_less

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

   714 qed

   715

   716 end

   717

   718 class ordered_ring = ring + ordered_cancel_semiring

   719 begin

   720

   721 subclass ordered_ab_group_add ..

   722

   723 lemma less_add_iff1:

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

   725 by (simp add: algebra_simps)

   726

   727 lemma less_add_iff2:

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

   729 by (simp add: algebra_simps)

   730

   731 lemma le_add_iff1:

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

   733 by (simp add: algebra_simps)

   734

   735 lemma le_add_iff2:

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

   737 by (simp add: algebra_simps)

   738

   739 lemma mult_left_mono_neg:

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

   741   apply (drule mult_left_mono [of _ _ "- c"])

   742   apply simp_all

   743   done

   744

   745 lemma mult_right_mono_neg:

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

   747   apply (drule mult_right_mono [of _ _ "- c"])

   748   apply simp_all

   749   done

   750

   751 lemma mult_nonpos_nonpos: "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> 0 \<le> a * b"

   752 using mult_right_mono_neg [of a 0 b] by simp

   753

   754 lemma split_mult_pos_le:

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

   756 by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)

   757

   758 end

   759

   760 class linordered_ring = ring + linordered_semiring + linordered_ab_group_add + abs_if

   761 begin

   762

   763 subclass ordered_ring ..

   764

   765 subclass ordered_ab_group_add_abs

   766 proof

   767   fix a b

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

   769     by (auto simp add: abs_if not_le not_less algebra_simps simp del: add.commute dest: add_neg_neg add_nonneg_nonneg)

   770 qed (auto simp add: abs_if)

   771

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

   773   using linear [of 0 a]

   774   by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)

   775

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

   777   by (simp add: not_less)

   778

   779 end

   780

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

   782    Basically, linordered_ring + no_zero_divisors = linordered_ring_strict.

   783  *)

   784 class linordered_ring_strict = ring + linordered_semiring_strict

   785   + ordered_ab_group_add + abs_if

   786 begin

   787

   788 subclass linordered_ring ..

   789

   790 lemma mult_strict_left_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> c * a < c * b"

   791 using mult_strict_left_mono [of b a "- c"] by simp

   792

   793 lemma mult_strict_right_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> a * c < b * c"

   794 using mult_strict_right_mono [of b a "- c"] by simp

   795

   796 lemma mult_neg_neg: "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> 0 < a * b"

   797 using mult_strict_right_mono_neg [of a 0 b] by simp

   798

   799 subclass ring_no_zero_divisors

   800 proof

   801   fix a b

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

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

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

   805   proof (cases "a < 0")

   806     case True note A' = this

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

   808       case True with A'

   809       show ?thesis by (auto dest: mult_neg_neg)

   810     next

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

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

   813     qed

   814   next

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

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

   817       case True with A'

   818       show ?thesis by (auto dest: mult_strict_right_mono_neg)

   819     next

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

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

   822     qed

   823   qed

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

   825 qed

   826

   827 lemma zero_less_mult_iff:

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

   829   apply (auto simp add: mult_pos_pos mult_neg_neg)

   830   apply (simp_all add: not_less le_less)

   831   apply (erule disjE) apply assumption defer

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

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

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

   835   apply (drule sym) apply simp

   836   apply (blast dest: zero_less_mult_pos)

   837   apply (blast dest: zero_less_mult_pos2)

   838   done

   839

   840 lemma zero_le_mult_iff:

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

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

   843

   844 lemma mult_less_0_iff:

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

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

   847   apply force

   848   done

   849

   850 lemma mult_le_0_iff:

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

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

   853   apply force

   854   done

   855

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

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

   858

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

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

   861

   862 lemma mult_less_cancel_right_disj:

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

   864   apply (cases "c = 0")

   865   apply (auto simp add: neq_iff mult_strict_right_mono

   866                       mult_strict_right_mono_neg)

   867   apply (auto simp add: not_less

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

   869                       not_le [symmetric, of a])

   870   apply (erule_tac [!] notE)

   871   apply (auto simp add: less_imp_le mult_right_mono

   872                       mult_right_mono_neg)

   873   done

   874

   875 lemma mult_less_cancel_left_disj:

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

   877   apply (cases "c = 0")

   878   apply (auto simp add: neq_iff mult_strict_left_mono

   879                       mult_strict_left_mono_neg)

   880   apply (auto simp add: not_less

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

   882                       not_le [symmetric, of a])

   883   apply (erule_tac [!] notE)

   884   apply (auto simp add: less_imp_le mult_left_mono

   885                       mult_left_mono_neg)

   886   done

   887

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

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

   890

   891 lemma mult_less_cancel_right:

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

   893   using mult_less_cancel_right_disj [of a c b] by auto

   894

   895 lemma mult_less_cancel_left:

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

   897   using mult_less_cancel_left_disj [of c a b] by auto

   898

   899 lemma mult_le_cancel_right:

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

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

   902

   903 lemma mult_le_cancel_left:

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

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

   906

   907 lemma mult_le_cancel_left_pos:

   908   "0 < c \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> a \<le> b"

   909 by (auto simp: mult_le_cancel_left)

   910

   911 lemma mult_le_cancel_left_neg:

   912   "c < 0 \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> b \<le> a"

   913 by (auto simp: mult_le_cancel_left)

   914

   915 lemma mult_less_cancel_left_pos:

   916   "0 < c \<Longrightarrow> c * a < c * b \<longleftrightarrow> a < b"

   917 by (auto simp: mult_less_cancel_left)

   918

   919 lemma mult_less_cancel_left_neg:

   920   "c < 0 \<Longrightarrow> c * a < c * b \<longleftrightarrow> b < a"

   921 by (auto simp: mult_less_cancel_left)

   922

   923 end

   924

   925 lemmas mult_sign_intros =

   926   mult_nonneg_nonneg mult_nonneg_nonpos

   927   mult_nonpos_nonneg mult_nonpos_nonpos

   928   mult_pos_pos mult_pos_neg

   929   mult_neg_pos mult_neg_neg

   930

   931 class ordered_comm_ring = comm_ring + ordered_comm_semiring

   932 begin

   933

   934 subclass ordered_ring ..

   935 subclass ordered_cancel_comm_semiring ..

   936

   937 end

   938

   939 class linordered_semidom = comm_semiring_1_cancel + linordered_comm_semiring_strict +

   940   (*previously linordered_semiring*)

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

   942 begin

   943

   944 lemma pos_add_strict:

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

   946   using add_strict_mono [of 0 a b c] by simp

   947

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

   949 by (rule zero_less_one [THEN less_imp_le])

   950

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

   952 by (simp add: not_le)

   953

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

   955 by (simp add: not_less)

   956

   957 lemma less_1_mult:

   958   assumes "1 < m" and "1 < n"

   959   shows "1 < m * n"

   960   using assms mult_strict_mono [of 1 m 1 n]

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

   962

   963 end

   964

   965 class linordered_idom = comm_ring_1 +

   966   linordered_comm_semiring_strict + ordered_ab_group_add +

   967   abs_if + sgn_if

   968   (*previously linordered_ring*)

   969 begin

   970

   971 subclass linordered_semiring_1_strict ..

   972 subclass linordered_ring_strict ..

   973 subclass ordered_comm_ring ..

   974 subclass idom ..

   975

   976 subclass linordered_semidom

   977 proof

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

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

   980 qed

   981

   982 lemma linorder_neqE_linordered_idom:

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

   984   using assms by (rule neqE)

   985

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

   987

   988 lemma mult_le_cancel_right1:

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

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

   991

   992 lemma mult_le_cancel_right2:

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

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

   995

   996 lemma mult_le_cancel_left1:

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

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

   999

  1000 lemma mult_le_cancel_left2:

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

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

  1003

  1004 lemma mult_less_cancel_right1:

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

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

  1007

  1008 lemma mult_less_cancel_right2:

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

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

  1011

  1012 lemma mult_less_cancel_left1:

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

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

  1015

  1016 lemma mult_less_cancel_left2:

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

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

  1019

  1020 lemma sgn_sgn [simp]:

  1021   "sgn (sgn a) = sgn a"

  1022 unfolding sgn_if by simp

  1023

  1024 lemma sgn_0_0:

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

  1026 unfolding sgn_if by simp

  1027

  1028 lemma sgn_1_pos:

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

  1030 unfolding sgn_if by simp

  1031

  1032 lemma sgn_1_neg:

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

  1034 unfolding sgn_if by auto

  1035

  1036 lemma sgn_pos [simp]:

  1037   "0 < a \<Longrightarrow> sgn a = 1"

  1038 unfolding sgn_1_pos .

  1039

  1040 lemma sgn_neg [simp]:

  1041   "a < 0 \<Longrightarrow> sgn a = - 1"

  1042 unfolding sgn_1_neg .

  1043

  1044 lemma sgn_times:

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

  1046 by (auto simp add: sgn_if zero_less_mult_iff)

  1047

  1048 lemma abs_sgn: "\<bar>k\<bar> = k * sgn k"

  1049 unfolding sgn_if abs_if by auto

  1050

  1051 lemma sgn_greater [simp]:

  1052   "0 < sgn a \<longleftrightarrow> 0 < a"

  1053   unfolding sgn_if by auto

  1054

  1055 lemma sgn_less [simp]:

  1056   "sgn a < 0 \<longleftrightarrow> a < 0"

  1057   unfolding sgn_if by auto

  1058

  1059 lemma abs_dvd_iff [simp]: "\<bar>m\<bar> dvd k \<longleftrightarrow> m dvd k"

  1060   by (simp add: abs_if)

  1061

  1062 lemma dvd_abs_iff [simp]: "m dvd \<bar>k\<bar> \<longleftrightarrow> m dvd k"

  1063   by (simp add: abs_if)

  1064

  1065 lemma dvd_if_abs_eq:

  1066   "\<bar>l\<bar> = \<bar>k\<bar> \<Longrightarrow> l dvd k"

  1067 by(subst abs_dvd_iff[symmetric]) simp

  1068

  1069 text {* The following lemmas can be proven in more general structures, but

  1070 are dangerous as simp rules in absence of @{thm neg_equal_zero},

  1071 @{thm neg_less_pos}, @{thm neg_less_eq_nonneg}. *}

  1072

  1073 lemma equation_minus_iff_1 [simp, no_atp]:

  1074   "1 = - a \<longleftrightarrow> a = - 1"

  1075   by (fact equation_minus_iff)

  1076

  1077 lemma minus_equation_iff_1 [simp, no_atp]:

  1078   "- a = 1 \<longleftrightarrow> a = - 1"

  1079   by (subst minus_equation_iff, auto)

  1080

  1081 lemma le_minus_iff_1 [simp, no_atp]:

  1082   "1 \<le> - b \<longleftrightarrow> b \<le> - 1"

  1083   by (fact le_minus_iff)

  1084

  1085 lemma minus_le_iff_1 [simp, no_atp]:

  1086   "- a \<le> 1 \<longleftrightarrow> - 1 \<le> a"

  1087   by (fact minus_le_iff)

  1088

  1089 lemma less_minus_iff_1 [simp, no_atp]:

  1090   "1 < - b \<longleftrightarrow> b < - 1"

  1091   by (fact less_minus_iff)

  1092

  1093 lemma minus_less_iff_1 [simp, no_atp]:

  1094   "- a < 1 \<longleftrightarrow> - 1 < a"

  1095   by (fact minus_less_iff)

  1096

  1097 end

  1098

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

  1100

  1101 lemmas mult_compare_simps =

  1102     mult_le_cancel_right mult_le_cancel_left

  1103     mult_le_cancel_right1 mult_le_cancel_right2

  1104     mult_le_cancel_left1 mult_le_cancel_left2

  1105     mult_less_cancel_right mult_less_cancel_left

  1106     mult_less_cancel_right1 mult_less_cancel_right2

  1107     mult_less_cancel_left1 mult_less_cancel_left2

  1108     mult_cancel_right mult_cancel_left

  1109     mult_cancel_right1 mult_cancel_right2

  1110     mult_cancel_left1 mult_cancel_left2

  1111

  1112 text {* Reasoning about inequalities with division *}

  1113

  1114 context linordered_semidom

  1115 begin

  1116

  1117 lemma less_add_one: "a < a + 1"

  1118 proof -

  1119   have "a + 0 < a + 1"

  1120     by (blast intro: zero_less_one add_strict_left_mono)

  1121   thus ?thesis by simp

  1122 qed

  1123

  1124 lemma zero_less_two: "0 < 1 + 1"

  1125 by (blast intro: less_trans zero_less_one less_add_one)

  1126

  1127 end

  1128

  1129 context linordered_idom

  1130 begin

  1131

  1132 lemma mult_right_le_one_le:

  1133   "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> x * y \<le> x"

  1134   by (auto simp add: mult_le_cancel_left2)

  1135

  1136 lemma mult_left_le_one_le:

  1137   "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> y * x \<le> x"

  1138   by (auto simp add: mult_le_cancel_right2)

  1139

  1140 end

  1141

  1142 text {* Absolute Value *}

  1143

  1144 context linordered_idom

  1145 begin

  1146

  1147 lemma mult_sgn_abs:

  1148   "sgn x * \<bar>x\<bar> = x"

  1149   unfolding abs_if sgn_if by auto

  1150

  1151 lemma abs_one [simp]:

  1152   "\<bar>1\<bar> = 1"

  1153   by (simp add: abs_if)

  1154

  1155 end

  1156

  1157 class ordered_ring_abs = ordered_ring + ordered_ab_group_add_abs +

  1158   assumes abs_eq_mult:

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

  1160

  1161 context linordered_idom

  1162 begin

  1163

  1164 subclass ordered_ring_abs proof

  1165 qed (auto simp add: abs_if not_less mult_less_0_iff)

  1166

  1167 lemma abs_mult:

  1168   "\<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>"

  1169   by (rule abs_eq_mult) auto

  1170

  1171 lemma abs_mult_self:

  1172   "\<bar>a\<bar> * \<bar>a\<bar> = a * a"

  1173   by (simp add: abs_if)

  1174

  1175 lemma abs_mult_less:

  1176   "\<bar>a\<bar> < c \<Longrightarrow> \<bar>b\<bar> < d \<Longrightarrow> \<bar>a\<bar> * \<bar>b\<bar> < c * d"

  1177 proof -

  1178   assume ac: "\<bar>a\<bar> < c"

  1179   hence cpos: "0<c" by (blast intro: le_less_trans abs_ge_zero)

  1180   assume "\<bar>b\<bar> < d"

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

  1182 qed

  1183

  1184 lemma abs_less_iff:

  1185   "\<bar>a\<bar> < b \<longleftrightarrow> a < b \<and> - a < b"

  1186   by (simp add: less_le abs_le_iff) (auto simp add: abs_if)

  1187

  1188 lemma abs_mult_pos:

  1189   "0 \<le> x \<Longrightarrow> \<bar>y\<bar> * x = \<bar>y * x\<bar>"

  1190   by (simp add: abs_mult)

  1191

  1192 lemma abs_diff_less_iff:

  1193   "\<bar>x - a\<bar> < r \<longleftrightarrow> a - r < x \<and> x < a + r"

  1194   by (auto simp add: diff_less_eq ac_simps abs_less_iff)

  1195

  1196 end

  1197

  1198 code_identifier

  1199   code_module Rings \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith

  1200

  1201 end

  1202