src/HOL/Rings.thy
 author wenzelm Fri Dec 17 17:43:54 2010 +0100 (2010-12-17) changeset 41229 d797baa3d57c parent 38642 8fa437809c67 child 44064 5bce8ff0d9ae permissions -rw-r--r--
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
     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 left_distrib[algebra_simps, field_simps]: "(a + b) * c = a * c + b * c"

    18   assumes right_distrib[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: left_distrib 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: left_distrib [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: right_distrib [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 end

    90

    91 class semiring_1 = zero_neq_one + semiring_0 + monoid_mult

    92

    93 text {* Abstract divisibility *}

    94

    95 class dvd = times

    96 begin

    97

    98 definition dvd :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "dvd" 50) where

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

   100

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

   102   unfolding dvd_def ..

   103

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

   105   unfolding dvd_def by blast

   106

   107 end

   108

   109 class comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult + dvd

   110   (*previously almost_semiring*)

   111 begin

   112

   113 subclass semiring_1 ..

   114

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

   116 proof

   117   show "a = a * 1" by simp

   118 qed

   119

   120 lemma dvd_trans:

   121   assumes "a dvd b" and "b dvd c"

   122   shows "a dvd c"

   123 proof -

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

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

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

   127   then show ?thesis ..

   128 qed

   129

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

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

   132

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

   134 proof

   135   show "0 = a * 0" by simp

   136 qed

   137

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

   139 by (auto intro!: dvdI)

   140

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

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

   143

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

   145   apply (subst mult_commute)

   146   apply (erule dvd_mult)

   147   done

   148

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

   150 by (rule dvd_mult) (rule dvd_refl)

   151

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

   153 by (rule dvd_mult2) (rule dvd_refl)

   154

   155 lemma mult_dvd_mono:

   156   assumes "a dvd b"

   157     and "c dvd d"

   158   shows "a * c dvd b * d"

   159 proof -

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

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

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

   163   then show ?thesis ..

   164 qed

   165

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

   167 by (simp add: dvd_def mult_assoc, blast)

   168

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

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

   171

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

   173 by simp

   174

   175 lemma dvd_add[simp]:

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

   177 proof -

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

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

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

   181   then show ?thesis ..

   182 qed

   183

   184 end

   185

   186 class no_zero_divisors = zero + times +

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

   188 begin

   189

   190 lemma divisors_zero:

   191   assumes "a * b = 0"

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

   193 proof (rule classical)

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

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

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

   197   with assms show ?thesis by simp

   198 qed

   199

   200 end

   201

   202 class semiring_1_cancel = semiring + cancel_comm_monoid_add

   203   + zero_neq_one + monoid_mult

   204 begin

   205

   206 subclass semiring_0_cancel ..

   207

   208 subclass semiring_1 ..

   209

   210 end

   211

   212 class comm_semiring_1_cancel = comm_semiring + cancel_comm_monoid_add

   213   + zero_neq_one + comm_monoid_mult

   214 begin

   215

   216 subclass semiring_1_cancel ..

   217 subclass comm_semiring_0_cancel ..

   218 subclass comm_semiring_1 ..

   219

   220 end

   221

   222 class ring = semiring + ab_group_add

   223 begin

   224

   225 subclass semiring_0_cancel ..

   226

   227 text {* Distribution rules *}

   228

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

   230 by (rule minus_unique) (simp add: left_distrib [symmetric])

   231

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

   233 by (rule minus_unique) (simp add: right_distrib [symmetric])

   234

   235 text{*Extract signs from products*}

   236 lemmas mult_minus_left [simp, no_atp] = minus_mult_left [symmetric]

   237 lemmas mult_minus_right [simp,no_atp] = minus_mult_right [symmetric]

   238

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

   240 by simp

   241

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

   243 by simp

   244

   245 lemma right_diff_distrib[algebra_simps, field_simps]: "a * (b - c) = a * b - a * c"

   246 by (simp add: right_distrib diff_minus)

   247

   248 lemma left_diff_distrib[algebra_simps, field_simps]: "(a - b) * c = a * c - b * c"

   249 by (simp add: left_distrib diff_minus)

   250

   251 lemmas ring_distribs[no_atp] =

   252   right_distrib left_distrib left_diff_distrib right_diff_distrib

   253

   254 lemma eq_add_iff1:

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

   256 by (simp add: algebra_simps)

   257

   258 lemma eq_add_iff2:

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

   260 by (simp add: algebra_simps)

   261

   262 end

   263

   264 lemmas ring_distribs[no_atp] =

   265   right_distrib left_distrib left_diff_distrib right_diff_distrib

   266

   267 class comm_ring = comm_semiring + ab_group_add

   268 begin

   269

   270 subclass ring ..

   271 subclass comm_semiring_0_cancel ..

   272

   273 end

   274

   275 class ring_1 = ring + zero_neq_one + monoid_mult

   276 begin

   277

   278 subclass semiring_1_cancel ..

   279

   280 end

   281

   282 class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult

   283   (*previously ring*)

   284 begin

   285

   286 subclass ring_1 ..

   287 subclass comm_semiring_1_cancel ..

   288

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

   290 proof

   291   assume "x dvd - y"

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

   293   then show "x dvd y" by simp

   294 next

   295   assume "x dvd y"

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

   297   then show "x dvd - y" by simp

   298 qed

   299

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

   301 proof

   302   assume "- x dvd y"

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

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

   305   then show "x dvd y" ..

   306 next

   307   assume "x dvd y"

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

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

   310   then show "- x dvd y" ..

   311 qed

   312

   313 lemma dvd_diff[simp]: "x dvd y \<Longrightarrow> x dvd z \<Longrightarrow> x dvd (y - z)"

   314 by (simp only: diff_minus dvd_add dvd_minus_iff)

   315

   316 end

   317

   318 class ring_no_zero_divisors = ring + no_zero_divisors

   319 begin

   320

   321 lemma mult_eq_0_iff [simp]:

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

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

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

   325     then show ?thesis using no_zero_divisors by simp

   326 next

   327   case True then show ?thesis by auto

   328 qed

   329

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

   331 lemma mult_cancel_right [simp, no_atp]:

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

   333 proof -

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

   335     by (simp add: algebra_simps)

   336   thus ?thesis by (simp add: disj_commute)

   337 qed

   338

   339 lemma mult_cancel_left [simp, no_atp]:

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

   341 proof -

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

   343     by (simp add: algebra_simps)

   344   thus ?thesis by simp

   345 qed

   346

   347 end

   348

   349 class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors

   350 begin

   351

   352 lemma square_eq_1_iff:

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

   354 proof -

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

   356     by (simp add: algebra_simps)

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

   358     by simp

   359   thus ?thesis

   360     by (simp add: eq_neg_iff_add_eq_0)

   361 qed

   362

   363 lemma mult_cancel_right1 [simp]:

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

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

   366

   367 lemma mult_cancel_right2 [simp]:

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

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

   370

   371 lemma mult_cancel_left1 [simp]:

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

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

   374

   375 lemma mult_cancel_left2 [simp]:

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

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

   378

   379 end

   380

   381 class idom = comm_ring_1 + no_zero_divisors

   382 begin

   383

   384 subclass ring_1_no_zero_divisors ..

   385

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

   387 proof

   388   assume "a * a = b * b"

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

   390     by (simp add: algebra_simps)

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

   392     by (simp add: eq_neg_iff_add_eq_0)

   393 next

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

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

   396 qed

   397

   398 lemma dvd_mult_cancel_right [simp]:

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

   400 proof -

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

   402     unfolding dvd_def by (simp add: mult_ac)

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

   404     unfolding dvd_def by simp

   405   finally show ?thesis .

   406 qed

   407

   408 lemma dvd_mult_cancel_left [simp]:

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

   410 proof -

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

   412     unfolding dvd_def by (simp add: mult_ac)

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

   414     unfolding dvd_def by simp

   415   finally show ?thesis .

   416 qed

   417

   418 end

   419

   420 class inverse =

   421   fixes inverse :: "'a \<Rightarrow> 'a"

   422     and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "'/" 70)

   423

   424 class division_ring = ring_1 + inverse +

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

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

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

   428 begin

   429

   430 subclass ring_1_no_zero_divisors

   431 proof

   432   fix a b :: 'a

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

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

   435   proof

   436     assume ab: "a * b = 0"

   437     hence "0 = inverse a * (a * b) * inverse b" by simp

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

   439       by (simp only: mult_assoc)

   440     also have "\<dots> = 1" using a b by simp

   441     finally show False by simp

   442   qed

   443 qed

   444

   445 lemma nonzero_imp_inverse_nonzero:

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

   447 proof

   448   assume ianz: "inverse a = 0"

   449   assume "a \<noteq> 0"

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

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

   452   finally have "1 = 0" .

   453   thus False by (simp add: eq_commute)

   454 qed

   455

   456 lemma inverse_zero_imp_zero:

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

   458 apply (rule classical)

   459 apply (drule nonzero_imp_inverse_nonzero)

   460 apply auto

   461 done

   462

   463 lemma inverse_unique:

   464   assumes ab: "a * b = 1"

   465   shows "inverse a = b"

   466 proof -

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

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

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

   470 qed

   471

   472 lemma nonzero_inverse_minus_eq:

   473   "a \<noteq> 0 \<Longrightarrow> inverse (- a) = - inverse a"

   474 by (rule inverse_unique) simp

   475

   476 lemma nonzero_inverse_inverse_eq:

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

   478 by (rule inverse_unique) simp

   479

   480 lemma nonzero_inverse_eq_imp_eq:

   481   assumes "inverse a = inverse b" and "a \<noteq> 0" and "b \<noteq> 0"

   482   shows "a = b"

   483 proof -

   484   from inverse a = inverse b

   485   have "inverse (inverse a) = inverse (inverse b)" by (rule arg_cong)

   486   with a \<noteq> 0 and b \<noteq> 0 show "a = b"

   487     by (simp add: nonzero_inverse_inverse_eq)

   488 qed

   489

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

   491 by (rule inverse_unique) simp

   492

   493 lemma nonzero_inverse_mult_distrib:

   494   assumes "a \<noteq> 0" and "b \<noteq> 0"

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

   496 proof -

   497   have "a * (b * inverse b) * inverse a = 1" using assms by simp

   498   hence "a * b * (inverse b * inverse a) = 1" by (simp only: mult_assoc)

   499   thus ?thesis by (rule inverse_unique)

   500 qed

   501

   502 lemma division_ring_inverse_add:

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

   504 by (simp add: algebra_simps)

   505

   506 lemma division_ring_inverse_diff:

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

   508 by (simp add: algebra_simps)

   509

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

   511 proof

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

   513   {

   514     hence "a = (a / b) * b" by (simp add: divide_inverse mult_assoc)

   515     also assume "a / b = 1"

   516     finally show "a = b" by simp

   517   next

   518     assume "a = b"

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

   520   }

   521 qed

   522

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

   524 by (simp add: divide_inverse)

   525

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

   527 by (simp add: divide_inverse)

   528

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

   530 by (simp add: divide_inverse)

   531

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

   533 by (simp add: divide_inverse)

   534

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

   536 by (simp add: divide_inverse algebra_simps)

   537

   538 lemma divide_1 [simp]: "a / 1 = a"

   539   by (simp add: divide_inverse)

   540

   541 lemma times_divide_eq_right [simp]: "a * (b / c) = (a * b) / c"

   542   by (simp add: divide_inverse mult_assoc)

   543

   544 lemma minus_divide_left: "- (a / b) = (-a) / b"

   545   by (simp add: divide_inverse)

   546

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

   548   by (simp add: divide_inverse nonzero_inverse_minus_eq)

   549

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

   551   by (simp add: divide_inverse nonzero_inverse_minus_eq)

   552

   553 lemma divide_minus_left [simp, no_atp]: "(-a) / b = - (a / b)"

   554   by (simp add: divide_inverse)

   555

   556 lemma diff_divide_distrib: "(a - b) / c = a / c - b / c"

   557   by (simp add: diff_minus add_divide_distrib)

   558

   559 lemma nonzero_eq_divide_eq [field_simps]: "c \<noteq> 0 \<Longrightarrow> a = b / c \<longleftrightarrow> a * c = b"

   560 proof -

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

   562   have "a = b / c \<longleftrightarrow> a * c = (b / c) * c" by simp

   563   also have "... \<longleftrightarrow> a * c = b" by (simp add: divide_inverse mult_assoc)

   564   finally show ?thesis .

   565 qed

   566

   567 lemma nonzero_divide_eq_eq [field_simps]: "c \<noteq> 0 \<Longrightarrow> b / c = a \<longleftrightarrow> b = a * c"

   568 proof -

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

   570   have "b / c = a \<longleftrightarrow> (b / c) * c = a * c" by simp

   571   also have "... \<longleftrightarrow> b = a * c" by (simp add: divide_inverse mult_assoc)

   572   finally show ?thesis .

   573 qed

   574

   575 lemma divide_eq_imp: "c \<noteq> 0 \<Longrightarrow> b = a * c \<Longrightarrow> b / c = a"

   576   by (simp add: divide_inverse mult_assoc)

   577

   578 lemma eq_divide_imp: "c \<noteq> 0 \<Longrightarrow> a * c = b \<Longrightarrow> a = b / c"

   579   by (drule sym) (simp add: divide_inverse mult_assoc)

   580

   581 end

   582

   583 class division_ring_inverse_zero = division_ring +

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

   585 begin

   586

   587 lemma divide_zero [simp]:

   588   "a / 0 = 0"

   589   by (simp add: divide_inverse)

   590

   591 lemma divide_self_if [simp]:

   592   "a / a = (if a = 0 then 0 else 1)"

   593   by simp

   594

   595 lemma inverse_nonzero_iff_nonzero [simp]:

   596   "inverse a = 0 \<longleftrightarrow> a = 0"

   597   by rule (fact inverse_zero_imp_zero, simp)

   598

   599 lemma inverse_minus_eq [simp]:

   600   "inverse (- a) = - inverse a"

   601 proof cases

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

   603 next

   604   assume "a\<noteq>0"

   605   thus ?thesis by (simp add: nonzero_inverse_minus_eq)

   606 qed

   607

   608 lemma inverse_eq_imp_eq:

   609   "inverse a = inverse b \<Longrightarrow> a = b"

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

   611  apply (force dest!: inverse_zero_imp_zero

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

   613 apply (force dest!: nonzero_inverse_eq_imp_eq)

   614 done

   615

   616 lemma inverse_eq_iff_eq [simp]:

   617   "inverse a = inverse b \<longleftrightarrow> a = b"

   618   by (force dest!: inverse_eq_imp_eq)

   619

   620 lemma inverse_inverse_eq [simp]:

   621   "inverse (inverse a) = a"

   622 proof cases

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

   624 next

   625   assume "a\<noteq>0"

   626   thus ?thesis by (simp add: nonzero_inverse_inverse_eq)

   627 qed

   628

   629 end

   630

   631 text {*

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

   633   \begin{itemize}

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

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

   636   \end{itemize}

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

   638   \begin{itemize}

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

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

   641   \end{itemize}

   642 *}

   643

   644 class ordered_semiring = semiring + comm_monoid_add + ordered_ab_semigroup_add +

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

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

   647 begin

   648

   649 lemma mult_mono:

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

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

   652 apply (erule mult_left_mono, assumption)

   653 done

   654

   655 lemma mult_mono':

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

   657 apply (rule mult_mono)

   658 apply (fast intro: order_trans)+

   659 done

   660

   661 end

   662

   663 class ordered_cancel_semiring = ordered_semiring + cancel_comm_monoid_add

   664 begin

   665

   666 subclass semiring_0_cancel ..

   667

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

   669 using mult_left_mono [of 0 b a] by simp

   670

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

   672 using mult_left_mono [of b 0 a] by simp

   673

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

   675 using mult_right_mono [of a 0 b] by simp

   676

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

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

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

   680

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

   682 by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)

   683

   684 end

   685

   686 class linordered_semiring = ordered_semiring + linordered_cancel_ab_semigroup_add

   687 begin

   688

   689 subclass ordered_cancel_semiring ..

   690

   691 subclass ordered_comm_monoid_add ..

   692

   693 lemma mult_left_less_imp_less:

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

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

   696

   697 lemma mult_right_less_imp_less:

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

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

   700

   701 end

   702

   703 class linordered_semiring_1 = linordered_semiring + semiring_1

   704 begin

   705

   706 lemma convex_bound_le:

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

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

   709 proof-

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

   711     by (simp add: add_mono mult_left_mono)

   712   thus ?thesis using assms unfolding left_distrib[symmetric] by simp

   713 qed

   714

   715 end

   716

   717 class linordered_semiring_strict = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add +

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

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

   720 begin

   721

   722 subclass semiring_0_cancel ..

   723

   724 subclass linordered_semiring

   725 proof

   726   fix a b c :: 'a

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

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

   729     unfolding le_less

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

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

   732     unfolding le_less

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

   734 qed

   735

   736 lemma mult_left_le_imp_le:

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

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

   739

   740 lemma mult_right_le_imp_le:

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

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

   743

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

   745 using mult_strict_left_mono [of 0 b a] by simp

   746

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

   748 using mult_strict_left_mono [of b 0 a] by simp

   749

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

   751 using mult_strict_right_mono [of a 0 b] by simp

   752

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

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

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

   756

   757 lemma zero_less_mult_pos:

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

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

   760  apply (auto simp add: le_less not_less)

   761 apply (drule_tac mult_pos_neg [of a b])

   762  apply (auto dest: less_not_sym)

   763 done

   764

   765 lemma zero_less_mult_pos2:

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

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

   768  apply (auto simp add: le_less not_less)

   769 apply (drule_tac mult_pos_neg2 [of a b])

   770  apply (auto dest: less_not_sym)

   771 done

   772

   773 text{*Strict monotonicity in both arguments*}

   774 lemma mult_strict_mono:

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

   776   shows "a * c < b * d"

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

   778   apply (simp add: mult_pos_pos)

   779   apply (erule mult_strict_right_mono [THEN less_trans])

   780   apply (force simp add: le_less)

   781   apply (erule mult_strict_left_mono, assumption)

   782   done

   783

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

   785 lemma mult_strict_mono':

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

   787   shows "a * c < b * d"

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

   789

   790 lemma mult_less_le_imp_less:

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

   792   shows "a * c < b * d"

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

   794   apply (erule less_le_trans)

   795   apply (erule mult_left_mono)

   796   apply simp

   797   apply (erule mult_strict_right_mono)

   798   apply assumption

   799   done

   800

   801 lemma mult_le_less_imp_less:

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

   803   shows "a * c < b * d"

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

   805   apply (erule le_less_trans)

   806   apply (erule mult_strict_left_mono)

   807   apply simp

   808   apply (erule mult_right_mono)

   809   apply simp

   810   done

   811

   812 lemma mult_less_imp_less_left:

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

   814   shows "a < b"

   815 proof (rule ccontr)

   816   assume "\<not>  a < b"

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

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

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

   820 qed

   821

   822 lemma mult_less_imp_less_right:

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

   824   shows "a < b"

   825 proof (rule ccontr)

   826   assume "\<not> a < b"

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

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

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

   830 qed

   831

   832 end

   833

   834 class linordered_semiring_1_strict = linordered_semiring_strict + semiring_1

   835 begin

   836

   837 subclass linordered_semiring_1 ..

   838

   839 lemma convex_bound_lt:

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

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

   842 proof -

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

   844     by (cases "u = 0")

   845        (auto intro!: add_less_le_mono mult_strict_left_mono mult_left_mono)

   846   thus ?thesis using assms unfolding left_distrib[symmetric] by simp

   847 qed

   848

   849 end

   850

   851 class ordered_comm_semiring = comm_semiring_0 + ordered_ab_semigroup_add +

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

   853 begin

   854

   855 subclass ordered_semiring

   856 proof

   857   fix a b c :: 'a

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

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

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

   861 qed

   862

   863 end

   864

   865 class ordered_cancel_comm_semiring = ordered_comm_semiring + cancel_comm_monoid_add

   866 begin

   867

   868 subclass comm_semiring_0_cancel ..

   869 subclass ordered_comm_semiring ..

   870 subclass ordered_cancel_semiring ..

   871

   872 end

   873

   874 class linordered_comm_semiring_strict = comm_semiring_0 + linordered_cancel_ab_semigroup_add +

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

   876 begin

   877

   878 subclass linordered_semiring_strict

   879 proof

   880   fix a b c :: 'a

   881   assume "a < b" "0 < c"

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

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

   884 qed

   885

   886 subclass ordered_cancel_comm_semiring

   887 proof

   888   fix a b c :: 'a

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

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

   891     unfolding le_less

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

   893 qed

   894

   895 end

   896

   897 class ordered_ring = ring + ordered_cancel_semiring

   898 begin

   899

   900 subclass ordered_ab_group_add ..

   901

   902 lemma less_add_iff1:

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

   904 by (simp add: algebra_simps)

   905

   906 lemma less_add_iff2:

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

   908 by (simp add: algebra_simps)

   909

   910 lemma le_add_iff1:

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

   912 by (simp add: algebra_simps)

   913

   914 lemma le_add_iff2:

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

   916 by (simp add: algebra_simps)

   917

   918 lemma mult_left_mono_neg:

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

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

   921   apply simp_all

   922   done

   923

   924 lemma mult_right_mono_neg:

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

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

   927   apply simp_all

   928   done

   929

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

   931 using mult_right_mono_neg [of a 0 b] by simp

   932

   933 lemma split_mult_pos_le:

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

   935 by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)

   936

   937 end

   938

   939 class linordered_ring = ring + linordered_semiring + linordered_ab_group_add + abs_if

   940 begin

   941

   942 subclass ordered_ring ..

   943

   944 subclass ordered_ab_group_add_abs

   945 proof

   946   fix a b

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

   948     by (auto simp add: abs_if not_less)

   949     (auto simp del: minus_add_distrib simp add: minus_add_distrib [symmetric],

   950      auto intro!: less_imp_le add_neg_neg)

   951 qed (auto simp add: abs_if)

   952

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

   954   using linear [of 0 a]

   955   by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)

   956

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

   958   by (simp add: not_less)

   959

   960 end

   961

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

   963    Basically, linordered_ring + no_zero_divisors = linordered_ring_strict.

   964  *)

   965 class linordered_ring_strict = ring + linordered_semiring_strict

   966   + ordered_ab_group_add + abs_if

   967 begin

   968

   969 subclass linordered_ring ..

   970

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

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

   973

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

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

   976

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

   978 using mult_strict_right_mono_neg [of a 0 b] by simp

   979

   980 subclass ring_no_zero_divisors

   981 proof

   982   fix a b

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

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

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

   986   proof (cases "a < 0")

   987     case True note A' = this

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

   989       case True with A'

   990       show ?thesis by (auto dest: mult_neg_neg)

   991     next

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

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

   994     qed

   995   next

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

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

   998       case True with A'

   999       show ?thesis by (auto dest: mult_strict_right_mono_neg)

  1000     next

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

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

  1003     qed

  1004   qed

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

  1006 qed

  1007

  1008 lemma zero_less_mult_iff:

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

  1010   apply (auto simp add: mult_pos_pos mult_neg_neg)

  1011   apply (simp_all add: not_less le_less)

  1012   apply (erule disjE) apply assumption defer

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

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

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

  1016   apply (drule sym) apply simp

  1017   apply (blast dest: zero_less_mult_pos)

  1018   apply (blast dest: zero_less_mult_pos2)

  1019   done

  1020

  1021 lemma zero_le_mult_iff:

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

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

  1024

  1025 lemma mult_less_0_iff:

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

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

  1028   apply force

  1029   done

  1030

  1031 lemma mult_le_0_iff:

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

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

  1034   apply force

  1035   done

  1036

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

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

  1039

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

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

  1042

  1043 lemma mult_less_cancel_right_disj:

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

  1045   apply (cases "c = 0")

  1046   apply (auto simp add: neq_iff mult_strict_right_mono

  1047                       mult_strict_right_mono_neg)

  1048   apply (auto simp add: not_less

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

  1050                       not_le [symmetric, of a])

  1051   apply (erule_tac [!] notE)

  1052   apply (auto simp add: less_imp_le mult_right_mono

  1053                       mult_right_mono_neg)

  1054   done

  1055

  1056 lemma mult_less_cancel_left_disj:

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

  1058   apply (cases "c = 0")

  1059   apply (auto simp add: neq_iff mult_strict_left_mono

  1060                       mult_strict_left_mono_neg)

  1061   apply (auto simp add: not_less

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

  1063                       not_le [symmetric, of a])

  1064   apply (erule_tac [!] notE)

  1065   apply (auto simp add: less_imp_le mult_left_mono

  1066                       mult_left_mono_neg)

  1067   done

  1068

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

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

  1071

  1072 lemma mult_less_cancel_right:

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

  1074   using mult_less_cancel_right_disj [of a c b] by auto

  1075

  1076 lemma mult_less_cancel_left:

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

  1078   using mult_less_cancel_left_disj [of c a b] by auto

  1079

  1080 lemma mult_le_cancel_right:

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

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

  1083

  1084 lemma mult_le_cancel_left:

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

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

  1087

  1088 lemma mult_le_cancel_left_pos:

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

  1090 by (auto simp: mult_le_cancel_left)

  1091

  1092 lemma mult_le_cancel_left_neg:

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

  1094 by (auto simp: mult_le_cancel_left)

  1095

  1096 lemma mult_less_cancel_left_pos:

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

  1098 by (auto simp: mult_less_cancel_left)

  1099

  1100 lemma mult_less_cancel_left_neg:

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

  1102 by (auto simp: mult_less_cancel_left)

  1103

  1104 end

  1105

  1106 lemmas mult_sign_intros =

  1107   mult_nonneg_nonneg mult_nonneg_nonpos

  1108   mult_nonpos_nonneg mult_nonpos_nonpos

  1109   mult_pos_pos mult_pos_neg

  1110   mult_neg_pos mult_neg_neg

  1111

  1112 class ordered_comm_ring = comm_ring + ordered_comm_semiring

  1113 begin

  1114

  1115 subclass ordered_ring ..

  1116 subclass ordered_cancel_comm_semiring ..

  1117

  1118 end

  1119

  1120 class linordered_semidom = comm_semiring_1_cancel + linordered_comm_semiring_strict +

  1121   (*previously linordered_semiring*)

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

  1123 begin

  1124

  1125 lemma pos_add_strict:

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

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

  1128

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

  1130 by (rule zero_less_one [THEN less_imp_le])

  1131

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

  1133 by (simp add: not_le)

  1134

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

  1136 by (simp add: not_less)

  1137

  1138 lemma less_1_mult:

  1139   assumes "1 < m" and "1 < n"

  1140   shows "1 < m * n"

  1141   using assms mult_strict_mono [of 1 m 1 n]

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

  1143

  1144 end

  1145

  1146 class linordered_idom = comm_ring_1 +

  1147   linordered_comm_semiring_strict + ordered_ab_group_add +

  1148   abs_if + sgn_if

  1149   (*previously linordered_ring*)

  1150 begin

  1151

  1152 subclass linordered_semiring_1_strict ..

  1153 subclass linordered_ring_strict ..

  1154 subclass ordered_comm_ring ..

  1155 subclass idom ..

  1156

  1157 subclass linordered_semidom

  1158 proof

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

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

  1161 qed

  1162

  1163 lemma linorder_neqE_linordered_idom:

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

  1165   using assms by (rule neqE)

  1166

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

  1168

  1169 lemma mult_le_cancel_right1:

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

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

  1172

  1173 lemma mult_le_cancel_right2:

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

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

  1176

  1177 lemma mult_le_cancel_left1:

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

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

  1180

  1181 lemma mult_le_cancel_left2:

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

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

  1184

  1185 lemma mult_less_cancel_right1:

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

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

  1188

  1189 lemma mult_less_cancel_right2:

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

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

  1192

  1193 lemma mult_less_cancel_left1:

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

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

  1196

  1197 lemma mult_less_cancel_left2:

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

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

  1200

  1201 lemma sgn_sgn [simp]:

  1202   "sgn (sgn a) = sgn a"

  1203 unfolding sgn_if by simp

  1204

  1205 lemma sgn_0_0:

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

  1207 unfolding sgn_if by simp

  1208

  1209 lemma sgn_1_pos:

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

  1211 unfolding sgn_if by simp

  1212

  1213 lemma sgn_1_neg:

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

  1215 unfolding sgn_if by auto

  1216

  1217 lemma sgn_pos [simp]:

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

  1219 unfolding sgn_1_pos .

  1220

  1221 lemma sgn_neg [simp]:

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

  1223 unfolding sgn_1_neg .

  1224

  1225 lemma sgn_times:

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

  1227 by (auto simp add: sgn_if zero_less_mult_iff)

  1228

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

  1230 unfolding sgn_if abs_if by auto

  1231

  1232 lemma sgn_greater [simp]:

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

  1234   unfolding sgn_if by auto

  1235

  1236 lemma sgn_less [simp]:

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

  1238   unfolding sgn_if by auto

  1239

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

  1241   by (simp add: abs_if)

  1242

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

  1244   by (simp add: abs_if)

  1245

  1246 lemma dvd_if_abs_eq:

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

  1248 by(subst abs_dvd_iff[symmetric]) simp

  1249

  1250 end

  1251

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

  1253

  1254 lemmas mult_compare_simps[no_atp] =

  1255     mult_le_cancel_right mult_le_cancel_left

  1256     mult_le_cancel_right1 mult_le_cancel_right2

  1257     mult_le_cancel_left1 mult_le_cancel_left2

  1258     mult_less_cancel_right mult_less_cancel_left

  1259     mult_less_cancel_right1 mult_less_cancel_right2

  1260     mult_less_cancel_left1 mult_less_cancel_left2

  1261     mult_cancel_right mult_cancel_left

  1262     mult_cancel_right1 mult_cancel_right2

  1263     mult_cancel_left1 mult_cancel_left2

  1264

  1265 text {* Reasoning about inequalities with division *}

  1266

  1267 context linordered_semidom

  1268 begin

  1269

  1270 lemma less_add_one: "a < a + 1"

  1271 proof -

  1272   have "a + 0 < a + 1"

  1273     by (blast intro: zero_less_one add_strict_left_mono)

  1274   thus ?thesis by simp

  1275 qed

  1276

  1277 lemma zero_less_two: "0 < 1 + 1"

  1278 by (blast intro: less_trans zero_less_one less_add_one)

  1279

  1280 end

  1281

  1282 context linordered_idom

  1283 begin

  1284

  1285 lemma mult_right_le_one_le:

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

  1287   by (auto simp add: mult_le_cancel_left2)

  1288

  1289 lemma mult_left_le_one_le:

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

  1291   by (auto simp add: mult_le_cancel_right2)

  1292

  1293 end

  1294

  1295 text {* Absolute Value *}

  1296

  1297 context linordered_idom

  1298 begin

  1299

  1300 lemma mult_sgn_abs:

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

  1302   unfolding abs_if sgn_if by auto

  1303

  1304 lemma abs_one [simp]:

  1305   "\<bar>1\<bar> = 1"

  1306   by (simp add: abs_if zero_less_one [THEN less_not_sym])

  1307

  1308 end

  1309

  1310 class ordered_ring_abs = ordered_ring + ordered_ab_group_add_abs +

  1311   assumes abs_eq_mult:

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

  1313

  1314 context linordered_idom

  1315 begin

  1316

  1317 subclass ordered_ring_abs proof

  1318 qed (auto simp add: abs_if not_less mult_less_0_iff)

  1319

  1320 lemma abs_mult:

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

  1322   by (rule abs_eq_mult) auto

  1323

  1324 lemma abs_mult_self:

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

  1326   by (simp add: abs_if)

  1327

  1328 lemma abs_mult_less:

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

  1330 proof -

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

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

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

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

  1335 qed

  1336

  1337 lemma less_minus_self_iff:

  1338   "a < - a \<longleftrightarrow> a < 0"

  1339   by (simp only: less_le less_eq_neg_nonpos equal_neg_zero)

  1340

  1341 lemma abs_less_iff:

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

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

  1344

  1345 lemma abs_mult_pos:

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

  1347   by (simp add: abs_mult)

  1348

  1349 end

  1350

  1351 code_modulename SML

  1352   Rings Arith

  1353

  1354 code_modulename OCaml

  1355   Rings Arith

  1356

  1357 code_modulename Haskell

  1358   Rings Arith

  1359

  1360 end