src/HOL/Rings.thy
 author wenzelm Mon Dec 28 01:26:34 2015 +0100 (2015-12-28) changeset 61944 5d06ecfdb472 parent 61799 4cf66f21b764 child 62347 2230b7047376 permissions -rw-r--r--
prefer symbols for "abs";
     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 \<open>Rings\<close>

    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\<open>For the \<open>combine_numerals\<close> simproc\<close>

    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 \<open>Abstract divisibility\<close>

   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 \<open>a dvd b\<close> obtain b' where "b = a * b'" ..

   184   moreover from \<open>c dvd d\<close> 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 \<open>a dvd b\<close> obtain b' where "b = a * b'" ..

   223   moreover from \<open>a dvd c\<close> 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 \<open>a dvd b\<close> 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 \<open>Distribution rules\<close>

   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\<open>Extract signs from products\<close>

   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 \<open>

   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 \<close>

   558

   559 class divide =

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

   561

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

   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 \<open>Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a::divide \<Rightarrow> 'a \<Rightarrow> 'a"})\<close>

   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 lemma divide_1 [simp]:

   633   "a div 1 = a"

   634   using nonzero_mult_divide_cancel_left [of 1 a] by simp

   635

   636 end

   637

   638 class idom_divide = idom + semidom_divide

   639

   640 class algebraic_semidom = semidom_divide

   641 begin

   642

   643 text \<open>

   644   Class @{class algebraic_semidom} enriches a integral domain

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

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

   647   which are degenerated there.

   648 \<close>

   649

   650 lemma dvd_times_left_cancel_iff [simp]:

   651   assumes "a \<noteq> 0"

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

   653 proof

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

   655   with assms have "c = b * d" by (simp add: ac_simps)

   656   then show ?Q ..

   657 next

   658   assume ?Q then obtain d where "c = b * d" ..

   659   then have "a * c = a * b * d" by (simp add: ac_simps)

   660   then show ?P ..

   661 qed

   662

   663 lemma dvd_times_right_cancel_iff [simp]:

   664   assumes "a \<noteq> 0"

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

   666 using dvd_times_left_cancel_iff [of a b c] assms by (simp add: ac_simps)

   667

   668 lemma div_dvd_iff_mult:

   669   assumes "b \<noteq> 0" and "b dvd a"

   670   shows "a div b dvd c \<longleftrightarrow> a dvd c * b"

   671 proof -

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

   673   with \<open>b \<noteq> 0\<close> show ?thesis by (simp add: ac_simps)

   674 qed

   675

   676 lemma dvd_div_iff_mult:

   677   assumes "c \<noteq> 0" and "c dvd b"

   678   shows "a dvd b div c \<longleftrightarrow> a * c dvd b"

   679 proof -

   680   from \<open>c dvd b\<close> obtain d where "b = c * d" ..

   681   with \<open>c \<noteq> 0\<close> show ?thesis by (simp add: mult.commute [of a])

   682 qed

   683

   684 lemma div_dvd_div [simp]:

   685   assumes "a dvd b" and "a dvd c"

   686   shows "b div a dvd c div a \<longleftrightarrow> b dvd c"

   687 proof (cases "a = 0")

   688   case True with assms show ?thesis by simp

   689 next

   690   case False

   691   moreover from assms obtain k l where "b = a * k" and "c = a * l"

   692     by (auto elim!: dvdE)

   693   ultimately show ?thesis by simp

   694 qed

   695

   696 lemma div_add [simp]:

   697   assumes "c dvd a" and "c dvd b"

   698   shows "(a + b) div c = a div c + b div c"

   699 proof (cases "c = 0")

   700   case True then show ?thesis by simp

   701 next

   702   case False

   703   moreover from assms obtain k l where "a = c * k" and "b = c * l"

   704     by (auto elim!: dvdE)

   705   moreover have "c * k + c * l = c * (k + l)"

   706     by (simp add: algebra_simps)

   707   ultimately show ?thesis

   708     by simp

   709 qed

   710

   711 lemma div_mult_div_if_dvd:

   712   assumes "b dvd a" and "d dvd c"

   713   shows "(a div b) * (c div d) = (a * c) div (b * d)"

   714 proof (cases "b = 0 \<or> c = 0")

   715   case True with assms show ?thesis by auto

   716 next

   717   case False

   718   moreover from assms obtain k l where "a = b * k" and "c = d * l"

   719     by (auto elim!: dvdE)

   720   moreover have "b * k * (d * l) div (b * d) = (b * d) * (k * l) div (b * d)"

   721     by (simp add: ac_simps)

   722   ultimately show ?thesis by simp

   723 qed

   724

   725 lemma dvd_div_eq_mult:

   726   assumes "a \<noteq> 0" and "a dvd b"

   727   shows "b div a = c \<longleftrightarrow> b = c * a"

   728 proof

   729   assume "b = c * a"

   730   then show "b div a = c" by (simp add: assms)

   731 next

   732   assume "b div a = c"

   733   then have "b div a * a = c * a" by simp

   734   moreover from \<open>a \<noteq> 0\<close> \<open>a dvd b\<close> have "b div a * a = b"

   735     by (auto elim!: dvdE simp add: ac_simps)

   736   ultimately show "b = c * a" by simp

   737 qed

   738

   739 lemma dvd_div_mult_self [simp]:

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

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

   742

   743 lemma dvd_mult_div_cancel [simp]:

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

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

   746

   747 lemma div_mult_swap:

   748   assumes "c dvd b"

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

   750 proof (cases "c = 0")

   751   case True then show ?thesis by simp

   752 next

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

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

   755     by simp

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

   757 qed

   758

   759 lemma dvd_div_mult:

   760   assumes "c dvd b"

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

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

   763

   764 lemma dvd_div_mult2_eq:

   765   assumes "b * c dvd a"

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

   767 using assms proof

   768   fix k

   769   assume "a = b * c * k"

   770   then show ?thesis

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

   772 qed

   773

   774 lemma dvd_div_div_eq_mult:

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

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

   777 proof -

   778   from assms have "a * c \<noteq> 0" by simp

   779   then have "?P \<longleftrightarrow> b div a * (a * c) = d div c * (a * c)"

   780     by simp

   781   also have "\<dots> \<longleftrightarrow> (a * (b div a)) * c = (c * (d div c)) * a"

   782     by (simp add: ac_simps)

   783   also have "\<dots> \<longleftrightarrow> (a * b div a) * c = (c * d div c) * a"

   784     using assms by (simp add: div_mult_swap)

   785   also have "\<dots> \<longleftrightarrow> ?Q"

   786     using assms by (simp add: ac_simps)

   787   finally show ?thesis .

   788 qed

   789

   790

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

   792

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

   794 where

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

   796

   797 lemma not_is_unit_0 [simp]:

   798   "\<not> is_unit 0"

   799   by simp

   800

   801 lemma unit_imp_dvd [dest]:

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

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

   804

   805 lemma unit_dvdE:

   806   assumes "is_unit a"

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

   808 proof -

   809   from assms have "a dvd b" by auto

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

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

   812   ultimately show thesis using that by blast

   813 qed

   814

   815 lemma dvd_unit_imp_unit:

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

   817   by (rule dvd_trans)

   818

   819 lemma unit_div_1_unit [simp, intro]:

   820   assumes "is_unit a"

   821   shows "is_unit (1 div a)"

   822 proof -

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

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

   825 qed

   826

   827 lemma is_unitE [elim?]:

   828   assumes "is_unit a"

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

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

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

   832 proof (rule that)

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

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

   835   from b_def \<open>is_unit a\<close> show "is_unit b" by simp

   836   from \<open>is_unit a\<close> and \<open>is_unit b\<close> show "a \<noteq> 0" and "b \<noteq> 0" by auto

   837   from b_def \<open>is_unit a\<close> show "a * b = 1" by simp

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

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

   840   from \<open>is_unit a\<close> have "a dvd c" ..

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

   842   with \<open>a \<noteq> 0\<close> \<open>a * b = 1\<close> show "c div a = c * b"

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

   844 qed

   845

   846 lemma unit_prod [intro]:

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

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

   849

   850 lemma unit_div [intro]:

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

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

   853

   854 lemma mult_unit_dvd_iff:

   855   assumes "is_unit b"

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

   857 proof

   858   assume "a * b dvd c"

   859   with assms show "a dvd c"

   860     by (simp add: dvd_mult_left)

   861 next

   862   assume "a dvd c"

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

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

   865     by (simp add: mult_ac)

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

   867 qed

   868

   869 lemma dvd_mult_unit_iff:

   870   assumes "is_unit b"

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

   872 proof

   873   assume "a dvd c * b"

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

   875     by (subst mult_assoc [symmetric]) simp

   876   also from \<open>is_unit b\<close> have "b * (1 div b) = 1" by (rule is_unitE) simp

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

   878   with \<open>a dvd c * b\<close> show "a dvd c" by (rule dvd_trans)

   879 next

   880   assume "a dvd c"

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

   882 qed

   883

   884 lemma div_unit_dvd_iff:

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

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

   887

   888 lemma dvd_div_unit_iff:

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

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

   891

   892 lemmas unit_dvd_iff = mult_unit_dvd_iff div_unit_dvd_iff

   893   dvd_mult_unit_iff dvd_div_unit_iff \<comment> \<open>FIXME consider fact collection\<close>

   894

   895 lemma unit_mult_div_div [simp]:

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

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

   898

   899 lemma unit_div_mult_self [simp]:

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

   901   by (rule dvd_div_mult_self) auto

   902

   903 lemma unit_div_1_div_1 [simp]:

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

   905   by (erule is_unitE) simp

   906

   907 lemma unit_div_mult_swap:

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

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

   910

   911 lemma unit_div_commute:

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

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

   914

   915 lemma unit_eq_div1:

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

   917   by (auto elim: is_unitE)

   918

   919 lemma unit_eq_div2:

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

   921   using unit_eq_div1 [of b c a] by auto

   922

   923 lemma unit_mult_left_cancel:

   924   assumes "is_unit a"

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

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

   927

   928 lemma unit_mult_right_cancel:

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

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

   931

   932 lemma unit_div_cancel:

   933   assumes "is_unit a"

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

   935 proof -

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

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

   938     by (rule unit_mult_right_cancel)

   939   with assms show ?thesis by simp

   940 qed

   941

   942 lemma is_unit_div_mult2_eq:

   943   assumes "is_unit b" and "is_unit c"

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

   945 proof -

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

   947   then have "b * c dvd a"

   948     by (rule unit_imp_dvd)

   949   then show ?thesis

   950     by (rule dvd_div_mult2_eq)

   951 qed

   952

   953 lemmas unit_simps = mult_unit_dvd_iff div_unit_dvd_iff dvd_mult_unit_iff

   954   dvd_div_unit_iff unit_div_mult_swap unit_div_commute

   955   unit_mult_left_cancel unit_mult_right_cancel unit_div_cancel

   956   unit_eq_div1 unit_eq_div2

   957

   958 lemma is_unit_divide_mult_cancel_left:

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

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

   961 proof -

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

   963     by (simp add: mult_unit_dvd_iff dvd_div_mult2_eq)

   964   with assms show ?thesis by simp

   965 qed

   966

   967 lemma is_unit_divide_mult_cancel_right:

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

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

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

   971

   972 end

   973

   974 class normalization_semidom = algebraic_semidom +

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

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

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

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

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

   980   assumes is_unit_normalize:

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

   982   assumes unit_factor_is_unit [iff]:

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

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

   985 begin

   986

   987 text \<open>

   988   Class @{class normalization_semidom} cultivates the idea that

   989   each integral domain can be split into equivalence classes

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

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

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

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

   994   values rather than associated elements.

   995 \<close>

   996

   997 lemma unit_factor_dvd [simp]:

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

   999   by (rule unit_imp_dvd) simp

  1000

  1001 lemma unit_factor_self [simp]:

  1002   "unit_factor a dvd a"

  1003   by (cases "a = 0") simp_all

  1004

  1005 lemma normalize_mult_unit_factor [simp]:

  1006   "normalize a * unit_factor a = a"

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

  1008

  1009 lemma normalize_eq_0_iff [simp]:

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

  1011 proof

  1012   assume ?P

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

  1014   ultimately show ?Q by simp

  1015 next

  1016   assume ?Q then show ?P by simp

  1017 qed

  1018

  1019 lemma unit_factor_eq_0_iff [simp]:

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

  1021 proof

  1022   assume ?P

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

  1024   ultimately show ?Q by simp

  1025 next

  1026   assume ?Q then show ?P by simp

  1027 qed

  1028

  1029 lemma is_unit_unit_factor:

  1030   assumes "is_unit a" shows "unit_factor a = a"

  1031 proof -

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

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

  1034   ultimately show ?thesis by simp

  1035 qed

  1036

  1037 lemma unit_factor_1 [simp]:

  1038   "unit_factor 1 = 1"

  1039   by (rule is_unit_unit_factor) simp

  1040

  1041 lemma normalize_1 [simp]:

  1042   "normalize 1 = 1"

  1043   by (rule is_unit_normalize) simp

  1044

  1045 lemma normalize_1_iff:

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

  1047 proof

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

  1049 next

  1050   assume ?P

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

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

  1053     by simp

  1054   then have "unit_factor a = a"

  1055     by simp

  1056   moreover have "is_unit (unit_factor a)"

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

  1058   ultimately show ?Q by simp

  1059 qed

  1060

  1061 lemma div_normalize [simp]:

  1062   "a div normalize a = unit_factor a"

  1063 proof (cases "a = 0")

  1064   case True then show ?thesis by simp

  1065 next

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

  1067   with nonzero_mult_divide_cancel_right

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

  1069   then show ?thesis by simp

  1070 qed

  1071

  1072 lemma div_unit_factor [simp]:

  1073   "a div unit_factor a = normalize a"

  1074 proof (cases "a = 0")

  1075   case True then show ?thesis by simp

  1076 next

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

  1078   with nonzero_mult_divide_cancel_left

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

  1080   then show ?thesis by simp

  1081 qed

  1082

  1083 lemma normalize_div [simp]:

  1084   "normalize a div a = 1 div unit_factor a"

  1085 proof (cases "a = 0")

  1086   case True then show ?thesis by simp

  1087 next

  1088   case False

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

  1090     by simp

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

  1092     using False by (subst is_unit_divide_mult_cancel_right) simp_all

  1093   finally show ?thesis .

  1094 qed

  1095

  1096 lemma mult_one_div_unit_factor [simp]:

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

  1098   by (cases "b = 0") simp_all

  1099

  1100 lemma normalize_mult:

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

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

  1103   case True then show ?thesis by auto

  1104 next

  1105   case False

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

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

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

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

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

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

  1112     using False by (subst unit_div_mult_swap) simp_all

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

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

  1115   finally show ?thesis .

  1116 qed

  1117

  1118 lemma unit_factor_idem [simp]:

  1119   "unit_factor (unit_factor a) = unit_factor a"

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

  1121

  1122 lemma normalize_unit_factor [simp]:

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

  1124   by (rule is_unit_normalize) simp

  1125

  1126 lemma normalize_idem [simp]:

  1127   "normalize (normalize a) = normalize a"

  1128 proof (cases "a = 0")

  1129   case True then show ?thesis by simp

  1130 next

  1131   case False

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

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

  1134     by (simp only: normalize_mult)

  1135   finally show ?thesis using False by simp_all

  1136 qed

  1137

  1138 lemma unit_factor_normalize [simp]:

  1139   assumes "a \<noteq> 0"

  1140   shows "unit_factor (normalize a) = 1"

  1141 proof -

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

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

  1144     by (simp only: unit_factor_mult_normalize)

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

  1146     by simp

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

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

  1149     by simp

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

  1151   show ?thesis by simp

  1152 qed

  1153

  1154 lemma dvd_unit_factor_div:

  1155   assumes "b dvd a"

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

  1157 proof -

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

  1159     by simp

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

  1161     by simp

  1162   then show ?thesis

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

  1164 qed

  1165

  1166 lemma dvd_normalize_div:

  1167   assumes "b dvd a"

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

  1169 proof -

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

  1171     by simp

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

  1173     by simp

  1174   then show ?thesis

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

  1176 qed

  1177

  1178 lemma normalize_dvd_iff [simp]:

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

  1180 proof -

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

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

  1183       by (cases "a = 0") simp_all

  1184   then show ?thesis by simp

  1185 qed

  1186

  1187 lemma dvd_normalize_iff [simp]:

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

  1189 proof -

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

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

  1192       by (cases "b = 0") simp_all

  1193   then show ?thesis by simp

  1194 qed

  1195

  1196 text \<open>

  1197   We avoid an explicit definition of associated elements but prefer

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

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

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

  1201   to sacrifice for this purpose here.

  1202 \<close>

  1203

  1204 lemma associatedI:

  1205   assumes "a dvd b" and "b dvd a"

  1206   shows "normalize a = normalize b"

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

  1208   case True with assms show ?thesis by auto

  1209 next

  1210   case False

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

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

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

  1214   with False have "1 = c * d"

  1215     unfolding mult_cancel_left by simp

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

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

  1218 qed

  1219

  1220 lemma associatedD1:

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

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

  1223   by simp

  1224

  1225 lemma associatedD2:

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

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

  1228   by simp

  1229

  1230 lemma associated_unit:

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

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

  1233

  1234 lemma associated_iff_dvd:

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

  1236 proof

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

  1238 next

  1239   assume ?P

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

  1241     by simp

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

  1243     by (simp add: ac_simps)

  1244   show ?Q

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

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

  1247   next

  1248     case False

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

  1250       by (simp_all add: mult_unit_dvd_iff dvd_mult_unit_iff)

  1251     with * show ?thesis by simp

  1252   qed

  1253 qed

  1254

  1255 lemma associated_eqI:

  1256   assumes "a dvd b" and "b dvd a"

  1257   assumes "normalize a = a" and "normalize b = b"

  1258   shows "a = b"

  1259 proof -

  1260   from assms have "normalize a = normalize b"

  1261     unfolding associated_iff_dvd by simp

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

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

  1264 qed

  1265

  1266 end

  1267

  1268 class ordered_semiring = semiring + comm_monoid_add + ordered_ab_semigroup_add +

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

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

  1271 begin

  1272

  1273 lemma mult_mono:

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

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

  1276 apply (erule mult_left_mono, assumption)

  1277 done

  1278

  1279 lemma mult_mono':

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

  1281 apply (rule mult_mono)

  1282 apply (fast intro: order_trans)+

  1283 done

  1284

  1285 end

  1286

  1287 class ordered_cancel_semiring = ordered_semiring + cancel_comm_monoid_add

  1288 begin

  1289

  1290 subclass semiring_0_cancel ..

  1291

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

  1293 using mult_left_mono [of 0 b a] by simp

  1294

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

  1296 using mult_left_mono [of b 0 a] by simp

  1297

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

  1299 using mult_right_mono [of a 0 b] by simp

  1300

  1301 text \<open>Legacy - use \<open>mult_nonpos_nonneg\<close>\<close>

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

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

  1304

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

  1306 by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)

  1307

  1308 end

  1309

  1310 class linordered_semiring = ordered_semiring + linordered_cancel_ab_semigroup_add

  1311 begin

  1312

  1313 subclass ordered_cancel_semiring ..

  1314

  1315 subclass ordered_comm_monoid_add ..

  1316

  1317 lemma mult_left_less_imp_less:

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

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

  1320

  1321 lemma mult_right_less_imp_less:

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

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

  1324

  1325 end

  1326

  1327 class linordered_semiring_1 = linordered_semiring + semiring_1

  1328 begin

  1329

  1330 lemma convex_bound_le:

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

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

  1333 proof-

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

  1335     by (simp add: add_mono mult_left_mono)

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

  1337 qed

  1338

  1339 end

  1340

  1341 class linordered_semiring_strict = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add +

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

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

  1344 begin

  1345

  1346 subclass semiring_0_cancel ..

  1347

  1348 subclass linordered_semiring

  1349 proof

  1350   fix a b c :: 'a

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

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

  1353     unfolding le_less

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

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

  1356     unfolding le_less

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

  1358 qed

  1359

  1360 lemma mult_left_le_imp_le:

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

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

  1363

  1364 lemma mult_right_le_imp_le:

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

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

  1367

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

  1369 using mult_strict_left_mono [of 0 b a] by simp

  1370

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

  1372 using mult_strict_left_mono [of b 0 a] by simp

  1373

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

  1375 using mult_strict_right_mono [of a 0 b] by simp

  1376

  1377 text \<open>Legacy - use \<open>mult_neg_pos\<close>\<close>

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

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

  1380

  1381 lemma zero_less_mult_pos:

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

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

  1384  apply (auto simp add: le_less not_less)

  1385 apply (drule_tac mult_pos_neg [of a b])

  1386  apply (auto dest: less_not_sym)

  1387 done

  1388

  1389 lemma zero_less_mult_pos2:

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

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

  1392  apply (auto simp add: le_less not_less)

  1393 apply (drule_tac mult_pos_neg2 [of a b])

  1394  apply (auto dest: less_not_sym)

  1395 done

  1396

  1397 text\<open>Strict monotonicity in both arguments\<close>

  1398 lemma mult_strict_mono:

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

  1400   shows "a * c < b * d"

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

  1402   apply (simp)

  1403   apply (erule mult_strict_right_mono [THEN less_trans])

  1404   apply (force simp add: le_less)

  1405   apply (erule mult_strict_left_mono, assumption)

  1406   done

  1407

  1408 text\<open>This weaker variant has more natural premises\<close>

  1409 lemma mult_strict_mono':

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

  1411   shows "a * c < b * d"

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

  1413

  1414 lemma mult_less_le_imp_less:

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

  1416   shows "a * c < b * d"

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

  1418   apply (erule less_le_trans)

  1419   apply (erule mult_left_mono)

  1420   apply simp

  1421   apply (erule mult_strict_right_mono)

  1422   apply assumption

  1423   done

  1424

  1425 lemma mult_le_less_imp_less:

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

  1427   shows "a * c < b * d"

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

  1429   apply (erule le_less_trans)

  1430   apply (erule mult_strict_left_mono)

  1431   apply simp

  1432   apply (erule mult_right_mono)

  1433   apply simp

  1434   done

  1435

  1436 end

  1437

  1438 class linordered_semiring_1_strict = linordered_semiring_strict + semiring_1

  1439 begin

  1440

  1441 subclass linordered_semiring_1 ..

  1442

  1443 lemma convex_bound_lt:

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

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

  1446 proof -

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

  1448     by (cases "u = 0")

  1449        (auto intro!: add_less_le_mono mult_strict_left_mono mult_left_mono)

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

  1451 qed

  1452

  1453 end

  1454

  1455 class ordered_comm_semiring = comm_semiring_0 + ordered_ab_semigroup_add +

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

  1457 begin

  1458

  1459 subclass ordered_semiring

  1460 proof

  1461   fix a b c :: 'a

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

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

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

  1465 qed

  1466

  1467 end

  1468

  1469 class ordered_cancel_comm_semiring = ordered_comm_semiring + cancel_comm_monoid_add

  1470 begin

  1471

  1472 subclass comm_semiring_0_cancel ..

  1473 subclass ordered_comm_semiring ..

  1474 subclass ordered_cancel_semiring ..

  1475

  1476 end

  1477

  1478 class linordered_comm_semiring_strict = comm_semiring_0 + linordered_cancel_ab_semigroup_add +

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

  1480 begin

  1481

  1482 subclass linordered_semiring_strict

  1483 proof

  1484   fix a b c :: 'a

  1485   assume "a < b" "0 < c"

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

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

  1488 qed

  1489

  1490 subclass ordered_cancel_comm_semiring

  1491 proof

  1492   fix a b c :: 'a

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

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

  1495     unfolding le_less

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

  1497 qed

  1498

  1499 end

  1500

  1501 class ordered_ring = ring + ordered_cancel_semiring

  1502 begin

  1503

  1504 subclass ordered_ab_group_add ..

  1505

  1506 lemma less_add_iff1:

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

  1508 by (simp add: algebra_simps)

  1509

  1510 lemma less_add_iff2:

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

  1512 by (simp add: algebra_simps)

  1513

  1514 lemma le_add_iff1:

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

  1516 by (simp add: algebra_simps)

  1517

  1518 lemma le_add_iff2:

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

  1520 by (simp add: algebra_simps)

  1521

  1522 lemma mult_left_mono_neg:

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

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

  1525   apply simp_all

  1526   done

  1527

  1528 lemma mult_right_mono_neg:

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

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

  1531   apply simp_all

  1532   done

  1533

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

  1535 using mult_right_mono_neg [of a 0 b] by simp

  1536

  1537 lemma split_mult_pos_le:

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

  1539 by (auto simp add: mult_nonpos_nonpos)

  1540

  1541 end

  1542

  1543 class linordered_ring = ring + linordered_semiring + linordered_ab_group_add + abs_if

  1544 begin

  1545

  1546 subclass ordered_ring ..

  1547

  1548 subclass ordered_ab_group_add_abs

  1549 proof

  1550   fix a b

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

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

  1553 qed (auto simp add: abs_if)

  1554

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

  1556   using linear [of 0 a]

  1557   by (auto simp add: mult_nonpos_nonpos)

  1558

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

  1560   by (simp add: not_less)

  1561

  1562 proposition abs_eq_iff: "\<bar>x\<bar> = \<bar>y\<bar> \<longleftrightarrow> x = y \<or> x = -y"

  1563   by (auto simp add: abs_if split: split_if_asm)

  1564

  1565 end

  1566

  1567 class linordered_ring_strict = ring + linordered_semiring_strict

  1568   + ordered_ab_group_add + abs_if

  1569 begin

  1570

  1571 subclass linordered_ring ..

  1572

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

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

  1575

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

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

  1578

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

  1580 using mult_strict_right_mono_neg [of a 0 b] by simp

  1581

  1582 subclass ring_no_zero_divisors

  1583 proof

  1584   fix a b

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

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

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

  1588   proof (cases "a < 0")

  1589     case True note A' = this

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

  1591       case True with A'

  1592       show ?thesis by (auto dest: mult_neg_neg)

  1593     next

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

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

  1596     qed

  1597   next

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

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

  1600       case True with A'

  1601       show ?thesis by (auto dest: mult_strict_right_mono_neg)

  1602     next

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

  1604       with A' show ?thesis by auto

  1605     qed

  1606   qed

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

  1608 qed

  1609

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

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

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

  1613

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

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

  1616

  1617 lemma mult_less_0_iff:

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

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

  1620   apply force

  1621   done

  1622

  1623 lemma mult_le_0_iff:

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

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

  1626   apply force

  1627   done

  1628

  1629 text\<open>Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"},

  1630    also with the relations \<open>\<le>\<close> and equality.\<close>

  1631

  1632 text\<open>These disjunction'' versions produce two cases when the comparison is

  1633  an assumption, but effectively four when the comparison is a goal.\<close>

  1634

  1635 lemma mult_less_cancel_right_disj:

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

  1637   apply (cases "c = 0")

  1638   apply (auto simp add: neq_iff mult_strict_right_mono

  1639                       mult_strict_right_mono_neg)

  1640   apply (auto simp add: not_less

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

  1642                       not_le [symmetric, of a])

  1643   apply (erule_tac [!] notE)

  1644   apply (auto simp add: less_imp_le mult_right_mono

  1645                       mult_right_mono_neg)

  1646   done

  1647

  1648 lemma mult_less_cancel_left_disj:

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

  1650   apply (cases "c = 0")

  1651   apply (auto simp add: neq_iff mult_strict_left_mono

  1652                       mult_strict_left_mono_neg)

  1653   apply (auto simp add: not_less

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

  1655                       not_le [symmetric, of a])

  1656   apply (erule_tac [!] notE)

  1657   apply (auto simp add: less_imp_le mult_left_mono

  1658                       mult_left_mono_neg)

  1659   done

  1660

  1661 text\<open>The conjunction of implication'' lemmas produce two cases when the

  1662 comparison is a goal, but give four when the comparison is an assumption.\<close>

  1663

  1664 lemma mult_less_cancel_right:

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

  1666   using mult_less_cancel_right_disj [of a c b] by auto

  1667

  1668 lemma mult_less_cancel_left:

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

  1670   using mult_less_cancel_left_disj [of c a b] by auto

  1671

  1672 lemma mult_le_cancel_right:

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

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

  1675

  1676 lemma mult_le_cancel_left:

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

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

  1679

  1680 lemma mult_le_cancel_left_pos:

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

  1682 by (auto simp: mult_le_cancel_left)

  1683

  1684 lemma mult_le_cancel_left_neg:

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

  1686 by (auto simp: mult_le_cancel_left)

  1687

  1688 lemma mult_less_cancel_left_pos:

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

  1690 by (auto simp: mult_less_cancel_left)

  1691

  1692 lemma mult_less_cancel_left_neg:

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

  1694 by (auto simp: mult_less_cancel_left)

  1695

  1696 end

  1697

  1698 lemmas mult_sign_intros =

  1699   mult_nonneg_nonneg mult_nonneg_nonpos

  1700   mult_nonpos_nonneg mult_nonpos_nonpos

  1701   mult_pos_pos mult_pos_neg

  1702   mult_neg_pos mult_neg_neg

  1703

  1704 class ordered_comm_ring = comm_ring + ordered_comm_semiring

  1705 begin

  1706

  1707 subclass ordered_ring ..

  1708 subclass ordered_cancel_comm_semiring ..

  1709

  1710 end

  1711

  1712 class linordered_semidom = semidom + linordered_comm_semiring_strict +

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

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

  1715 begin

  1716

  1717 text \<open>Addition is the inverse of subtraction.\<close>

  1718

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

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

  1721

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

  1723   by simp

  1724

  1725 lemma add_le_imp_le_diff:

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

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

  1728   apply (frule le_add_diff_inverse2)

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

  1730   using add_implies_diff by fastforce

  1731

  1732 lemma add_le_add_imp_diff_le:

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

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

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

  1736 proof -

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

  1738     using a1 by simp

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

  1740     using a1 by (simp add: add_le_imp_le_diff)

  1741   ultimately show ?thesis

  1742     using a2

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

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

  1745     by (simp add: add.commute diff_diff_add)

  1746 qed

  1747

  1748 lemma pos_add_strict:

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

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

  1751

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

  1753 by (rule zero_less_one [THEN less_imp_le])

  1754

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

  1756 by (simp add: not_le)

  1757

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

  1759 by (simp add: not_less)

  1760

  1761 lemma less_1_mult:

  1762   assumes "1 < m" and "1 < n"

  1763   shows "1 < m * n"

  1764   using assms mult_strict_mono [of 1 m 1 n]

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

  1766

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

  1768   using mult_left_mono[of c 1 a] by simp

  1769

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

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

  1772

  1773 end

  1774

  1775 class linordered_idom = comm_ring_1 +

  1776   linordered_comm_semiring_strict + ordered_ab_group_add +

  1777   abs_if + sgn_if

  1778 begin

  1779

  1780 subclass linordered_semiring_1_strict ..

  1781 subclass linordered_ring_strict ..

  1782 subclass ordered_comm_ring ..

  1783 subclass idom ..

  1784

  1785 subclass linordered_semidom

  1786 proof

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

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

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

  1790     by simp

  1791 qed

  1792

  1793 lemma linorder_neqE_linordered_idom:

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

  1795   using assms by (rule neqE)

  1796

  1797 text \<open>These cancellation simprules also produce two cases when the comparison is a goal.\<close>

  1798

  1799 lemma mult_le_cancel_right1:

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

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

  1802

  1803 lemma mult_le_cancel_right2:

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

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

  1806

  1807 lemma mult_le_cancel_left1:

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

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

  1810

  1811 lemma mult_le_cancel_left2:

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

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

  1814

  1815 lemma mult_less_cancel_right1:

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

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

  1818

  1819 lemma mult_less_cancel_right2:

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

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

  1822

  1823 lemma mult_less_cancel_left1:

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

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

  1826

  1827 lemma mult_less_cancel_left2:

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

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

  1830

  1831 lemma sgn_sgn [simp]:

  1832   "sgn (sgn a) = sgn a"

  1833 unfolding sgn_if by simp

  1834

  1835 lemma sgn_0_0:

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

  1837 unfolding sgn_if by simp

  1838

  1839 lemma sgn_1_pos:

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

  1841 unfolding sgn_if by simp

  1842

  1843 lemma sgn_1_neg:

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

  1845 unfolding sgn_if by auto

  1846

  1847 lemma sgn_pos [simp]:

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

  1849 unfolding sgn_1_pos .

  1850

  1851 lemma sgn_neg [simp]:

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

  1853 unfolding sgn_1_neg .

  1854

  1855 lemma sgn_times:

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

  1857 by (auto simp add: sgn_if zero_less_mult_iff)

  1858

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

  1860 unfolding sgn_if abs_if by auto

  1861

  1862 lemma sgn_greater [simp]:

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

  1864   unfolding sgn_if by auto

  1865

  1866 lemma sgn_less [simp]:

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

  1868   unfolding sgn_if by auto

  1869

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

  1871   by (simp add: abs_if)

  1872

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

  1874   by (simp add: abs_if)

  1875

  1876 lemma dvd_if_abs_eq:

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

  1878 by(subst abs_dvd_iff[symmetric]) simp

  1879

  1880 text \<open>The following lemmas can be proven in more general structures, but

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

  1882 @{thm neg_less_pos}, @{thm neg_less_eq_nonneg}.\<close>

  1883

  1884 lemma equation_minus_iff_1 [simp, no_atp]:

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

  1886   by (fact equation_minus_iff)

  1887

  1888 lemma minus_equation_iff_1 [simp, no_atp]:

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

  1890   by (subst minus_equation_iff, auto)

  1891

  1892 lemma le_minus_iff_1 [simp, no_atp]:

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

  1894   by (fact le_minus_iff)

  1895

  1896 lemma minus_le_iff_1 [simp, no_atp]:

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

  1898   by (fact minus_le_iff)

  1899

  1900 lemma less_minus_iff_1 [simp, no_atp]:

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

  1902   by (fact less_minus_iff)

  1903

  1904 lemma minus_less_iff_1 [simp, no_atp]:

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

  1906   by (fact minus_less_iff)

  1907

  1908 end

  1909

  1910 text \<open>Simprules for comparisons where common factors can be cancelled.\<close>

  1911

  1912 lemmas mult_compare_simps =

  1913     mult_le_cancel_right mult_le_cancel_left

  1914     mult_le_cancel_right1 mult_le_cancel_right2

  1915     mult_le_cancel_left1 mult_le_cancel_left2

  1916     mult_less_cancel_right mult_less_cancel_left

  1917     mult_less_cancel_right1 mult_less_cancel_right2

  1918     mult_less_cancel_left1 mult_less_cancel_left2

  1919     mult_cancel_right mult_cancel_left

  1920     mult_cancel_right1 mult_cancel_right2

  1921     mult_cancel_left1 mult_cancel_left2

  1922

  1923 text \<open>Reasoning about inequalities with division\<close>

  1924

  1925 context linordered_semidom

  1926 begin

  1927

  1928 lemma less_add_one: "a < a + 1"

  1929 proof -

  1930   have "a + 0 < a + 1"

  1931     by (blast intro: zero_less_one add_strict_left_mono)

  1932   thus ?thesis by simp

  1933 qed

  1934

  1935 lemma zero_less_two: "0 < 1 + 1"

  1936 by (blast intro: less_trans zero_less_one less_add_one)

  1937

  1938 end

  1939

  1940 context linordered_idom

  1941 begin

  1942

  1943 lemma mult_right_le_one_le:

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

  1945   by (rule mult_left_le)

  1946

  1947 lemma mult_left_le_one_le:

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

  1949   by (auto simp add: mult_le_cancel_right2)

  1950

  1951 end

  1952

  1953 text \<open>Absolute Value\<close>

  1954

  1955 context linordered_idom

  1956 begin

  1957

  1958 lemma mult_sgn_abs:

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

  1960   unfolding abs_if sgn_if by auto

  1961

  1962 lemma abs_one [simp]:

  1963   "\<bar>1\<bar> = 1"

  1964   by (simp add: abs_if)

  1965

  1966 end

  1967

  1968 class ordered_ring_abs = ordered_ring + ordered_ab_group_add_abs +

  1969   assumes abs_eq_mult:

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

  1971

  1972 context linordered_idom

  1973 begin

  1974

  1975 subclass ordered_ring_abs proof

  1976 qed (auto simp add: abs_if not_less mult_less_0_iff)

  1977

  1978 lemma abs_mult:

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

  1980   by (rule abs_eq_mult) auto

  1981

  1982 lemma abs_mult_self [simp]:

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

  1984   by (simp add: abs_if)

  1985

  1986 lemma abs_mult_less:

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

  1988 proof -

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

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

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

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

  1993 qed

  1994

  1995 lemma abs_less_iff:

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

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

  1998

  1999 lemma abs_mult_pos:

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

  2001   by (simp add: abs_mult)

  2002

  2003 lemma abs_diff_less_iff:

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

  2005   by (auto simp add: diff_less_eq ac_simps abs_less_iff)

  2006

  2007 lemma abs_diff_le_iff:

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

  2009   by (auto simp add: diff_le_eq ac_simps abs_le_iff)

  2010

  2011 end

  2012

  2013 hide_fact (open) comm_mult_left_mono comm_mult_strict_left_mono distrib

  2014

  2015 code_identifier

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

  2017

  2018 end