src/HOL/Rings.thy
author wenzelm
Tue Sep 01 22:32:58 2015 +0200 (2015-09-01)
changeset 61076 bdc1e2f0a86a
parent 60867 86e7560e07d0
child 61649 268d88ec9087
permissions -rw-r--r--
eliminated \<Colon>;
     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 @{text combine_numerals} 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 -- \<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 @{text mult_nonpos_nonneg}\<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 @{text mult_neg_pos}\<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 end
  1563 
  1564 class linordered_ring_strict = ring + linordered_semiring_strict
  1565   + ordered_ab_group_add + abs_if
  1566 begin
  1567 
  1568 subclass linordered_ring ..
  1569 
  1570 lemma mult_strict_left_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> c * a < c * b"
  1571 using mult_strict_left_mono [of b a "- c"] by simp
  1572 
  1573 lemma mult_strict_right_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> a * c < b * c"
  1574 using mult_strict_right_mono [of b a "- c"] by simp
  1575 
  1576 lemma mult_neg_neg: "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> 0 < a * b"
  1577 using mult_strict_right_mono_neg [of a 0 b] by simp
  1578 
  1579 subclass ring_no_zero_divisors
  1580 proof
  1581   fix a b
  1582   assume "a \<noteq> 0" then have A: "a < 0 \<or> 0 < a" by (simp add: neq_iff)
  1583   assume "b \<noteq> 0" then have B: "b < 0 \<or> 0 < b" by (simp add: neq_iff)
  1584   have "a * b < 0 \<or> 0 < a * b"
  1585   proof (cases "a < 0")
  1586     case True note A' = this
  1587     show ?thesis proof (cases "b < 0")
  1588       case True with A'
  1589       show ?thesis by (auto dest: mult_neg_neg)
  1590     next
  1591       case False with B have "0 < b" by auto
  1592       with A' show ?thesis by (auto dest: mult_strict_right_mono)
  1593     qed
  1594   next
  1595     case False with A have A': "0 < a" by auto
  1596     show ?thesis proof (cases "b < 0")
  1597       case True with A'
  1598       show ?thesis by (auto dest: mult_strict_right_mono_neg)
  1599     next
  1600       case False with B have "0 < b" by auto
  1601       with A' show ?thesis by auto
  1602     qed
  1603   qed
  1604   then show "a * b \<noteq> 0" by (simp add: neq_iff)
  1605 qed
  1606 
  1607 lemma zero_less_mult_iff: "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0"
  1608   by (cases a 0 b 0 rule: linorder_cases[case_product linorder_cases])
  1609      (auto simp add: mult_neg_neg not_less le_less dest: zero_less_mult_pos zero_less_mult_pos2)
  1610 
  1611 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"
  1612   by (auto simp add: eq_commute [of 0] le_less not_less zero_less_mult_iff)
  1613 
  1614 lemma mult_less_0_iff:
  1615   "a * b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b"
  1616   apply (insert zero_less_mult_iff [of "-a" b])
  1617   apply force
  1618   done
  1619 
  1620 lemma mult_le_0_iff:
  1621   "a * b \<le> 0 \<longleftrightarrow> 0 \<le> a \<and> b \<le> 0 \<or> a \<le> 0 \<and> 0 \<le> b"
  1622   apply (insert zero_le_mult_iff [of "-a" b])
  1623   apply force
  1624   done
  1625 
  1626 text\<open>Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"},
  1627    also with the relations @{text "\<le>"} and equality.\<close>
  1628 
  1629 text\<open>These ``disjunction'' versions produce two cases when the comparison is
  1630  an assumption, but effectively four when the comparison is a goal.\<close>
  1631 
  1632 lemma mult_less_cancel_right_disj:
  1633   "a * c < b * c \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"
  1634   apply (cases "c = 0")
  1635   apply (auto simp add: neq_iff mult_strict_right_mono
  1636                       mult_strict_right_mono_neg)
  1637   apply (auto simp add: not_less
  1638                       not_le [symmetric, of "a*c"]
  1639                       not_le [symmetric, of a])
  1640   apply (erule_tac [!] notE)
  1641   apply (auto simp add: less_imp_le mult_right_mono
  1642                       mult_right_mono_neg)
  1643   done
  1644 
  1645 lemma mult_less_cancel_left_disj:
  1646   "c * a < c * b \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"
  1647   apply (cases "c = 0")
  1648   apply (auto simp add: neq_iff mult_strict_left_mono
  1649                       mult_strict_left_mono_neg)
  1650   apply (auto simp add: not_less
  1651                       not_le [symmetric, of "c*a"]
  1652                       not_le [symmetric, of a])
  1653   apply (erule_tac [!] notE)
  1654   apply (auto simp add: less_imp_le mult_left_mono
  1655                       mult_left_mono_neg)
  1656   done
  1657 
  1658 text\<open>The ``conjunction of implication'' lemmas produce two cases when the
  1659 comparison is a goal, but give four when the comparison is an assumption.\<close>
  1660 
  1661 lemma mult_less_cancel_right:
  1662   "a * c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)"
  1663   using mult_less_cancel_right_disj [of a c b] by auto
  1664 
  1665 lemma mult_less_cancel_left:
  1666   "c * a < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)"
  1667   using mult_less_cancel_left_disj [of c a b] by auto
  1668 
  1669 lemma mult_le_cancel_right:
  1670    "a * c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
  1671 by (simp add: not_less [symmetric] mult_less_cancel_right_disj)
  1672 
  1673 lemma mult_le_cancel_left:
  1674   "c * a \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
  1675 by (simp add: not_less [symmetric] mult_less_cancel_left_disj)
  1676 
  1677 lemma mult_le_cancel_left_pos:
  1678   "0 < c \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> a \<le> b"
  1679 by (auto simp: mult_le_cancel_left)
  1680 
  1681 lemma mult_le_cancel_left_neg:
  1682   "c < 0 \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> b \<le> a"
  1683 by (auto simp: mult_le_cancel_left)
  1684 
  1685 lemma mult_less_cancel_left_pos:
  1686   "0 < c \<Longrightarrow> c * a < c * b \<longleftrightarrow> a < b"
  1687 by (auto simp: mult_less_cancel_left)
  1688 
  1689 lemma mult_less_cancel_left_neg:
  1690   "c < 0 \<Longrightarrow> c * a < c * b \<longleftrightarrow> b < a"
  1691 by (auto simp: mult_less_cancel_left)
  1692 
  1693 end
  1694 
  1695 lemmas mult_sign_intros =
  1696   mult_nonneg_nonneg mult_nonneg_nonpos
  1697   mult_nonpos_nonneg mult_nonpos_nonpos
  1698   mult_pos_pos mult_pos_neg
  1699   mult_neg_pos mult_neg_neg
  1700 
  1701 class ordered_comm_ring = comm_ring + ordered_comm_semiring
  1702 begin
  1703 
  1704 subclass ordered_ring ..
  1705 subclass ordered_cancel_comm_semiring ..
  1706 
  1707 end
  1708 
  1709 class linordered_semidom = semidom + linordered_comm_semiring_strict +
  1710   assumes zero_less_one [simp]: "0 < 1"
  1711   assumes le_add_diff_inverse2 [simp]: "b \<le> a \<Longrightarrow> a - b + b = a"
  1712 begin
  1713 
  1714 text \<open>Addition is the inverse of subtraction.\<close>
  1715 
  1716 lemma le_add_diff_inverse [simp]: "b \<le> a \<Longrightarrow> b + (a - b) = a"
  1717   by (frule le_add_diff_inverse2) (simp add: add.commute)
  1718 
  1719 lemma add_diff_inverse: "~ a<b \<Longrightarrow> b + (a - b) = a"
  1720   by simp
  1721 
  1722 lemma add_le_imp_le_diff: 
  1723   shows "i + k \<le> n \<Longrightarrow> i \<le> n - k"
  1724   apply (subst add_le_cancel_right [where c=k, symmetric])
  1725   apply (frule le_add_diff_inverse2)
  1726   apply (simp only: add.assoc [symmetric])
  1727   using add_implies_diff by fastforce
  1728 
  1729 lemma add_le_add_imp_diff_le: 
  1730   assumes a1: "i + k \<le> n"
  1731       and a2: "n \<le> j + k"
  1732   shows "\<lbrakk>i + k \<le> n; n \<le> j + k\<rbrakk> \<Longrightarrow> n - k \<le> j"
  1733 proof -
  1734   have "n - (i + k) + (i + k) = n"
  1735     using a1 by simp
  1736   moreover have "n - k = n - k - i + i"
  1737     using a1 by (simp add: add_le_imp_le_diff)
  1738   ultimately show ?thesis
  1739     using a2
  1740     apply (simp add: add.assoc [symmetric])
  1741     apply (rule add_le_imp_le_diff [of _ k "j+k", simplified add_diff_cancel_right'])
  1742     by (simp add: add.commute diff_diff_add)
  1743 qed
  1744 
  1745 lemma pos_add_strict:
  1746   shows "0 < a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
  1747   using add_strict_mono [of 0 a b c] by simp
  1748 
  1749 lemma zero_le_one [simp]: "0 \<le> 1"
  1750 by (rule zero_less_one [THEN less_imp_le])
  1751 
  1752 lemma not_one_le_zero [simp]: "\<not> 1 \<le> 0"
  1753 by (simp add: not_le)
  1754 
  1755 lemma not_one_less_zero [simp]: "\<not> 1 < 0"
  1756 by (simp add: not_less)
  1757 
  1758 lemma less_1_mult:
  1759   assumes "1 < m" and "1 < n"
  1760   shows "1 < m * n"
  1761   using assms mult_strict_mono [of 1 m 1 n]
  1762     by (simp add:  less_trans [OF zero_less_one])
  1763 
  1764 lemma mult_left_le: "c \<le> 1 \<Longrightarrow> 0 \<le> a \<Longrightarrow> a * c \<le> a"
  1765   using mult_left_mono[of c 1 a] by simp
  1766 
  1767 lemma mult_le_one: "a \<le> 1 \<Longrightarrow> 0 \<le> b \<Longrightarrow> b \<le> 1 \<Longrightarrow> a * b \<le> 1"
  1768   using mult_mono[of a 1 b 1] by simp
  1769 
  1770 end
  1771 
  1772 class linordered_idom = comm_ring_1 +
  1773   linordered_comm_semiring_strict + ordered_ab_group_add +
  1774   abs_if + sgn_if
  1775 begin
  1776 
  1777 subclass linordered_semiring_1_strict ..
  1778 subclass linordered_ring_strict ..
  1779 subclass ordered_comm_ring ..
  1780 subclass idom ..
  1781 
  1782 subclass linordered_semidom
  1783 proof
  1784   have "0 \<le> 1 * 1" by (rule zero_le_square)
  1785   thus "0 < 1" by (simp add: le_less)
  1786   show "\<And>b a. b \<le> a \<Longrightarrow> a - b + b = a"
  1787     by simp
  1788 qed
  1789 
  1790 lemma linorder_neqE_linordered_idom:
  1791   assumes "x \<noteq> y" obtains "x < y" | "y < x"
  1792   using assms by (rule neqE)
  1793 
  1794 text \<open>These cancellation simprules also produce two cases when the comparison is a goal.\<close>
  1795 
  1796 lemma mult_le_cancel_right1:
  1797   "c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)"
  1798 by (insert mult_le_cancel_right [of 1 c b], simp)
  1799 
  1800 lemma mult_le_cancel_right2:
  1801   "a * c \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)"
  1802 by (insert mult_le_cancel_right [of a c 1], simp)
  1803 
  1804 lemma mult_le_cancel_left1:
  1805   "c \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)"
  1806 by (insert mult_le_cancel_left [of c 1 b], simp)
  1807 
  1808 lemma mult_le_cancel_left2:
  1809   "c * a \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)"
  1810 by (insert mult_le_cancel_left [of c a 1], simp)
  1811 
  1812 lemma mult_less_cancel_right1:
  1813   "c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)"
  1814 by (insert mult_less_cancel_right [of 1 c b], simp)
  1815 
  1816 lemma mult_less_cancel_right2:
  1817   "a * c < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"
  1818 by (insert mult_less_cancel_right [of a c 1], simp)
  1819 
  1820 lemma mult_less_cancel_left1:
  1821   "c < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)"
  1822 by (insert mult_less_cancel_left [of c 1 b], simp)
  1823 
  1824 lemma mult_less_cancel_left2:
  1825   "c * a < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"
  1826 by (insert mult_less_cancel_left [of c a 1], simp)
  1827 
  1828 lemma sgn_sgn [simp]:
  1829   "sgn (sgn a) = sgn a"
  1830 unfolding sgn_if by simp
  1831 
  1832 lemma sgn_0_0:
  1833   "sgn a = 0 \<longleftrightarrow> a = 0"
  1834 unfolding sgn_if by simp
  1835 
  1836 lemma sgn_1_pos:
  1837   "sgn a = 1 \<longleftrightarrow> a > 0"
  1838 unfolding sgn_if by simp
  1839 
  1840 lemma sgn_1_neg:
  1841   "sgn a = - 1 \<longleftrightarrow> a < 0"
  1842 unfolding sgn_if by auto
  1843 
  1844 lemma sgn_pos [simp]:
  1845   "0 < a \<Longrightarrow> sgn a = 1"
  1846 unfolding sgn_1_pos .
  1847 
  1848 lemma sgn_neg [simp]:
  1849   "a < 0 \<Longrightarrow> sgn a = - 1"
  1850 unfolding sgn_1_neg .
  1851 
  1852 lemma sgn_times:
  1853   "sgn (a * b) = sgn a * sgn b"
  1854 by (auto simp add: sgn_if zero_less_mult_iff)
  1855 
  1856 lemma abs_sgn: "\<bar>k\<bar> = k * sgn k"
  1857 unfolding sgn_if abs_if by auto
  1858 
  1859 lemma sgn_greater [simp]:
  1860   "0 < sgn a \<longleftrightarrow> 0 < a"
  1861   unfolding sgn_if by auto
  1862 
  1863 lemma sgn_less [simp]:
  1864   "sgn a < 0 \<longleftrightarrow> a < 0"
  1865   unfolding sgn_if by auto
  1866 
  1867 lemma abs_dvd_iff [simp]: "\<bar>m\<bar> dvd k \<longleftrightarrow> m dvd k"
  1868   by (simp add: abs_if)
  1869 
  1870 lemma dvd_abs_iff [simp]: "m dvd \<bar>k\<bar> \<longleftrightarrow> m dvd k"
  1871   by (simp add: abs_if)
  1872 
  1873 lemma dvd_if_abs_eq:
  1874   "\<bar>l\<bar> = \<bar>k\<bar> \<Longrightarrow> l dvd k"
  1875 by(subst abs_dvd_iff[symmetric]) simp
  1876 
  1877 text \<open>The following lemmas can be proven in more general structures, but
  1878 are dangerous as simp rules in absence of @{thm neg_equal_zero},
  1879 @{thm neg_less_pos}, @{thm neg_less_eq_nonneg}.\<close>
  1880 
  1881 lemma equation_minus_iff_1 [simp, no_atp]:
  1882   "1 = - a \<longleftrightarrow> a = - 1"
  1883   by (fact equation_minus_iff)
  1884 
  1885 lemma minus_equation_iff_1 [simp, no_atp]:
  1886   "- a = 1 \<longleftrightarrow> a = - 1"
  1887   by (subst minus_equation_iff, auto)
  1888 
  1889 lemma le_minus_iff_1 [simp, no_atp]:
  1890   "1 \<le> - b \<longleftrightarrow> b \<le> - 1"
  1891   by (fact le_minus_iff)
  1892 
  1893 lemma minus_le_iff_1 [simp, no_atp]:
  1894   "- a \<le> 1 \<longleftrightarrow> - 1 \<le> a"
  1895   by (fact minus_le_iff)
  1896 
  1897 lemma less_minus_iff_1 [simp, no_atp]:
  1898   "1 < - b \<longleftrightarrow> b < - 1"
  1899   by (fact less_minus_iff)
  1900 
  1901 lemma minus_less_iff_1 [simp, no_atp]:
  1902   "- a < 1 \<longleftrightarrow> - 1 < a"
  1903   by (fact minus_less_iff)
  1904 
  1905 end
  1906 
  1907 text \<open>Simprules for comparisons where common factors can be cancelled.\<close>
  1908 
  1909 lemmas mult_compare_simps =
  1910     mult_le_cancel_right mult_le_cancel_left
  1911     mult_le_cancel_right1 mult_le_cancel_right2
  1912     mult_le_cancel_left1 mult_le_cancel_left2
  1913     mult_less_cancel_right mult_less_cancel_left
  1914     mult_less_cancel_right1 mult_less_cancel_right2
  1915     mult_less_cancel_left1 mult_less_cancel_left2
  1916     mult_cancel_right mult_cancel_left
  1917     mult_cancel_right1 mult_cancel_right2
  1918     mult_cancel_left1 mult_cancel_left2
  1919 
  1920 text \<open>Reasoning about inequalities with division\<close>
  1921 
  1922 context linordered_semidom
  1923 begin
  1924 
  1925 lemma less_add_one: "a < a + 1"
  1926 proof -
  1927   have "a + 0 < a + 1"
  1928     by (blast intro: zero_less_one add_strict_left_mono)
  1929   thus ?thesis by simp
  1930 qed
  1931 
  1932 lemma zero_less_two: "0 < 1 + 1"
  1933 by (blast intro: less_trans zero_less_one less_add_one)
  1934 
  1935 end
  1936 
  1937 context linordered_idom
  1938 begin
  1939 
  1940 lemma mult_right_le_one_le:
  1941   "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> x * y \<le> x"
  1942   by (rule mult_left_le)
  1943 
  1944 lemma mult_left_le_one_le:
  1945   "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> y * x \<le> x"
  1946   by (auto simp add: mult_le_cancel_right2)
  1947 
  1948 end
  1949 
  1950 text \<open>Absolute Value\<close>
  1951 
  1952 context linordered_idom
  1953 begin
  1954 
  1955 lemma mult_sgn_abs:
  1956   "sgn x * \<bar>x\<bar> = x"
  1957   unfolding abs_if sgn_if by auto
  1958 
  1959 lemma abs_one [simp]:
  1960   "\<bar>1\<bar> = 1"
  1961   by (simp add: abs_if)
  1962 
  1963 end
  1964 
  1965 class ordered_ring_abs = ordered_ring + ordered_ab_group_add_abs +
  1966   assumes abs_eq_mult:
  1967     "(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>"
  1968 
  1969 context linordered_idom
  1970 begin
  1971 
  1972 subclass ordered_ring_abs proof
  1973 qed (auto simp add: abs_if not_less mult_less_0_iff)
  1974 
  1975 lemma abs_mult:
  1976   "\<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>"
  1977   by (rule abs_eq_mult) auto
  1978 
  1979 lemma abs_mult_self:
  1980   "\<bar>a\<bar> * \<bar>a\<bar> = a * a"
  1981   by (simp add: abs_if)
  1982 
  1983 lemma abs_mult_less:
  1984   "\<bar>a\<bar> < c \<Longrightarrow> \<bar>b\<bar> < d \<Longrightarrow> \<bar>a\<bar> * \<bar>b\<bar> < c * d"
  1985 proof -
  1986   assume ac: "\<bar>a\<bar> < c"
  1987   hence cpos: "0<c" by (blast intro: le_less_trans abs_ge_zero)
  1988   assume "\<bar>b\<bar> < d"
  1989   thus ?thesis by (simp add: ac cpos mult_strict_mono)
  1990 qed
  1991 
  1992 lemma abs_less_iff:
  1993   "\<bar>a\<bar> < b \<longleftrightarrow> a < b \<and> - a < b"
  1994   by (simp add: less_le abs_le_iff) (auto simp add: abs_if)
  1995 
  1996 lemma abs_mult_pos:
  1997   "0 \<le> x \<Longrightarrow> \<bar>y\<bar> * x = \<bar>y * x\<bar>"
  1998   by (simp add: abs_mult)
  1999 
  2000 lemma abs_diff_less_iff:
  2001   "\<bar>x - a\<bar> < r \<longleftrightarrow> a - r < x \<and> x < a + r"
  2002   by (auto simp add: diff_less_eq ac_simps abs_less_iff)
  2003 
  2004 lemma abs_diff_le_iff:
  2005    "\<bar>x - a\<bar> \<le> r \<longleftrightarrow> a - r \<le> x \<and> x \<le> a + r"
  2006   by (auto simp add: diff_le_eq ac_simps abs_le_iff)
  2007 
  2008 end
  2009 
  2010 hide_fact (open) comm_mult_left_mono comm_mult_strict_left_mono distrib
  2011 
  2012 code_identifier
  2013   code_module Rings \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
  2014 
  2015 end