src/HOL/Rings.thy
 author haftmann Wed Jul 08 14:01:41 2015 +0200 (2015-07-08) changeset 60688 01488b559910 parent 60685 cb21b7022b00 child 60690 a9e45c9588c3 permissions -rw-r--r--
avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
     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 section {* 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]: "(a + b) * c = a * c + b * c"

    18   assumes distrib_left[algebra_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 ac_simps)

    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 begin

    32

    33 lemma mult_not_zero:

    34   "a * b \<noteq> 0 \<Longrightarrow> a \<noteq> 0 \<and> b \<noteq> 0"

    35   by auto

    36

    37 end

    38

    39 class semiring_0 = semiring + comm_monoid_add + mult_zero

    40

    41 class semiring_0_cancel = semiring + cancel_comm_monoid_add

    42 begin

    43

    44 subclass semiring_0

    45 proof

    46   fix a :: 'a

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

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

    49 next

    50   fix a :: 'a

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

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

    53 qed

    54

    55 end

    56

    57 class comm_semiring = ab_semigroup_add + ab_semigroup_mult +

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

    59 begin

    60

    61 subclass semiring

    62 proof

    63   fix a b c :: 'a

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

    65   have "a * (b + c) = (b + c) * a" by (simp add: ac_simps)

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

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

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

    69 qed

    70

    71 end

    72

    73 class comm_semiring_0 = comm_semiring + comm_monoid_add + mult_zero

    74 begin

    75

    76 subclass semiring_0 ..

    77

    78 end

    79

    80 class comm_semiring_0_cancel = comm_semiring + cancel_comm_monoid_add

    81 begin

    82

    83 subclass semiring_0_cancel ..

    84

    85 subclass comm_semiring_0 ..

    86

    87 end

    88

    89 class zero_neq_one = zero + one +

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

    91 begin

    92

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

    94 by (rule not_sym) (rule zero_neq_one)

    95

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

    97 where

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

    99

   100 lemma of_bool_eq [simp, code]:

   101   "of_bool False = 0"

   102   "of_bool True = 1"

   103   by (simp_all add: of_bool_def)

   104

   105 lemma of_bool_eq_iff:

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

   107   by (simp add: of_bool_def)

   108

   109 lemma split_of_bool [split]:

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

   111   by (cases p) simp_all

   112

   113 lemma split_of_bool_asm:

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

   115   by (cases p) simp_all

   116

   117 end

   118

   119 class semiring_1 = zero_neq_one + semiring_0 + monoid_mult

   120

   121 text {* Abstract divisibility *}

   122

   123 class dvd = times

   124 begin

   125

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

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

   128

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

   130   unfolding dvd_def ..

   131

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

   133   unfolding dvd_def by blast

   134

   135 end

   136

   137 context comm_monoid_mult

   138 begin

   139

   140 subclass dvd .

   141

   142 lemma dvd_refl [simp]:

   143   "a dvd a"

   144 proof

   145   show "a = a * 1" by simp

   146 qed

   147

   148 lemma dvd_trans:

   149   assumes "a dvd b" and "b dvd c"

   150   shows "a dvd c"

   151 proof -

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

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

   154   ultimately have "c = a * (v * w)" by (simp add: mult.assoc)

   155   then show ?thesis ..

   156 qed

   157

   158 lemma one_dvd [simp]:

   159   "1 dvd a"

   160   by (auto intro!: dvdI)

   161

   162 lemma dvd_mult [simp]:

   163   "a dvd c \<Longrightarrow> a dvd (b * c)"

   164   by (auto intro!: mult.left_commute dvdI elim!: dvdE)

   165

   166 lemma dvd_mult2 [simp]:

   167   "a dvd b \<Longrightarrow> a dvd (b * c)"

   168   using dvd_mult [of a b c] by (simp add: ac_simps)

   169

   170 lemma dvd_triv_right [simp]:

   171   "a dvd b * a"

   172   by (rule dvd_mult) (rule dvd_refl)

   173

   174 lemma dvd_triv_left [simp]:

   175   "a dvd a * b"

   176   by (rule dvd_mult2) (rule dvd_refl)

   177

   178 lemma mult_dvd_mono:

   179   assumes "a dvd b"

   180     and "c dvd d"

   181   shows "a * c dvd b * d"

   182 proof -

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

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

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

   186   then show ?thesis ..

   187 qed

   188

   189 lemma dvd_mult_left:

   190   "a * b dvd c \<Longrightarrow> a dvd c"

   191   by (simp add: dvd_def mult.assoc) blast

   192

   193 lemma dvd_mult_right:

   194   "a * b dvd c \<Longrightarrow> b dvd c"

   195   using dvd_mult_left [of b a c] by (simp add: ac_simps)

   196

   197 end

   198

   199 class comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult

   200 begin

   201

   202 subclass semiring_1 ..

   203

   204 lemma dvd_0_left_iff [simp]:

   205   "0 dvd a \<longleftrightarrow> a = 0"

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

   207

   208 lemma dvd_0_right [iff]:

   209   "a dvd 0"

   210 proof

   211   show "0 = a * 0" by simp

   212 qed

   213

   214 lemma dvd_0_left:

   215   "0 dvd a \<Longrightarrow> a = 0"

   216   by simp

   217

   218 lemma dvd_add [simp]:

   219   assumes "a dvd b" and "a dvd c"

   220   shows "a dvd (b + c)"

   221 proof -

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

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

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

   225   then show ?thesis ..

   226 qed

   227

   228 end

   229

   230 class semiring_1_cancel = semiring + cancel_comm_monoid_add

   231   + zero_neq_one + monoid_mult

   232 begin

   233

   234 subclass semiring_0_cancel ..

   235

   236 subclass semiring_1 ..

   237

   238 end

   239

   240 class comm_semiring_1_cancel = comm_semiring + cancel_comm_monoid_add +

   241                                zero_neq_one + comm_monoid_mult +

   242   assumes right_diff_distrib' [algebra_simps]: "a * (b - c) = a * b - a * c"

   243 begin

   244

   245 subclass semiring_1_cancel ..

   246 subclass comm_semiring_0_cancel ..

   247 subclass comm_semiring_1 ..

   248

   249 lemma left_diff_distrib' [algebra_simps]:

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

   251   by (simp add: algebra_simps)

   252

   253 lemma dvd_add_times_triv_left_iff [simp]:

   254   "a dvd c * a + b \<longleftrightarrow> a dvd b"

   255 proof -

   256   have "a dvd a * c + b \<longleftrightarrow> a dvd b" (is "?P \<longleftrightarrow> ?Q")

   257   proof

   258     assume ?Q then show ?P by simp

   259   next

   260     assume ?P

   261     then obtain d where "a * c + b = a * d" ..

   262     then have "a * c + b - a * c = a * d - a * c" by simp

   263     then have "b = a * d - a * c" by simp

   264     then have "b = a * (d - c)" by (simp add: algebra_simps)

   265     then show ?Q ..

   266   qed

   267   then show "a dvd c * a + b \<longleftrightarrow> a dvd b" by (simp add: ac_simps)

   268 qed

   269

   270 lemma dvd_add_times_triv_right_iff [simp]:

   271   "a dvd b + c * a \<longleftrightarrow> a dvd b"

   272   using dvd_add_times_triv_left_iff [of a c b] by (simp add: ac_simps)

   273

   274 lemma dvd_add_triv_left_iff [simp]:

   275   "a dvd a + b \<longleftrightarrow> a dvd b"

   276   using dvd_add_times_triv_left_iff [of a 1 b] by simp

   277

   278 lemma dvd_add_triv_right_iff [simp]:

   279   "a dvd b + a \<longleftrightarrow> a dvd b"

   280   using dvd_add_times_triv_right_iff [of a b 1] by simp

   281

   282 lemma dvd_add_right_iff:

   283   assumes "a dvd b"

   284   shows "a dvd b + c \<longleftrightarrow> a dvd c" (is "?P \<longleftrightarrow> ?Q")

   285 proof

   286   assume ?P then obtain d where "b + c = a * d" ..

   287   moreover from a dvd b obtain e where "b = a * e" ..

   288   ultimately have "a * e + c = a * d" by simp

   289   then have "a * e + c - a * e = a * d - a * e" by simp

   290   then have "c = a * d - a * e" by simp

   291   then have "c = a * (d - e)" by (simp add: algebra_simps)

   292   then show ?Q ..

   293 next

   294   assume ?Q with assms show ?P by simp

   295 qed

   296

   297 lemma dvd_add_left_iff:

   298   assumes "a dvd c"

   299   shows "a dvd b + c \<longleftrightarrow> a dvd b"

   300   using assms dvd_add_right_iff [of a c b] by (simp add: ac_simps)

   301

   302 end

   303

   304 class ring = semiring + ab_group_add

   305 begin

   306

   307 subclass semiring_0_cancel ..

   308

   309 text {* Distribution rules *}

   310

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

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

   313

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

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

   316

   317 text{*Extract signs from products*}

   318 lemmas mult_minus_left [simp] = minus_mult_left [symmetric]

   319 lemmas mult_minus_right [simp] = minus_mult_right [symmetric]

   320

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

   322 by simp

   323

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

   325 by simp

   326

   327 lemma right_diff_distrib [algebra_simps]:

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

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

   330

   331 lemma left_diff_distrib [algebra_simps]:

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

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

   334

   335 lemmas ring_distribs =

   336   distrib_left distrib_right left_diff_distrib right_diff_distrib

   337

   338 lemma eq_add_iff1:

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

   340 by (simp add: algebra_simps)

   341

   342 lemma eq_add_iff2:

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

   344 by (simp add: algebra_simps)

   345

   346 end

   347

   348 lemmas ring_distribs =

   349   distrib_left distrib_right left_diff_distrib right_diff_distrib

   350

   351 class comm_ring = comm_semiring + ab_group_add

   352 begin

   353

   354 subclass ring ..

   355 subclass comm_semiring_0_cancel ..

   356

   357 lemma square_diff_square_factored:

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

   359   by (simp add: algebra_simps)

   360

   361 end

   362

   363 class ring_1 = ring + zero_neq_one + monoid_mult

   364 begin

   365

   366 subclass semiring_1_cancel ..

   367

   368 lemma square_diff_one_factored:

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

   370   by (simp add: algebra_simps)

   371

   372 end

   373

   374 class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult

   375 begin

   376

   377 subclass ring_1 ..

   378 subclass comm_semiring_1_cancel

   379   by unfold_locales (simp add: algebra_simps)

   380

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

   382 proof

   383   assume "x dvd - y"

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

   385   then show "x dvd y" by simp

   386 next

   387   assume "x dvd y"

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

   389   then show "x dvd - y" by simp

   390 qed

   391

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

   393 proof

   394   assume "- x dvd y"

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

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

   397   then show "x dvd y" ..

   398 next

   399   assume "x dvd y"

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

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

   402   then show "- x dvd y" ..

   403 qed

   404

   405 lemma dvd_diff [simp]:

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

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

   408

   409 end

   410

   411 class semiring_no_zero_divisors = semiring_0 +

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

   413 begin

   414

   415 lemma divisors_zero:

   416   assumes "a * b = 0"

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

   418 proof (rule classical)

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

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

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

   422   with assms show ?thesis by simp

   423 qed

   424

   425 lemma mult_eq_0_iff [simp]:

   426   shows "a * b = 0 \<longleftrightarrow> a = 0 \<or> b = 0"

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

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

   429     then show ?thesis using no_zero_divisors by simp

   430 next

   431   case True then show ?thesis by auto

   432 qed

   433

   434 end

   435

   436 class semiring_no_zero_divisors_cancel = semiring_no_zero_divisors +

   437   assumes mult_cancel_right [simp]: "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b"

   438     and mult_cancel_left [simp]: "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b"

   439 begin

   440

   441 lemma mult_left_cancel:

   442   "c \<noteq> 0 \<Longrightarrow> c * a = c * b \<longleftrightarrow> a = b"

   443   by simp

   444

   445 lemma mult_right_cancel:

   446   "c \<noteq> 0 \<Longrightarrow> a * c = b * c \<longleftrightarrow> a = b"

   447   by simp

   448

   449 end

   450

   451 class ring_no_zero_divisors = ring + semiring_no_zero_divisors

   452 begin

   453

   454 subclass semiring_no_zero_divisors_cancel

   455 proof

   456   fix a b c

   457   have "a * c = b * c \<longleftrightarrow> (a - b) * c = 0"

   458     by (simp add: algebra_simps)

   459   also have "\<dots> \<longleftrightarrow> c = 0 \<or> a = b"

   460     by auto

   461   finally show "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b" .

   462   have "c * a = c * b \<longleftrightarrow> c * (a - b) = 0"

   463     by (simp add: algebra_simps)

   464   also have "\<dots> \<longleftrightarrow> c = 0 \<or> a = b"

   465     by auto

   466   finally show "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b" .

   467 qed

   468

   469 end

   470

   471 class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors

   472 begin

   473

   474 lemma square_eq_1_iff:

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

   476 proof -

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

   478     by (simp add: algebra_simps)

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

   480     by simp

   481   thus ?thesis

   482     by (simp add: eq_neg_iff_add_eq_0)

   483 qed

   484

   485 lemma mult_cancel_right1 [simp]:

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

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

   488

   489 lemma mult_cancel_right2 [simp]:

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

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

   492

   493 lemma mult_cancel_left1 [simp]:

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

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

   496

   497 lemma mult_cancel_left2 [simp]:

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

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

   500

   501 end

   502

   503 class semidom = comm_semiring_1_cancel + semiring_no_zero_divisors

   504

   505 class idom = comm_ring_1 + semiring_no_zero_divisors

   506 begin

   507

   508 subclass semidom ..

   509

   510 subclass ring_1_no_zero_divisors ..

   511

   512 lemma dvd_mult_cancel_right [simp]:

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

   514 proof -

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

   516     unfolding dvd_def by (simp add: ac_simps)

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

   518     unfolding dvd_def by simp

   519   finally show ?thesis .

   520 qed

   521

   522 lemma dvd_mult_cancel_left [simp]:

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

   524 proof -

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

   526     unfolding dvd_def by (simp add: ac_simps)

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

   528     unfolding dvd_def by simp

   529   finally show ?thesis .

   530 qed

   531

   532 lemma square_eq_iff: "a * a = b * b \<longleftrightarrow> a = b \<or> a = - b"

   533 proof

   534   assume "a * a = b * b"

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

   536     by (simp add: algebra_simps)

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

   538     by (simp add: eq_neg_iff_add_eq_0)

   539 next

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

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

   542 qed

   543

   544 end

   545

   546 text {*

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

   548   \begin{itemize}

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

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

   551   \end{itemize}

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

   553   \begin{itemize}

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

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

   556   \end{itemize}

   557 *}

   558

   559 class divide =

   560   fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "div" 70)

   561

   562 setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a \<Rightarrow> 'a \<Rightarrow> 'a"}) *}

   563

   564 context semiring

   565 begin

   566

   567 lemma [field_simps]:

   568   shows distrib_left_NO_MATCH: "NO_MATCH (x div y) a \<Longrightarrow> a * (b + c) = a * b + a * c"

   569     and distrib_right_NO_MATCH: "NO_MATCH (x div y) c \<Longrightarrow> (a + b) * c = a * c + b * c"

   570   by (rule distrib_left distrib_right)+

   571

   572 end

   573

   574 context ring

   575 begin

   576

   577 lemma [field_simps]:

   578   shows left_diff_distrib_NO_MATCH: "NO_MATCH (x div y) c \<Longrightarrow> (a - b) * c = a * c - b * c"

   579     and right_diff_distrib_NO_MATCH: "NO_MATCH (x div y) a \<Longrightarrow> a * (b - c) = a * b - a * c"

   580   by (rule left_diff_distrib right_diff_distrib)+

   581

   582 end

   583

   584 setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a::divide \<Rightarrow> 'a \<Rightarrow> 'a"}) *}

   585

   586 class semidom_divide = semidom + divide +

   587   assumes nonzero_mult_divide_cancel_right [simp]: "b \<noteq> 0 \<Longrightarrow> (a * b) div b = a"

   588   assumes divide_zero [simp]: "a div 0 = 0"

   589 begin

   590

   591 lemma nonzero_mult_divide_cancel_left [simp]:

   592   "a \<noteq> 0 \<Longrightarrow> (a * b) div a = b"

   593   using nonzero_mult_divide_cancel_right [of a b] by (simp add: ac_simps)

   594

   595 subclass semiring_no_zero_divisors_cancel

   596 proof

   597   fix a b c

   598   { fix a b c

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

   600     proof (cases "c = 0")

   601       case True then show ?thesis by simp

   602     next

   603       case False

   604       { assume "a * c = b * c"

   605         then have "a * c div c = b * c div c"

   606           by simp

   607         with False have "a = b"

   608           by simp

   609       } then show ?thesis by auto

   610     qed

   611   }

   612   from this [of a c b]

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

   614     by (simp add: ac_simps)

   615 qed

   616

   617 lemma div_self [simp]:

   618   assumes "a \<noteq> 0"

   619   shows "a div a = 1"

   620   using assms nonzero_mult_divide_cancel_left [of a 1] by simp

   621

   622 lemma divide_zero_left [simp]:

   623   "0 div a = 0"

   624 proof (cases "a = 0")

   625   case True then show ?thesis by simp

   626 next

   627   case False then have "a * 0 div a = 0"

   628     by (rule nonzero_mult_divide_cancel_left)

   629   then show ?thesis by simp

   630 qed

   631

   632 end

   633

   634 class idom_divide = idom + semidom_divide

   635

   636 class algebraic_semidom = semidom_divide

   637 begin

   638

   639 text \<open>

   640   Class @{class algebraic_semidom} enriches a integral domain

   641   by notions from algebra, like units in a ring.

   642   It is a separate class to avoid spoiling fields with notions

   643   which are degenerated there.

   644 \<close>

   645

   646 lemma dvd_div_mult_self [simp]:

   647   "a dvd b \<Longrightarrow> b div a * a = b"

   648   by (cases "a = 0") (auto elim: dvdE simp add: ac_simps)

   649

   650 lemma dvd_mult_div_cancel [simp]:

   651   "a dvd b \<Longrightarrow> a * (b div a) = b"

   652   using dvd_div_mult_self [of a b] by (simp add: ac_simps)

   653

   654 lemma div_mult_swap:

   655   assumes "c dvd b"

   656   shows "a * (b div c) = (a * b) div c"

   657 proof (cases "c = 0")

   658   case True then show ?thesis by simp

   659 next

   660   case False from assms obtain d where "b = c * d" ..

   661   moreover from False have "a * divide (d * c) c = ((a * d) * c) div c"

   662     by simp

   663   ultimately show ?thesis by (simp add: ac_simps)

   664 qed

   665

   666 lemma dvd_div_mult:

   667   assumes "c dvd b"

   668   shows "b div c * a = (b * a) div c"

   669   using assms div_mult_swap [of c b a] by (simp add: ac_simps)

   670

   671 lemma dvd_div_mult2_eq:

   672   assumes "b * c dvd a"

   673   shows "a div (b * c) = a div b div c"

   674 using assms proof

   675   fix k

   676   assume "a = b * c * k"

   677   then show ?thesis

   678     by (cases "b = 0 \<or> c = 0") (auto, simp add: ac_simps)

   679 qed

   680

   681

   682 text \<open>Units: invertible elements in a ring\<close>

   683

   684 abbreviation is_unit :: "'a \<Rightarrow> bool"

   685 where

   686   "is_unit a \<equiv> a dvd 1"

   687

   688 lemma not_is_unit_0 [simp]:

   689   "\<not> is_unit 0"

   690   by simp

   691

   692 lemma unit_imp_dvd [dest]:

   693   "is_unit b \<Longrightarrow> b dvd a"

   694   by (rule dvd_trans [of _ 1]) simp_all

   695

   696 lemma unit_dvdE:

   697   assumes "is_unit a"

   698   obtains c where "a \<noteq> 0" and "b = a * c"

   699 proof -

   700   from assms have "a dvd b" by auto

   701   then obtain c where "b = a * c" ..

   702   moreover from assms have "a \<noteq> 0" by auto

   703   ultimately show thesis using that by blast

   704 qed

   705

   706 lemma dvd_unit_imp_unit:

   707   "a dvd b \<Longrightarrow> is_unit b \<Longrightarrow> is_unit a"

   708   by (rule dvd_trans)

   709

   710 lemma unit_div_1_unit [simp, intro]:

   711   assumes "is_unit a"

   712   shows "is_unit (1 div a)"

   713 proof -

   714   from assms have "1 = 1 div a * a" by simp

   715   then show "is_unit (1 div a)" by (rule dvdI)

   716 qed

   717

   718 lemma is_unitE [elim?]:

   719   assumes "is_unit a"

   720   obtains b where "a \<noteq> 0" and "b \<noteq> 0"

   721     and "is_unit b" and "1 div a = b" and "1 div b = a"

   722     and "a * b = 1" and "c div a = c * b"

   723 proof (rule that)

   724   def b \<equiv> "1 div a"

   725   then show "1 div a = b" by simp

   726   from b_def is_unit a show "is_unit b" by simp

   727   from is_unit a and is_unit b show "a \<noteq> 0" and "b \<noteq> 0" by auto

   728   from b_def is_unit a show "a * b = 1" by simp

   729   then have "1 = a * b" ..

   730   with b_def b \<noteq> 0 show "1 div b = a" by simp

   731   from is_unit a have "a dvd c" ..

   732   then obtain d where "c = a * d" ..

   733   with a \<noteq> 0 a * b = 1 show "c div a = c * b"

   734     by (simp add: mult.assoc mult.left_commute [of a])

   735 qed

   736

   737 lemma unit_prod [intro]:

   738   "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a * b)"

   739   by (subst mult_1_left [of 1, symmetric]) (rule mult_dvd_mono)

   740

   741 lemma unit_div [intro]:

   742   "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a div b)"

   743   by (erule is_unitE [of b a]) (simp add: ac_simps unit_prod)

   744

   745 lemma mult_unit_dvd_iff:

   746   assumes "is_unit b"

   747   shows "a * b dvd c \<longleftrightarrow> a dvd c"

   748 proof

   749   assume "a * b dvd c"

   750   with assms show "a dvd c"

   751     by (simp add: dvd_mult_left)

   752 next

   753   assume "a dvd c"

   754   then obtain k where "c = a * k" ..

   755   with assms have "c = (a * b) * (1 div b * k)"

   756     by (simp add: mult_ac)

   757   then show "a * b dvd c" by (rule dvdI)

   758 qed

   759

   760 lemma dvd_mult_unit_iff:

   761   assumes "is_unit b"

   762   shows "a dvd c * b \<longleftrightarrow> a dvd c"

   763 proof

   764   assume "a dvd c * b"

   765   with assms have "c * b dvd c * (b * (1 div b))"

   766     by (subst mult_assoc [symmetric]) simp

   767   also from is_unit b have "b * (1 div b) = 1" by (rule is_unitE) simp

   768   finally have "c * b dvd c" by simp

   769   with a dvd c * b show "a dvd c" by (rule dvd_trans)

   770 next

   771   assume "a dvd c"

   772   then show "a dvd c * b" by simp

   773 qed

   774

   775 lemma div_unit_dvd_iff:

   776   "is_unit b \<Longrightarrow> a div b dvd c \<longleftrightarrow> a dvd c"

   777   by (erule is_unitE [of _ a]) (auto simp add: mult_unit_dvd_iff)

   778

   779 lemma dvd_div_unit_iff:

   780   "is_unit b \<Longrightarrow> a dvd c div b \<longleftrightarrow> a dvd c"

   781   by (erule is_unitE [of _ c]) (simp add: dvd_mult_unit_iff)

   782

   783 lemmas unit_dvd_iff = mult_unit_dvd_iff div_unit_dvd_iff

   784   dvd_mult_unit_iff dvd_div_unit_iff -- \<open>FIXME consider fact collection\<close>

   785

   786 lemma unit_mult_div_div [simp]:

   787   "is_unit a \<Longrightarrow> b * (1 div a) = b div a"

   788   by (erule is_unitE [of _ b]) simp

   789

   790 lemma unit_div_mult_self [simp]:

   791   "is_unit a \<Longrightarrow> b div a * a = b"

   792   by (rule dvd_div_mult_self) auto

   793

   794 lemma unit_div_1_div_1 [simp]:

   795   "is_unit a \<Longrightarrow> 1 div (1 div a) = a"

   796   by (erule is_unitE) simp

   797

   798 lemma unit_div_mult_swap:

   799   "is_unit c \<Longrightarrow> a * (b div c) = (a * b) div c"

   800   by (erule unit_dvdE [of _ b]) (simp add: mult.left_commute [of _ c])

   801

   802 lemma unit_div_commute:

   803   "is_unit b \<Longrightarrow> (a div b) * c = (a * c) div b"

   804   using unit_div_mult_swap [of b c a] by (simp add: ac_simps)

   805

   806 lemma unit_eq_div1:

   807   "is_unit b \<Longrightarrow> a div b = c \<longleftrightarrow> a = c * b"

   808   by (auto elim: is_unitE)

   809

   810 lemma unit_eq_div2:

   811   "is_unit b \<Longrightarrow> a = c div b \<longleftrightarrow> a * b = c"

   812   using unit_eq_div1 [of b c a] by auto

   813

   814 lemma unit_mult_left_cancel:

   815   assumes "is_unit a"

   816   shows "a * b = a * c \<longleftrightarrow> b = c" (is "?P \<longleftrightarrow> ?Q")

   817   using assms mult_cancel_left [of a b c] by auto

   818

   819 lemma unit_mult_right_cancel:

   820   "is_unit a \<Longrightarrow> b * a = c * a \<longleftrightarrow> b = c"

   821   using unit_mult_left_cancel [of a b c] by (auto simp add: ac_simps)

   822

   823 lemma unit_div_cancel:

   824   assumes "is_unit a"

   825   shows "b div a = c div a \<longleftrightarrow> b = c"

   826 proof -

   827   from assms have "is_unit (1 div a)" by simp

   828   then have "b * (1 div a) = c * (1 div a) \<longleftrightarrow> b = c"

   829     by (rule unit_mult_right_cancel)

   830   with assms show ?thesis by simp

   831 qed

   832

   833 lemma is_unit_div_mult2_eq:

   834   assumes "is_unit b" and "is_unit c"

   835   shows "a div (b * c) = a div b div c"

   836 proof -

   837   from assms have "is_unit (b * c)" by (simp add: unit_prod)

   838   then have "b * c dvd a"

   839     by (rule unit_imp_dvd)

   840   then show ?thesis

   841     by (rule dvd_div_mult2_eq)

   842 qed

   843

   844 lemmas unit_simps = mult_unit_dvd_iff div_unit_dvd_iff dvd_mult_unit_iff

   845   dvd_div_unit_iff unit_div_mult_swap unit_div_commute

   846   unit_mult_left_cancel unit_mult_right_cancel unit_div_cancel

   847   unit_eq_div1 unit_eq_div2

   848

   849 lemma is_unit_divide_mult_cancel_left:

   850   assumes "a \<noteq> 0" and "is_unit b"

   851   shows "a div (a * b) = 1 div b"

   852 proof -

   853   from assms have "a div (a * b) = a div a div b"

   854     by (simp add: mult_unit_dvd_iff dvd_div_mult2_eq)

   855   with assms show ?thesis by simp

   856 qed

   857

   858 lemma is_unit_divide_mult_cancel_right:

   859   assumes "a \<noteq> 0" and "is_unit b"

   860   shows "a div (b * a) = 1 div b"

   861   using assms is_unit_divide_mult_cancel_left [of a b] by (simp add: ac_simps)

   862

   863 end

   864

   865 class normalization_semidom = algebraic_semidom +

   866   fixes normalize :: "'a \<Rightarrow> 'a"

   867     and unit_factor :: "'a \<Rightarrow> 'a"

   868   assumes unit_factor_mult_normalize [simp]: "unit_factor a * normalize a = a"

   869   assumes normalize_0 [simp]: "normalize 0 = 0"

   870     and unit_factor_0 [simp]: "unit_factor 0 = 0"

   871   assumes is_unit_normalize:

   872     "is_unit a  \<Longrightarrow> normalize a = 1"

   873   assumes unit_factor_is_unit [iff]:

   874     "a \<noteq> 0 \<Longrightarrow> is_unit (unit_factor a)"

   875   assumes unit_factor_mult: "unit_factor (a * b) = unit_factor a * unit_factor b"

   876 begin

   877

   878 text \<open>

   879   Class @{class normalization_semidom} cultivates the idea that

   880   each integral domain can be split into equivalence classes

   881   whose representants are associated, i.e. divide each other.

   882   @{const normalize} specifies a canonical representant for each equivalence

   883   class.  The rationale behind this is that it is easier to reason about equality

   884   than equivalences, hence we prefer to think about equality of normalized

   885   values rather than associated elements.

   886 \<close>

   887

   888 lemma unit_factor_dvd [simp]:

   889   "a \<noteq> 0 \<Longrightarrow> unit_factor a dvd b"

   890   by (rule unit_imp_dvd) simp

   891

   892 lemma unit_factor_self [simp]:

   893   "unit_factor a dvd a"

   894   by (cases "a = 0") simp_all

   895

   896 lemma normalize_mult_unit_factor [simp]:

   897   "normalize a * unit_factor a = a"

   898   using unit_factor_mult_normalize [of a] by (simp add: ac_simps)

   899

   900 lemma normalize_eq_0_iff [simp]:

   901   "normalize a = 0 \<longleftrightarrow> a = 0" (is "?P \<longleftrightarrow> ?Q")

   902 proof

   903   assume ?P

   904   moreover have "unit_factor a * normalize a = a" by simp

   905   ultimately show ?Q by simp

   906 next

   907   assume ?Q then show ?P by simp

   908 qed

   909

   910 lemma unit_factor_eq_0_iff [simp]:

   911   "unit_factor a = 0 \<longleftrightarrow> a = 0" (is "?P \<longleftrightarrow> ?Q")

   912 proof

   913   assume ?P

   914   moreover have "unit_factor a * normalize a = a" by simp

   915   ultimately show ?Q by simp

   916 next

   917   assume ?Q then show ?P by simp

   918 qed

   919

   920 lemma is_unit_unit_factor:

   921   assumes "is_unit a" shows "unit_factor a = a"

   922 proof -

   923   from assms have "normalize a = 1" by (rule is_unit_normalize)

   924   moreover from unit_factor_mult_normalize have "unit_factor a * normalize a = a" .

   925   ultimately show ?thesis by simp

   926 qed

   927

   928 lemma unit_factor_1 [simp]:

   929   "unit_factor 1 = 1"

   930   by (rule is_unit_unit_factor) simp

   931

   932 lemma normalize_1 [simp]:

   933   "normalize 1 = 1"

   934   by (rule is_unit_normalize) simp

   935

   936 lemma normalize_1_iff:

   937   "normalize a = 1 \<longleftrightarrow> is_unit a" (is "?P \<longleftrightarrow> ?Q")

   938 proof

   939   assume ?Q then show ?P by (rule is_unit_normalize)

   940 next

   941   assume ?P

   942   then have "a \<noteq> 0" by auto

   943   from \<open>?P\<close> have "unit_factor a * normalize a = unit_factor a * 1"

   944     by simp

   945   then have "unit_factor a = a"

   946     by simp

   947   moreover have "is_unit (unit_factor a)"

   948     using \<open>a \<noteq> 0\<close> by simp

   949   ultimately show ?Q by simp

   950 qed

   951

   952 lemma div_normalize [simp]:

   953   "a div normalize a = unit_factor a"

   954 proof (cases "a = 0")

   955   case True then show ?thesis by simp

   956 next

   957   case False then have "normalize a \<noteq> 0" by simp

   958   with nonzero_mult_divide_cancel_right

   959   have "unit_factor a * normalize a div normalize a = unit_factor a" by blast

   960   then show ?thesis by simp

   961 qed

   962

   963 lemma div_unit_factor [simp]:

   964   "a div unit_factor a = normalize a"

   965 proof (cases "a = 0")

   966   case True then show ?thesis by simp

   967 next

   968   case False then have "unit_factor a \<noteq> 0" by simp

   969   with nonzero_mult_divide_cancel_left

   970   have "unit_factor a * normalize a div unit_factor a = normalize a" by blast

   971   then show ?thesis by simp

   972 qed

   973

   974 lemma normalize_div [simp]:

   975   "normalize a div a = 1 div unit_factor a"

   976 proof (cases "a = 0")

   977   case True then show ?thesis by simp

   978 next

   979   case False

   980   have "normalize a div a = normalize a div (unit_factor a * normalize a)"

   981     by simp

   982   also have "\<dots> = 1 div unit_factor a"

   983     using False by (subst is_unit_divide_mult_cancel_right) simp_all

   984   finally show ?thesis .

   985 qed

   986

   987 lemma mult_one_div_unit_factor [simp]:

   988   "a * (1 div unit_factor b) = a div unit_factor b"

   989   by (cases "b = 0") simp_all

   990

   991 lemma normalize_mult:

   992   "normalize (a * b) = normalize a * normalize b"

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

   994   case True then show ?thesis by auto

   995 next

   996   case False

   997   from unit_factor_mult_normalize have "unit_factor (a * b) * normalize (a * b) = a * b" .

   998   then have "normalize (a * b) = a * b div unit_factor (a * b)" by simp

   999   also have "\<dots> = a * b div unit_factor (b * a)" by (simp add: ac_simps)

  1000   also have "\<dots> = a * b div unit_factor b div unit_factor a"

  1001     using False by (simp add: unit_factor_mult is_unit_div_mult2_eq [symmetric])

  1002   also have "\<dots> = a * (b div unit_factor b) div unit_factor a"

  1003     using False by (subst unit_div_mult_swap) simp_all

  1004   also have "\<dots> = normalize a * normalize b"

  1005     using False by (simp add: mult.commute [of a] mult.commute [of "normalize a"] unit_div_mult_swap [symmetric])

  1006   finally show ?thesis .

  1007 qed

  1008

  1009 lemma unit_factor_idem [simp]:

  1010   "unit_factor (unit_factor a) = unit_factor a"

  1011   by (cases "a = 0") (auto intro: is_unit_unit_factor)

  1012

  1013 lemma normalize_unit_factor [simp]:

  1014   "a \<noteq> 0 \<Longrightarrow> normalize (unit_factor a) = 1"

  1015   by (rule is_unit_normalize) simp

  1016

  1017 lemma normalize_idem [simp]:

  1018   "normalize (normalize a) = normalize a"

  1019 proof (cases "a = 0")

  1020   case True then show ?thesis by simp

  1021 next

  1022   case False

  1023   have "normalize a = normalize (unit_factor a * normalize a)" by simp

  1024   also have "\<dots> = normalize (unit_factor a) * normalize (normalize a)"

  1025     by (simp only: normalize_mult)

  1026   finally show ?thesis using False by simp_all

  1027 qed

  1028

  1029 lemma unit_factor_normalize [simp]:

  1030   assumes "a \<noteq> 0"

  1031   shows "unit_factor (normalize a) = 1"

  1032 proof -

  1033   from assms have "normalize a \<noteq> 0" by simp

  1034   have "unit_factor (normalize a) * normalize (normalize a) = normalize a"

  1035     by (simp only: unit_factor_mult_normalize)

  1036   then have "unit_factor (normalize a) * normalize a = normalize a"

  1037     by simp

  1038   with \<open>normalize a \<noteq> 0\<close>

  1039   have "unit_factor (normalize a) * normalize a div normalize a = normalize a div normalize a"

  1040     by simp

  1041   with \<open>normalize a \<noteq> 0\<close>

  1042   show ?thesis by simp

  1043 qed

  1044

  1045 lemma dvd_unit_factor_div:

  1046   assumes "b dvd a"

  1047   shows "unit_factor (a div b) = unit_factor a div unit_factor b"

  1048 proof -

  1049   from assms have "a = a div b * b"

  1050     by simp

  1051   then have "unit_factor a = unit_factor (a div b * b)"

  1052     by simp

  1053   then show ?thesis

  1054     by (cases "b = 0") (simp_all add: unit_factor_mult)

  1055 qed

  1056

  1057 lemma dvd_normalize_div:

  1058   assumes "b dvd a"

  1059   shows "normalize (a div b) = normalize a div normalize b"

  1060 proof -

  1061   from assms have "a = a div b * b"

  1062     by simp

  1063   then have "normalize a = normalize (a div b * b)"

  1064     by simp

  1065   then show ?thesis

  1066     by (cases "b = 0") (simp_all add: normalize_mult)

  1067 qed

  1068

  1069 lemma normalize_dvd_iff [simp]:

  1070   "normalize a dvd b \<longleftrightarrow> a dvd b"

  1071 proof -

  1072   have "normalize a dvd b \<longleftrightarrow> unit_factor a * normalize a dvd b"

  1073     using mult_unit_dvd_iff [of "unit_factor a" "normalize a" b]

  1074       by (cases "a = 0") simp_all

  1075   then show ?thesis by simp

  1076 qed

  1077

  1078 lemma dvd_normalize_iff [simp]:

  1079   "a dvd normalize b \<longleftrightarrow> a dvd b"

  1080 proof -

  1081   have "a dvd normalize  b \<longleftrightarrow> a dvd normalize b * unit_factor b"

  1082     using dvd_mult_unit_iff [of "unit_factor b" a "normalize b"]

  1083       by (cases "b = 0") simp_all

  1084   then show ?thesis by simp

  1085 qed

  1086

  1087 text \<open>

  1088   We avoid an explicit definition of associated elements but prefer

  1089   explicit normalisation instead.  In theory we could define an abbreviation

  1090   like @{prop "associated a b \<longleftrightarrow> normalize a = normalize b"} but this is

  1091   counterproductive without suggestive infix syntax, which we do not want

  1092   to sacrifice for this purpose here.

  1093 \<close>

  1094

  1095 lemma associatedI:

  1096   assumes "a dvd b" and "b dvd a"

  1097   shows "normalize a = normalize b"

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

  1099   case True with assms show ?thesis by auto

  1100 next

  1101   case False

  1102   from \<open>a dvd b\<close> obtain c where b: "b = a * c" ..

  1103   moreover from \<open>b dvd a\<close> obtain d where a: "a = b * d" ..

  1104   ultimately have "b * 1 = b * (c * d)" by (simp add: ac_simps)

  1105   with False have "1 = c * d"

  1106     unfolding mult_cancel_left by simp

  1107   then have "is_unit c" and "is_unit d" by auto

  1108   with a b show ?thesis by (simp add: normalize_mult is_unit_normalize)

  1109 qed

  1110

  1111 lemma associatedD1:

  1112   "normalize a = normalize b \<Longrightarrow> a dvd b"

  1113   using dvd_normalize_iff [of _ b, symmetric] normalize_dvd_iff [of a _, symmetric]

  1114   by simp

  1115

  1116 lemma associatedD2:

  1117   "normalize a = normalize b \<Longrightarrow> b dvd a"

  1118   using dvd_normalize_iff [of _ a, symmetric] normalize_dvd_iff [of b _, symmetric]

  1119   by simp

  1120

  1121 lemma associated_unit:

  1122   "normalize a = normalize b \<Longrightarrow> is_unit a \<Longrightarrow> is_unit b"

  1123   using dvd_unit_imp_unit by (auto dest!: associatedD1 associatedD2)

  1124

  1125 lemma associated_iff_dvd:

  1126   "normalize a = normalize b \<longleftrightarrow> a dvd b \<and> b dvd a" (is "?P \<longleftrightarrow> ?Q")

  1127 proof

  1128   assume ?Q then show ?P by (auto intro!: associatedI)

  1129 next

  1130   assume ?P

  1131   then have "unit_factor a * normalize a = unit_factor a * normalize b"

  1132     by simp

  1133   then have *: "normalize b * unit_factor a = a"

  1134     by (simp add: ac_simps)

  1135   show ?Q

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

  1137     case True with \<open>?P\<close> show ?thesis by auto

  1138   next

  1139     case False

  1140     then have "b dvd normalize b * unit_factor a" and "normalize b * unit_factor a dvd b"

  1141       by (simp_all add: mult_unit_dvd_iff dvd_mult_unit_iff)

  1142     with * show ?thesis by simp

  1143   qed

  1144 qed

  1145

  1146 lemma associated_eqI:

  1147   assumes "a dvd b" and "b dvd a"

  1148   assumes "normalize a = a" and "normalize b = b"

  1149   shows "a = b"

  1150 proof -

  1151   from assms have "normalize a = normalize b"

  1152     unfolding associated_iff_dvd by simp

  1153   with \<open>normalize a = a\<close> have "a = normalize b" by simp

  1154   with \<open>normalize b = b\<close> show "a = b" by simp

  1155 qed

  1156

  1157 end

  1158

  1159 class ordered_semiring = semiring + comm_monoid_add + ordered_ab_semigroup_add +

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

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

  1162 begin

  1163

  1164 lemma mult_mono:

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

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

  1167 apply (erule mult_left_mono, assumption)

  1168 done

  1169

  1170 lemma mult_mono':

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

  1172 apply (rule mult_mono)

  1173 apply (fast intro: order_trans)+

  1174 done

  1175

  1176 end

  1177

  1178 class ordered_cancel_semiring = ordered_semiring + cancel_comm_monoid_add

  1179 begin

  1180

  1181 subclass semiring_0_cancel ..

  1182

  1183 lemma mult_nonneg_nonneg[simp]: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b"

  1184 using mult_left_mono [of 0 b a] by simp

  1185

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

  1187 using mult_left_mono [of b 0 a] by simp

  1188

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

  1190 using mult_right_mono [of a 0 b] by simp

  1191

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

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

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

  1195

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

  1197 by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)

  1198

  1199 end

  1200

  1201 class linordered_semiring = ordered_semiring + linordered_cancel_ab_semigroup_add

  1202 begin

  1203

  1204 subclass ordered_cancel_semiring ..

  1205

  1206 subclass ordered_comm_monoid_add ..

  1207

  1208 lemma mult_left_less_imp_less:

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

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

  1211

  1212 lemma mult_right_less_imp_less:

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

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

  1215

  1216 end

  1217

  1218 class linordered_semiring_1 = linordered_semiring + semiring_1

  1219 begin

  1220

  1221 lemma convex_bound_le:

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

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

  1224 proof-

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

  1226     by (simp add: add_mono mult_left_mono)

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

  1228 qed

  1229

  1230 end

  1231

  1232 class linordered_semiring_strict = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add +

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

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

  1235 begin

  1236

  1237 subclass semiring_0_cancel ..

  1238

  1239 subclass linordered_semiring

  1240 proof

  1241   fix a b c :: 'a

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

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

  1244     unfolding le_less

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

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

  1247     unfolding le_less

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

  1249 qed

  1250

  1251 lemma mult_left_le_imp_le:

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

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

  1254

  1255 lemma mult_right_le_imp_le:

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

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

  1258

  1259 lemma mult_pos_pos[simp]: "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a * b"

  1260 using mult_strict_left_mono [of 0 b a] by simp

  1261

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

  1263 using mult_strict_left_mono [of b 0 a] by simp

  1264

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

  1266 using mult_strict_right_mono [of a 0 b] by simp

  1267

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

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

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

  1271

  1272 lemma zero_less_mult_pos:

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

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

  1275  apply (auto simp add: le_less not_less)

  1276 apply (drule_tac mult_pos_neg [of a b])

  1277  apply (auto dest: less_not_sym)

  1278 done

  1279

  1280 lemma zero_less_mult_pos2:

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

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

  1283  apply (auto simp add: le_less not_less)

  1284 apply (drule_tac mult_pos_neg2 [of a b])

  1285  apply (auto dest: less_not_sym)

  1286 done

  1287

  1288 text{*Strict monotonicity in both arguments*}

  1289 lemma mult_strict_mono:

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

  1291   shows "a * c < b * d"

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

  1293   apply (simp)

  1294   apply (erule mult_strict_right_mono [THEN less_trans])

  1295   apply (force simp add: le_less)

  1296   apply (erule mult_strict_left_mono, assumption)

  1297   done

  1298

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

  1300 lemma mult_strict_mono':

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

  1302   shows "a * c < b * d"

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

  1304

  1305 lemma mult_less_le_imp_less:

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

  1307   shows "a * c < b * d"

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

  1309   apply (erule less_le_trans)

  1310   apply (erule mult_left_mono)

  1311   apply simp

  1312   apply (erule mult_strict_right_mono)

  1313   apply assumption

  1314   done

  1315

  1316 lemma mult_le_less_imp_less:

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

  1318   shows "a * c < b * d"

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

  1320   apply (erule le_less_trans)

  1321   apply (erule mult_strict_left_mono)

  1322   apply simp

  1323   apply (erule mult_right_mono)

  1324   apply simp

  1325   done

  1326

  1327 end

  1328

  1329 class linordered_semiring_1_strict = linordered_semiring_strict + semiring_1

  1330 begin

  1331

  1332 subclass linordered_semiring_1 ..

  1333

  1334 lemma convex_bound_lt:

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

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

  1337 proof -

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

  1339     by (cases "u = 0")

  1340        (auto intro!: add_less_le_mono mult_strict_left_mono mult_left_mono)

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

  1342 qed

  1343

  1344 end

  1345

  1346 class ordered_comm_semiring = comm_semiring_0 + ordered_ab_semigroup_add +

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

  1348 begin

  1349

  1350 subclass ordered_semiring

  1351 proof

  1352   fix a b c :: 'a

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

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

  1355   thus "a * c \<le> b * c" by (simp only: mult.commute)

  1356 qed

  1357

  1358 end

  1359

  1360 class ordered_cancel_comm_semiring = ordered_comm_semiring + cancel_comm_monoid_add

  1361 begin

  1362

  1363 subclass comm_semiring_0_cancel ..

  1364 subclass ordered_comm_semiring ..

  1365 subclass ordered_cancel_semiring ..

  1366

  1367 end

  1368

  1369 class linordered_comm_semiring_strict = comm_semiring_0 + linordered_cancel_ab_semigroup_add +

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

  1371 begin

  1372

  1373 subclass linordered_semiring_strict

  1374 proof

  1375   fix a b c :: 'a

  1376   assume "a < b" "0 < c"

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

  1378   thus "a * c < b * c" by (simp only: mult.commute)

  1379 qed

  1380

  1381 subclass ordered_cancel_comm_semiring

  1382 proof

  1383   fix a b c :: 'a

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

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

  1386     unfolding le_less

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

  1388 qed

  1389

  1390 end

  1391

  1392 class ordered_ring = ring + ordered_cancel_semiring

  1393 begin

  1394

  1395 subclass ordered_ab_group_add ..

  1396

  1397 lemma less_add_iff1:

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

  1399 by (simp add: algebra_simps)

  1400

  1401 lemma less_add_iff2:

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

  1403 by (simp add: algebra_simps)

  1404

  1405 lemma le_add_iff1:

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

  1407 by (simp add: algebra_simps)

  1408

  1409 lemma le_add_iff2:

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

  1411 by (simp add: algebra_simps)

  1412

  1413 lemma mult_left_mono_neg:

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

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

  1416   apply simp_all

  1417   done

  1418

  1419 lemma mult_right_mono_neg:

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

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

  1422   apply simp_all

  1423   done

  1424

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

  1426 using mult_right_mono_neg [of a 0 b] by simp

  1427

  1428 lemma split_mult_pos_le:

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

  1430 by (auto simp add: mult_nonpos_nonpos)

  1431

  1432 end

  1433

  1434 class linordered_ring = ring + linordered_semiring + linordered_ab_group_add + abs_if

  1435 begin

  1436

  1437 subclass ordered_ring ..

  1438

  1439 subclass ordered_ab_group_add_abs

  1440 proof

  1441   fix a b

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

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

  1444 qed (auto simp add: abs_if)

  1445

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

  1447   using linear [of 0 a]

  1448   by (auto simp add: mult_nonpos_nonpos)

  1449

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

  1451   by (simp add: not_less)

  1452

  1453 end

  1454

  1455 class linordered_ring_strict = ring + linordered_semiring_strict

  1456   + ordered_ab_group_add + abs_if

  1457 begin

  1458

  1459 subclass linordered_ring ..

  1460

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

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

  1463

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

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

  1466

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

  1468 using mult_strict_right_mono_neg [of a 0 b] by simp

  1469

  1470 subclass ring_no_zero_divisors

  1471 proof

  1472   fix a b

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

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

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

  1476   proof (cases "a < 0")

  1477     case True note A' = this

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

  1479       case True with A'

  1480       show ?thesis by (auto dest: mult_neg_neg)

  1481     next

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

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

  1484     qed

  1485   next

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

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

  1488       case True with A'

  1489       show ?thesis by (auto dest: mult_strict_right_mono_neg)

  1490     next

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

  1492       with A' show ?thesis by auto

  1493     qed

  1494   qed

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

  1496 qed

  1497

  1498 lemma zero_less_mult_iff: "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0"

  1499   by (cases a 0 b 0 rule: linorder_cases[case_product linorder_cases])

  1500      (auto simp add: mult_neg_neg not_less le_less dest: zero_less_mult_pos zero_less_mult_pos2)

  1501

  1502 lemma zero_le_mult_iff: "0 \<le> a * b \<longleftrightarrow> 0 \<le> a \<and> 0 \<le> b \<or> a \<le> 0 \<and> b \<le> 0"

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

  1504

  1505 lemma mult_less_0_iff:

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

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

  1508   apply force

  1509   done

  1510

  1511 lemma mult_le_0_iff:

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

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

  1514   apply force

  1515   done

  1516

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

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

  1519

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

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

  1522

  1523 lemma mult_less_cancel_right_disj:

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

  1525   apply (cases "c = 0")

  1526   apply (auto simp add: neq_iff mult_strict_right_mono

  1527                       mult_strict_right_mono_neg)

  1528   apply (auto simp add: not_less

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

  1530                       not_le [symmetric, of a])

  1531   apply (erule_tac [!] notE)

  1532   apply (auto simp add: less_imp_le mult_right_mono

  1533                       mult_right_mono_neg)

  1534   done

  1535

  1536 lemma mult_less_cancel_left_disj:

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

  1538   apply (cases "c = 0")

  1539   apply (auto simp add: neq_iff mult_strict_left_mono

  1540                       mult_strict_left_mono_neg)

  1541   apply (auto simp add: not_less

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

  1543                       not_le [symmetric, of a])

  1544   apply (erule_tac [!] notE)

  1545   apply (auto simp add: less_imp_le mult_left_mono

  1546                       mult_left_mono_neg)

  1547   done

  1548

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

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

  1551

  1552 lemma mult_less_cancel_right:

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

  1554   using mult_less_cancel_right_disj [of a c b] by auto

  1555

  1556 lemma mult_less_cancel_left:

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

  1558   using mult_less_cancel_left_disj [of c a b] by auto

  1559

  1560 lemma mult_le_cancel_right:

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

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

  1563

  1564 lemma mult_le_cancel_left:

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

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

  1567

  1568 lemma mult_le_cancel_left_pos:

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

  1570 by (auto simp: mult_le_cancel_left)

  1571

  1572 lemma mult_le_cancel_left_neg:

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

  1574 by (auto simp: mult_le_cancel_left)

  1575

  1576 lemma mult_less_cancel_left_pos:

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

  1578 by (auto simp: mult_less_cancel_left)

  1579

  1580 lemma mult_less_cancel_left_neg:

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

  1582 by (auto simp: mult_less_cancel_left)

  1583

  1584 end

  1585

  1586 lemmas mult_sign_intros =

  1587   mult_nonneg_nonneg mult_nonneg_nonpos

  1588   mult_nonpos_nonneg mult_nonpos_nonpos

  1589   mult_pos_pos mult_pos_neg

  1590   mult_neg_pos mult_neg_neg

  1591

  1592 class ordered_comm_ring = comm_ring + ordered_comm_semiring

  1593 begin

  1594

  1595 subclass ordered_ring ..

  1596 subclass ordered_cancel_comm_semiring ..

  1597

  1598 end

  1599

  1600 class linordered_semidom = semidom + linordered_comm_semiring_strict +

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

  1602   assumes le_add_diff_inverse2 [simp]: "b \<le> a \<Longrightarrow> a - b + b = a"

  1603 begin

  1604

  1605 text {* Addition is the inverse of subtraction. *}

  1606

  1607 lemma le_add_diff_inverse [simp]: "b \<le> a \<Longrightarrow> b + (a - b) = a"

  1608   by (frule le_add_diff_inverse2) (simp add: add.commute)

  1609

  1610 lemma add_diff_inverse: "~ a<b \<Longrightarrow> b + (a - b) = a"

  1611   by simp

  1612

  1613 lemma add_le_imp_le_diff:

  1614   shows "i + k \<le> n \<Longrightarrow> i \<le> n - k"

  1615   apply (subst add_le_cancel_right [where c=k, symmetric])

  1616   apply (frule le_add_diff_inverse2)

  1617   apply (simp only: add.assoc [symmetric])

  1618   using add_implies_diff by fastforce

  1619

  1620 lemma add_le_add_imp_diff_le:

  1621   assumes a1: "i + k \<le> n"

  1622       and a2: "n \<le> j + k"

  1623   shows "\<lbrakk>i + k \<le> n; n \<le> j + k\<rbrakk> \<Longrightarrow> n - k \<le> j"

  1624 proof -

  1625   have "n - (i + k) + (i + k) = n"

  1626     using a1 by simp

  1627   moreover have "n - k = n - k - i + i"

  1628     using a1 by (simp add: add_le_imp_le_diff)

  1629   ultimately show ?thesis

  1630     using a2

  1631     apply (simp add: add.assoc [symmetric])

  1632     apply (rule add_le_imp_le_diff [of _ k "j+k", simplified add_diff_cancel_right'])

  1633     by (simp add: add.commute diff_diff_add)

  1634 qed

  1635

  1636 lemma pos_add_strict:

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

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

  1639

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

  1641 by (rule zero_less_one [THEN less_imp_le])

  1642

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

  1644 by (simp add: not_le)

  1645

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

  1647 by (simp add: not_less)

  1648

  1649 lemma less_1_mult:

  1650   assumes "1 < m" and "1 < n"

  1651   shows "1 < m * n"

  1652   using assms mult_strict_mono [of 1 m 1 n]

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

  1654

  1655 lemma mult_left_le: "c \<le> 1 \<Longrightarrow> 0 \<le> a \<Longrightarrow> a * c \<le> a"

  1656   using mult_left_mono[of c 1 a] by simp

  1657

  1658 lemma mult_le_one: "a \<le> 1 \<Longrightarrow> 0 \<le> b \<Longrightarrow> b \<le> 1 \<Longrightarrow> a * b \<le> 1"

  1659   using mult_mono[of a 1 b 1] by simp

  1660

  1661 end

  1662

  1663 class linordered_idom = comm_ring_1 +

  1664   linordered_comm_semiring_strict + ordered_ab_group_add +

  1665   abs_if + sgn_if

  1666 begin

  1667

  1668 subclass linordered_semiring_1_strict ..

  1669 subclass linordered_ring_strict ..

  1670 subclass ordered_comm_ring ..

  1671 subclass idom ..

  1672

  1673 subclass linordered_semidom

  1674 proof

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

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

  1677   show "\<And>b a. b \<le> a \<Longrightarrow> a - b + b = a"

  1678     by simp

  1679 qed

  1680

  1681 lemma linorder_neqE_linordered_idom:

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

  1683   using assms by (rule neqE)

  1684

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

  1686

  1687 lemma mult_le_cancel_right1:

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

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

  1690

  1691 lemma mult_le_cancel_right2:

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

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

  1694

  1695 lemma mult_le_cancel_left1:

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

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

  1698

  1699 lemma mult_le_cancel_left2:

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

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

  1702

  1703 lemma mult_less_cancel_right1:

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

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

  1706

  1707 lemma mult_less_cancel_right2:

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

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

  1710

  1711 lemma mult_less_cancel_left1:

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

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

  1714

  1715 lemma mult_less_cancel_left2:

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

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

  1718

  1719 lemma sgn_sgn [simp]:

  1720   "sgn (sgn a) = sgn a"

  1721 unfolding sgn_if by simp

  1722

  1723 lemma sgn_0_0:

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

  1725 unfolding sgn_if by simp

  1726

  1727 lemma sgn_1_pos:

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

  1729 unfolding sgn_if by simp

  1730

  1731 lemma sgn_1_neg:

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

  1733 unfolding sgn_if by auto

  1734

  1735 lemma sgn_pos [simp]:

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

  1737 unfolding sgn_1_pos .

  1738

  1739 lemma sgn_neg [simp]:

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

  1741 unfolding sgn_1_neg .

  1742

  1743 lemma sgn_times:

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

  1745 by (auto simp add: sgn_if zero_less_mult_iff)

  1746

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

  1748 unfolding sgn_if abs_if by auto

  1749

  1750 lemma sgn_greater [simp]:

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

  1752   unfolding sgn_if by auto

  1753

  1754 lemma sgn_less [simp]:

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

  1756   unfolding sgn_if by auto

  1757

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

  1759   by (simp add: abs_if)

  1760

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

  1762   by (simp add: abs_if)

  1763

  1764 lemma dvd_if_abs_eq:

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

  1766 by(subst abs_dvd_iff[symmetric]) simp

  1767

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

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

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

  1771

  1772 lemma equation_minus_iff_1 [simp, no_atp]:

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

  1774   by (fact equation_minus_iff)

  1775

  1776 lemma minus_equation_iff_1 [simp, no_atp]:

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

  1778   by (subst minus_equation_iff, auto)

  1779

  1780 lemma le_minus_iff_1 [simp, no_atp]:

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

  1782   by (fact le_minus_iff)

  1783

  1784 lemma minus_le_iff_1 [simp, no_atp]:

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

  1786   by (fact minus_le_iff)

  1787

  1788 lemma less_minus_iff_1 [simp, no_atp]:

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

  1790   by (fact less_minus_iff)

  1791

  1792 lemma minus_less_iff_1 [simp, no_atp]:

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

  1794   by (fact minus_less_iff)

  1795

  1796 end

  1797

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

  1799

  1800 lemmas mult_compare_simps =

  1801     mult_le_cancel_right mult_le_cancel_left

  1802     mult_le_cancel_right1 mult_le_cancel_right2

  1803     mult_le_cancel_left1 mult_le_cancel_left2

  1804     mult_less_cancel_right mult_less_cancel_left

  1805     mult_less_cancel_right1 mult_less_cancel_right2

  1806     mult_less_cancel_left1 mult_less_cancel_left2

  1807     mult_cancel_right mult_cancel_left

  1808     mult_cancel_right1 mult_cancel_right2

  1809     mult_cancel_left1 mult_cancel_left2

  1810

  1811 text {* Reasoning about inequalities with division *}

  1812

  1813 context linordered_semidom

  1814 begin

  1815

  1816 lemma less_add_one: "a < a + 1"

  1817 proof -

  1818   have "a + 0 < a + 1"

  1819     by (blast intro: zero_less_one add_strict_left_mono)

  1820   thus ?thesis by simp

  1821 qed

  1822

  1823 lemma zero_less_two: "0 < 1 + 1"

  1824 by (blast intro: less_trans zero_less_one less_add_one)

  1825

  1826 end

  1827

  1828 context linordered_idom

  1829 begin

  1830

  1831 lemma mult_right_le_one_le:

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

  1833   by (rule mult_left_le)

  1834

  1835 lemma mult_left_le_one_le:

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

  1837   by (auto simp add: mult_le_cancel_right2)

  1838

  1839 end

  1840

  1841 text {* Absolute Value *}

  1842

  1843 context linordered_idom

  1844 begin

  1845

  1846 lemma mult_sgn_abs:

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

  1848   unfolding abs_if sgn_if by auto

  1849

  1850 lemma abs_one [simp]:

  1851   "\<bar>1\<bar> = 1"

  1852   by (simp add: abs_if)

  1853

  1854 end

  1855

  1856 class ordered_ring_abs = ordered_ring + ordered_ab_group_add_abs +

  1857   assumes abs_eq_mult:

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

  1859

  1860 context linordered_idom

  1861 begin

  1862

  1863 subclass ordered_ring_abs proof

  1864 qed (auto simp add: abs_if not_less mult_less_0_iff)

  1865

  1866 lemma abs_mult:

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

  1868   by (rule abs_eq_mult) auto

  1869

  1870 lemma abs_mult_self:

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

  1872   by (simp add: abs_if)

  1873

  1874 lemma abs_mult_less:

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

  1876 proof -

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

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

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

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

  1881 qed

  1882

  1883 lemma abs_less_iff:

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

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

  1886

  1887 lemma abs_mult_pos:

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

  1889   by (simp add: abs_mult)

  1890

  1891 lemma abs_diff_less_iff:

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

  1893   by (auto simp add: diff_less_eq ac_simps abs_less_iff)

  1894

  1895 lemma abs_diff_le_iff:

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

  1897   by (auto simp add: diff_le_eq ac_simps abs_le_iff)

  1898

  1899 end

  1900

  1901 hide_fact (open) comm_mult_left_mono comm_mult_strict_left_mono distrib

  1902

  1903 code_identifier

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

  1905

  1906 end