src/HOL/Rings.thy
author haftmann
Wed Jul 08 14:01:41 2015 +0200 (2015-07-08)
changeset 60688 01488b559910
parent 60685 cb21b7022b00
child 60690 a9e45c9588c3
permissions -rw-r--r--
avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
     1 (*  Title:      HOL/Rings.thy
     2     Author:     Gertrud Bauer
     3     Author:     Steven Obua
     4     Author:     Tobias Nipkow
     5     Author:     Lawrence C Paulson
     6     Author:     Markus Wenzel
     7     Author:     Jeremy Avigad
     8 *)
     9 
    10 section {* Rings *}
    11 
    12 theory Rings
    13 imports Groups
    14 begin
    15 
    16 class semiring = ab_semigroup_add + semigroup_mult +
    17   assumes distrib_right[algebra_simps]: "(a + b) * c = a * c + b * c"
    18   assumes distrib_left[algebra_simps]: "a * (b + c) = a * b + a * c"
    19 begin
    20 
    21 text{*For the @{text combine_numerals} simproc*}
    22 lemma combine_common_factor:
    23   "a * e + (b * e + c) = (a + b) * e + c"
    24 by (simp add: distrib_right ac_simps)
    25 
    26 end
    27 
    28 class mult_zero = times + zero +
    29   assumes mult_zero_left [simp]: "0 * a = 0"
    30   assumes mult_zero_right [simp]: "a * 0 = 0"
    31 begin
    32 
    33 lemma mult_not_zero:
    34   "a * b \<noteq> 0 \<Longrightarrow> a \<noteq> 0 \<and> b \<noteq> 0"
    35   by auto
    36 
    37 end
    38 
    39 class semiring_0 = semiring + comm_monoid_add + mult_zero
    40 
    41 class semiring_0_cancel = semiring + cancel_comm_monoid_add
    42 begin
    43 
    44 subclass semiring_0
    45 proof
    46   fix a :: 'a
    47   have "0 * a + 0 * a = 0 * a + 0" by (simp add: distrib_right [symmetric])
    48   thus "0 * a = 0" by (simp only: add_left_cancel)
    49 next
    50   fix a :: 'a
    51   have "a * 0 + a * 0 = a * 0 + 0" by (simp add: distrib_left [symmetric])
    52   thus "a * 0 = 0" by (simp only: add_left_cancel)
    53 qed
    54 
    55 end
    56 
    57 class comm_semiring = ab_semigroup_add + ab_semigroup_mult +
    58   assumes distrib: "(a + b) * c = a * c + b * c"
    59 begin
    60 
    61 subclass semiring
    62 proof
    63   fix a b c :: 'a
    64   show "(a + b) * c = a * c + b * c" by (simp add: distrib)
    65   have "a * (b + c) = (b + c) * a" by (simp add: ac_simps)
    66   also have "... = b * a + c * a" by (simp only: distrib)
    67   also have "... = a * b + a * c" by (simp add: ac_simps)
    68   finally show "a * (b + c) = a * b + a * c" by blast
    69 qed
    70 
    71 end
    72 
    73 class comm_semiring_0 = comm_semiring + comm_monoid_add + mult_zero
    74 begin
    75 
    76 subclass semiring_0 ..
    77 
    78 end
    79 
    80 class comm_semiring_0_cancel = comm_semiring + cancel_comm_monoid_add
    81 begin
    82 
    83 subclass semiring_0_cancel ..
    84 
    85 subclass comm_semiring_0 ..
    86 
    87 end
    88 
    89 class zero_neq_one = zero + one +
    90   assumes zero_neq_one [simp]: "0 \<noteq> 1"
    91 begin
    92 
    93 lemma one_neq_zero [simp]: "1 \<noteq> 0"
    94 by (rule not_sym) (rule zero_neq_one)
    95 
    96 definition of_bool :: "bool \<Rightarrow> 'a"
    97 where
    98   "of_bool p = (if p then 1 else 0)"
    99 
   100 lemma of_bool_eq [simp, code]:
   101   "of_bool False = 0"
   102   "of_bool True = 1"
   103   by (simp_all add: of_bool_def)
   104 
   105 lemma of_bool_eq_iff:
   106   "of_bool p = of_bool q \<longleftrightarrow> p = q"
   107   by (simp add: of_bool_def)
   108 
   109 lemma split_of_bool [split]:
   110   "P (of_bool p) \<longleftrightarrow> (p \<longrightarrow> P 1) \<and> (\<not> p \<longrightarrow> P 0)"
   111   by (cases p) simp_all
   112 
   113 lemma split_of_bool_asm:
   114   "P (of_bool p) \<longleftrightarrow> \<not> (p \<and> \<not> P 1 \<or> \<not> p \<and> \<not> P 0)"
   115   by (cases p) simp_all
   116 
   117 end
   118 
   119 class semiring_1 = zero_neq_one + semiring_0 + monoid_mult
   120 
   121 text {* Abstract divisibility *}
   122 
   123 class dvd = times
   124 begin
   125 
   126 definition dvd :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "dvd" 50) where
   127   "b dvd a \<longleftrightarrow> (\<exists>k. a = b * k)"
   128 
   129 lemma dvdI [intro?]: "a = b * k \<Longrightarrow> b dvd a"
   130   unfolding dvd_def ..
   131 
   132 lemma dvdE [elim?]: "b dvd a \<Longrightarrow> (\<And>k. a = b * k \<Longrightarrow> P) \<Longrightarrow> P"
   133   unfolding dvd_def by blast
   134 
   135 end
   136 
   137 context comm_monoid_mult
   138 begin
   139 
   140 subclass dvd .
   141 
   142 lemma dvd_refl [simp]:
   143   "a dvd a"
   144 proof
   145   show "a = a * 1" by simp
   146 qed
   147 
   148 lemma dvd_trans:
   149   assumes "a dvd b" and "b dvd c"
   150   shows "a dvd c"
   151 proof -
   152   from assms obtain v where "b = a * v" by (auto elim!: dvdE)
   153   moreover from assms obtain w where "c = b * w" by (auto elim!: dvdE)
   154   ultimately have "c = a * (v * w)" by (simp add: mult.assoc)
   155   then show ?thesis ..
   156 qed
   157 
   158 lemma one_dvd [simp]:
   159   "1 dvd a"
   160   by (auto intro!: dvdI)
   161 
   162 lemma dvd_mult [simp]:
   163   "a dvd c \<Longrightarrow> a dvd (b * c)"
   164   by (auto intro!: mult.left_commute dvdI elim!: dvdE)
   165 
   166 lemma dvd_mult2 [simp]:
   167   "a dvd b \<Longrightarrow> a dvd (b * c)"
   168   using dvd_mult [of a b c] by (simp add: ac_simps)
   169 
   170 lemma dvd_triv_right [simp]:
   171   "a dvd b * a"
   172   by (rule dvd_mult) (rule dvd_refl)
   173 
   174 lemma dvd_triv_left [simp]:
   175   "a dvd a * b"
   176   by (rule dvd_mult2) (rule dvd_refl)
   177 
   178 lemma mult_dvd_mono:
   179   assumes "a dvd b"
   180     and "c dvd d"
   181   shows "a * c dvd b * d"
   182 proof -
   183   from `a dvd b` obtain b' where "b = a * b'" ..
   184   moreover from `c dvd d` obtain d' where "d = c * d'" ..
   185   ultimately have "b * d = (a * c) * (b' * d')" by (simp add: ac_simps)
   186   then show ?thesis ..
   187 qed
   188 
   189 lemma dvd_mult_left:
   190   "a * b dvd c \<Longrightarrow> a dvd c"
   191   by (simp add: dvd_def mult.assoc) blast
   192 
   193 lemma dvd_mult_right:
   194   "a * b dvd c \<Longrightarrow> b dvd c"
   195   using dvd_mult_left [of b a c] by (simp add: ac_simps)
   196 
   197 end
   198 
   199 class comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult
   200 begin
   201 
   202 subclass semiring_1 ..
   203 
   204 lemma dvd_0_left_iff [simp]:
   205   "0 dvd a \<longleftrightarrow> a = 0"
   206   by (auto intro: dvd_refl elim!: dvdE)
   207 
   208 lemma dvd_0_right [iff]:
   209   "a dvd 0"
   210 proof
   211   show "0 = a * 0" by simp
   212 qed
   213 
   214 lemma dvd_0_left:
   215   "0 dvd a \<Longrightarrow> a = 0"
   216   by simp
   217 
   218 lemma dvd_add [simp]:
   219   assumes "a dvd b" and "a dvd c"
   220   shows "a dvd (b + c)"
   221 proof -
   222   from `a dvd b` obtain b' where "b = a * b'" ..
   223   moreover from `a dvd c` obtain c' where "c = a * c'" ..
   224   ultimately have "b + c = a * (b' + c')" by (simp add: distrib_left)
   225   then show ?thesis ..
   226 qed
   227 
   228 end
   229 
   230 class semiring_1_cancel = semiring + cancel_comm_monoid_add
   231   + zero_neq_one + monoid_mult
   232 begin
   233 
   234 subclass semiring_0_cancel ..
   235 
   236 subclass semiring_1 ..
   237 
   238 end
   239 
   240 class comm_semiring_1_cancel = comm_semiring + cancel_comm_monoid_add +
   241                                zero_neq_one + comm_monoid_mult +
   242   assumes right_diff_distrib' [algebra_simps]: "a * (b - c) = a * b - a * c"
   243 begin
   244 
   245 subclass semiring_1_cancel ..
   246 subclass comm_semiring_0_cancel ..
   247 subclass comm_semiring_1 ..
   248 
   249 lemma left_diff_distrib' [algebra_simps]:
   250   "(b - c) * a = b * a - c * a"
   251   by (simp add: algebra_simps)
   252 
   253 lemma dvd_add_times_triv_left_iff [simp]:
   254   "a dvd c * a + b \<longleftrightarrow> a dvd b"
   255 proof -
   256   have "a dvd a * c + b \<longleftrightarrow> a dvd b" (is "?P \<longleftrightarrow> ?Q")
   257   proof
   258     assume ?Q then show ?P by simp
   259   next
   260     assume ?P
   261     then obtain d where "a * c + b = a * d" ..
   262     then have "a * c + b - a * c = a * d - a * c" by simp
   263     then have "b = a * d - a * c" by simp
   264     then have "b = a * (d - c)" by (simp add: algebra_simps)
   265     then show ?Q ..
   266   qed
   267   then show "a dvd c * a + b \<longleftrightarrow> a dvd b" by (simp add: ac_simps)
   268 qed
   269 
   270 lemma dvd_add_times_triv_right_iff [simp]:
   271   "a dvd b + c * a \<longleftrightarrow> a dvd b"
   272   using dvd_add_times_triv_left_iff [of a c b] by (simp add: ac_simps)
   273 
   274 lemma dvd_add_triv_left_iff [simp]:
   275   "a dvd a + b \<longleftrightarrow> a dvd b"
   276   using dvd_add_times_triv_left_iff [of a 1 b] by simp
   277 
   278 lemma dvd_add_triv_right_iff [simp]:
   279   "a dvd b + a \<longleftrightarrow> a dvd b"
   280   using dvd_add_times_triv_right_iff [of a b 1] by simp
   281 
   282 lemma dvd_add_right_iff:
   283   assumes "a dvd b"
   284   shows "a dvd b + c \<longleftrightarrow> a dvd c" (is "?P \<longleftrightarrow> ?Q")
   285 proof
   286   assume ?P then obtain d where "b + c = a * d" ..
   287   moreover from `a dvd b` obtain e where "b = a * e" ..
   288   ultimately have "a * e + c = a * d" by simp
   289   then have "a * e + c - a * e = a * d - a * e" by simp
   290   then have "c = a * d - a * e" by simp
   291   then have "c = a * (d - e)" by (simp add: algebra_simps)
   292   then show ?Q ..
   293 next
   294   assume ?Q with assms show ?P by simp
   295 qed
   296 
   297 lemma dvd_add_left_iff:
   298   assumes "a dvd c"
   299   shows "a dvd b + c \<longleftrightarrow> a dvd b"
   300   using assms dvd_add_right_iff [of a c b] by (simp add: ac_simps)
   301 
   302 end
   303 
   304 class ring = semiring + ab_group_add
   305 begin
   306 
   307 subclass semiring_0_cancel ..
   308 
   309 text {* Distribution rules *}
   310 
   311 lemma minus_mult_left: "- (a * b) = - a * b"
   312 by (rule minus_unique) (simp add: distrib_right [symmetric])
   313 
   314 lemma minus_mult_right: "- (a * b) = a * - b"
   315 by (rule minus_unique) (simp add: distrib_left [symmetric])
   316 
   317 text{*Extract signs from products*}
   318 lemmas mult_minus_left [simp] = minus_mult_left [symmetric]
   319 lemmas mult_minus_right [simp] = minus_mult_right [symmetric]
   320 
   321 lemma minus_mult_minus [simp]: "- a * - b = a * b"
   322 by simp
   323 
   324 lemma minus_mult_commute: "- a * b = a * - b"
   325 by simp
   326 
   327 lemma right_diff_distrib [algebra_simps]:
   328   "a * (b - c) = a * b - a * c"
   329   using distrib_left [of a b "-c "] by simp
   330 
   331 lemma left_diff_distrib [algebra_simps]:
   332   "(a - b) * c = a * c - b * c"
   333   using distrib_right [of a "- b" c] by simp
   334 
   335 lemmas ring_distribs =
   336   distrib_left distrib_right left_diff_distrib right_diff_distrib
   337 
   338 lemma eq_add_iff1:
   339   "a * e + c = b * e + d \<longleftrightarrow> (a - b) * e + c = d"
   340 by (simp add: algebra_simps)
   341 
   342 lemma eq_add_iff2:
   343   "a * e + c = b * e + d \<longleftrightarrow> c = (b - a) * e + d"
   344 by (simp add: algebra_simps)
   345 
   346 end
   347 
   348 lemmas ring_distribs =
   349   distrib_left distrib_right left_diff_distrib right_diff_distrib
   350 
   351 class comm_ring = comm_semiring + ab_group_add
   352 begin
   353 
   354 subclass ring ..
   355 subclass comm_semiring_0_cancel ..
   356 
   357 lemma square_diff_square_factored:
   358   "x * x - y * y = (x + y) * (x - y)"
   359   by (simp add: algebra_simps)
   360 
   361 end
   362 
   363 class ring_1 = ring + zero_neq_one + monoid_mult
   364 begin
   365 
   366 subclass semiring_1_cancel ..
   367 
   368 lemma square_diff_one_factored:
   369   "x * x - 1 = (x + 1) * (x - 1)"
   370   by (simp add: algebra_simps)
   371 
   372 end
   373 
   374 class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult
   375 begin
   376 
   377 subclass ring_1 ..
   378 subclass comm_semiring_1_cancel
   379   by unfold_locales (simp add: algebra_simps)
   380 
   381 lemma dvd_minus_iff [simp]: "x dvd - y \<longleftrightarrow> x dvd y"
   382 proof
   383   assume "x dvd - y"
   384   then have "x dvd - 1 * - y" by (rule dvd_mult)
   385   then show "x dvd y" by simp
   386 next
   387   assume "x dvd y"
   388   then have "x dvd - 1 * y" by (rule dvd_mult)
   389   then show "x dvd - y" by simp
   390 qed
   391 
   392 lemma minus_dvd_iff [simp]: "- x dvd y \<longleftrightarrow> x dvd y"
   393 proof
   394   assume "- x dvd y"
   395   then obtain k where "y = - x * k" ..
   396   then have "y = x * - k" by simp
   397   then show "x dvd y" ..
   398 next
   399   assume "x dvd y"
   400   then obtain k where "y = x * k" ..
   401   then have "y = - x * - k" by simp
   402   then show "- x dvd y" ..
   403 qed
   404 
   405 lemma dvd_diff [simp]:
   406   "x dvd y \<Longrightarrow> x dvd z \<Longrightarrow> x dvd (y - z)"
   407   using dvd_add [of x y "- z"] by simp
   408 
   409 end
   410 
   411 class semiring_no_zero_divisors = semiring_0 +
   412   assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
   413 begin
   414 
   415 lemma divisors_zero:
   416   assumes "a * b = 0"
   417   shows "a = 0 \<or> b = 0"
   418 proof (rule classical)
   419   assume "\<not> (a = 0 \<or> b = 0)"
   420   then have "a \<noteq> 0" and "b \<noteq> 0" by auto
   421   with no_zero_divisors have "a * b \<noteq> 0" by blast
   422   with assms show ?thesis by simp
   423 qed
   424 
   425 lemma mult_eq_0_iff [simp]:
   426   shows "a * b = 0 \<longleftrightarrow> a = 0 \<or> b = 0"
   427 proof (cases "a = 0 \<or> b = 0")
   428   case False then have "a \<noteq> 0" and "b \<noteq> 0" by auto
   429     then show ?thesis using no_zero_divisors by simp
   430 next
   431   case True then show ?thesis by auto
   432 qed
   433 
   434 end
   435 
   436 class semiring_no_zero_divisors_cancel = semiring_no_zero_divisors +
   437   assumes mult_cancel_right [simp]: "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b"
   438     and mult_cancel_left [simp]: "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b"
   439 begin
   440 
   441 lemma mult_left_cancel:
   442   "c \<noteq> 0 \<Longrightarrow> c * a = c * b \<longleftrightarrow> a = b"
   443   by simp
   444 
   445 lemma mult_right_cancel:
   446   "c \<noteq> 0 \<Longrightarrow> a * c = b * c \<longleftrightarrow> a = b"
   447   by simp
   448 
   449 end
   450 
   451 class ring_no_zero_divisors = ring + semiring_no_zero_divisors
   452 begin
   453 
   454 subclass semiring_no_zero_divisors_cancel
   455 proof
   456   fix a b c
   457   have "a * c = b * c \<longleftrightarrow> (a - b) * c = 0"
   458     by (simp add: algebra_simps)
   459   also have "\<dots> \<longleftrightarrow> c = 0 \<or> a = b"
   460     by auto
   461   finally show "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b" .
   462   have "c * a = c * b \<longleftrightarrow> c * (a - b) = 0"
   463     by (simp add: algebra_simps)
   464   also have "\<dots> \<longleftrightarrow> c = 0 \<or> a = b"
   465     by auto
   466   finally show "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b" .
   467 qed
   468 
   469 end
   470 
   471 class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors
   472 begin
   473 
   474 lemma square_eq_1_iff:
   475   "x * x = 1 \<longleftrightarrow> x = 1 \<or> x = - 1"
   476 proof -
   477   have "(x - 1) * (x + 1) = x * x - 1"
   478     by (simp add: algebra_simps)
   479   hence "x * x = 1 \<longleftrightarrow> (x - 1) * (x + 1) = 0"
   480     by simp
   481   thus ?thesis
   482     by (simp add: eq_neg_iff_add_eq_0)
   483 qed
   484 
   485 lemma mult_cancel_right1 [simp]:
   486   "c = b * c \<longleftrightarrow> c = 0 \<or> b = 1"
   487 by (insert mult_cancel_right [of 1 c b], force)
   488 
   489 lemma mult_cancel_right2 [simp]:
   490   "a * c = c \<longleftrightarrow> c = 0 \<or> a = 1"
   491 by (insert mult_cancel_right [of a c 1], simp)
   492 
   493 lemma mult_cancel_left1 [simp]:
   494   "c = c * b \<longleftrightarrow> c = 0 \<or> b = 1"
   495 by (insert mult_cancel_left [of c 1 b], force)
   496 
   497 lemma mult_cancel_left2 [simp]:
   498   "c * a = c \<longleftrightarrow> c = 0 \<or> a = 1"
   499 by (insert mult_cancel_left [of c a 1], simp)
   500 
   501 end
   502 
   503 class semidom = comm_semiring_1_cancel + semiring_no_zero_divisors
   504 
   505 class idom = comm_ring_1 + semiring_no_zero_divisors
   506 begin
   507 
   508 subclass semidom ..
   509 
   510 subclass ring_1_no_zero_divisors ..
   511 
   512 lemma dvd_mult_cancel_right [simp]:
   513   "a * c dvd b * c \<longleftrightarrow> c = 0 \<or> a dvd b"
   514 proof -
   515   have "a * c dvd b * c \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)"
   516     unfolding dvd_def by (simp add: ac_simps)
   517   also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b"
   518     unfolding dvd_def by simp
   519   finally show ?thesis .
   520 qed
   521 
   522 lemma dvd_mult_cancel_left [simp]:
   523   "c * a dvd c * b \<longleftrightarrow> c = 0 \<or> a dvd b"
   524 proof -
   525   have "c * a dvd c * b \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)"
   526     unfolding dvd_def by (simp add: ac_simps)
   527   also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b"
   528     unfolding dvd_def by simp
   529   finally show ?thesis .
   530 qed
   531 
   532 lemma square_eq_iff: "a * a = b * b \<longleftrightarrow> a = b \<or> a = - b"
   533 proof
   534   assume "a * a = b * b"
   535   then have "(a - b) * (a + b) = 0"
   536     by (simp add: algebra_simps)
   537   then show "a = b \<or> a = - b"
   538     by (simp add: eq_neg_iff_add_eq_0)
   539 next
   540   assume "a = b \<or> a = - b"
   541   then show "a * a = b * b" by auto
   542 qed
   543 
   544 end
   545 
   546 text {*
   547   The theory of partially ordered rings is taken from the books:
   548   \begin{itemize}
   549   \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979
   550   \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963
   551   \end{itemize}
   552   Most of the used notions can also be looked up in
   553   \begin{itemize}
   554   \item @{url "http://www.mathworld.com"} by Eric Weisstein et. al.
   555   \item \emph{Algebra I} by van der Waerden, Springer.
   556   \end{itemize}
   557 *}
   558 
   559 class divide =
   560   fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "div" 70)
   561 
   562 setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
   563 
   564 context semiring
   565 begin
   566 
   567 lemma [field_simps]:
   568   shows distrib_left_NO_MATCH: "NO_MATCH (x div y) a \<Longrightarrow> a * (b + c) = a * b + a * c"
   569     and distrib_right_NO_MATCH: "NO_MATCH (x div y) c \<Longrightarrow> (a + b) * c = a * c + b * c"
   570   by (rule distrib_left distrib_right)+
   571 
   572 end
   573 
   574 context ring
   575 begin
   576 
   577 lemma [field_simps]:
   578   shows left_diff_distrib_NO_MATCH: "NO_MATCH (x div y) c \<Longrightarrow> (a - b) * c = a * c - b * c"
   579     and right_diff_distrib_NO_MATCH: "NO_MATCH (x div y) a \<Longrightarrow> a * (b - c) = a * b - a * c"
   580   by (rule left_diff_distrib right_diff_distrib)+
   581 
   582 end
   583 
   584 setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a::divide \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
   585 
   586 class semidom_divide = semidom + divide +
   587   assumes nonzero_mult_divide_cancel_right [simp]: "b \<noteq> 0 \<Longrightarrow> (a * b) div b = a"
   588   assumes divide_zero [simp]: "a div 0 = 0"
   589 begin
   590 
   591 lemma nonzero_mult_divide_cancel_left [simp]:
   592   "a \<noteq> 0 \<Longrightarrow> (a * b) div a = b"
   593   using nonzero_mult_divide_cancel_right [of a b] by (simp add: ac_simps)
   594 
   595 subclass semiring_no_zero_divisors_cancel
   596 proof
   597   fix a b c
   598   { fix a b c
   599     show "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b"
   600     proof (cases "c = 0")
   601       case True then show ?thesis by simp
   602     next
   603       case False
   604       { assume "a * c = b * c"
   605         then have "a * c div c = b * c div c"
   606           by simp
   607         with False have "a = b"
   608           by simp
   609       } then show ?thesis by auto
   610     qed
   611   }
   612   from this [of a c b]
   613   show "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b"
   614     by (simp add: ac_simps)
   615 qed
   616 
   617 lemma div_self [simp]:
   618   assumes "a \<noteq> 0"
   619   shows "a div a = 1"
   620   using assms nonzero_mult_divide_cancel_left [of a 1] by simp
   621 
   622 lemma divide_zero_left [simp]:
   623   "0 div a = 0"
   624 proof (cases "a = 0")
   625   case True then show ?thesis by simp
   626 next
   627   case False then have "a * 0 div a = 0"
   628     by (rule nonzero_mult_divide_cancel_left)
   629   then show ?thesis by simp
   630 qed 
   631 
   632 end
   633 
   634 class idom_divide = idom + semidom_divide
   635 
   636 class algebraic_semidom = semidom_divide
   637 begin
   638 
   639 text \<open>
   640   Class @{class algebraic_semidom} enriches a integral domain
   641   by notions from algebra, like units in a ring.
   642   It is a separate class to avoid spoiling fields with notions
   643   which are degenerated there.
   644 \<close>
   645 
   646 lemma dvd_div_mult_self [simp]:
   647   "a dvd b \<Longrightarrow> b div a * a = b"
   648   by (cases "a = 0") (auto elim: dvdE simp add: ac_simps)
   649 
   650 lemma dvd_mult_div_cancel [simp]:
   651   "a dvd b \<Longrightarrow> a * (b div a) = b"
   652   using dvd_div_mult_self [of a b] by (simp add: ac_simps)
   653 
   654 lemma div_mult_swap:
   655   assumes "c dvd b"
   656   shows "a * (b div c) = (a * b) div c"
   657 proof (cases "c = 0")
   658   case True then show ?thesis by simp
   659 next
   660   case False from assms obtain d where "b = c * d" ..
   661   moreover from False have "a * divide (d * c) c = ((a * d) * c) div c"
   662     by simp
   663   ultimately show ?thesis by (simp add: ac_simps)
   664 qed
   665 
   666 lemma dvd_div_mult:
   667   assumes "c dvd b"
   668   shows "b div c * a = (b * a) div c"
   669   using assms div_mult_swap [of c b a] by (simp add: ac_simps)
   670 
   671 lemma dvd_div_mult2_eq:
   672   assumes "b * c dvd a"
   673   shows "a div (b * c) = a div b div c"
   674 using assms proof
   675   fix k
   676   assume "a = b * c * k"
   677   then show ?thesis
   678     by (cases "b = 0 \<or> c = 0") (auto, simp add: ac_simps)
   679 qed
   680 
   681 
   682 text \<open>Units: invertible elements in a ring\<close>
   683 
   684 abbreviation is_unit :: "'a \<Rightarrow> bool"
   685 where
   686   "is_unit a \<equiv> a dvd 1"
   687 
   688 lemma not_is_unit_0 [simp]:
   689   "\<not> is_unit 0"
   690   by simp
   691 
   692 lemma unit_imp_dvd [dest]:
   693   "is_unit b \<Longrightarrow> b dvd a"
   694   by (rule dvd_trans [of _ 1]) simp_all
   695 
   696 lemma unit_dvdE:
   697   assumes "is_unit a"
   698   obtains c where "a \<noteq> 0" and "b = a * c"
   699 proof -
   700   from assms have "a dvd b" by auto
   701   then obtain c where "b = a * c" ..
   702   moreover from assms have "a \<noteq> 0" by auto
   703   ultimately show thesis using that by blast
   704 qed
   705 
   706 lemma dvd_unit_imp_unit:
   707   "a dvd b \<Longrightarrow> is_unit b \<Longrightarrow> is_unit a"
   708   by (rule dvd_trans)
   709 
   710 lemma unit_div_1_unit [simp, intro]:
   711   assumes "is_unit a"
   712   shows "is_unit (1 div a)"
   713 proof -
   714   from assms have "1 = 1 div a * a" by simp
   715   then show "is_unit (1 div a)" by (rule dvdI)
   716 qed
   717 
   718 lemma is_unitE [elim?]:
   719   assumes "is_unit a"
   720   obtains b where "a \<noteq> 0" and "b \<noteq> 0"
   721     and "is_unit b" and "1 div a = b" and "1 div b = a"
   722     and "a * b = 1" and "c div a = c * b"
   723 proof (rule that)
   724   def b \<equiv> "1 div a"
   725   then show "1 div a = b" by simp
   726   from b_def `is_unit a` show "is_unit b" by simp
   727   from `is_unit a` and `is_unit b` show "a \<noteq> 0" and "b \<noteq> 0" by auto
   728   from b_def `is_unit a` show "a * b = 1" by simp
   729   then have "1 = a * b" ..
   730   with b_def `b \<noteq> 0` show "1 div b = a" by simp
   731   from `is_unit a` have "a dvd c" ..
   732   then obtain d where "c = a * d" ..
   733   with `a \<noteq> 0` `a * b = 1` show "c div a = c * b"
   734     by (simp add: mult.assoc mult.left_commute [of a])
   735 qed
   736 
   737 lemma unit_prod [intro]:
   738   "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a * b)"
   739   by (subst mult_1_left [of 1, symmetric]) (rule mult_dvd_mono)
   740 
   741 lemma unit_div [intro]:
   742   "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a div b)"
   743   by (erule is_unitE [of b a]) (simp add: ac_simps unit_prod)
   744 
   745 lemma mult_unit_dvd_iff:
   746   assumes "is_unit b"
   747   shows "a * b dvd c \<longleftrightarrow> a dvd c"
   748 proof
   749   assume "a * b dvd c"
   750   with assms show "a dvd c"
   751     by (simp add: dvd_mult_left)
   752 next
   753   assume "a dvd c"
   754   then obtain k where "c = a * k" ..
   755   with assms have "c = (a * b) * (1 div b * k)"
   756     by (simp add: mult_ac)
   757   then show "a * b dvd c" by (rule dvdI)
   758 qed
   759 
   760 lemma dvd_mult_unit_iff:
   761   assumes "is_unit b"
   762   shows "a dvd c * b \<longleftrightarrow> a dvd c"
   763 proof
   764   assume "a dvd c * b"
   765   with assms have "c * b dvd c * (b * (1 div b))"
   766     by (subst mult_assoc [symmetric]) simp
   767   also from `is_unit b` have "b * (1 div b) = 1" by (rule is_unitE) simp
   768   finally have "c * b dvd c" by simp
   769   with `a dvd c * b` show "a dvd c" by (rule dvd_trans)
   770 next
   771   assume "a dvd c"
   772   then show "a dvd c * b" by simp
   773 qed
   774 
   775 lemma div_unit_dvd_iff:
   776   "is_unit b \<Longrightarrow> a div b dvd c \<longleftrightarrow> a dvd c"
   777   by (erule is_unitE [of _ a]) (auto simp add: mult_unit_dvd_iff)
   778 
   779 lemma dvd_div_unit_iff:
   780   "is_unit b \<Longrightarrow> a dvd c div b \<longleftrightarrow> a dvd c"
   781   by (erule is_unitE [of _ c]) (simp add: dvd_mult_unit_iff)
   782 
   783 lemmas unit_dvd_iff = mult_unit_dvd_iff div_unit_dvd_iff
   784   dvd_mult_unit_iff dvd_div_unit_iff -- \<open>FIXME consider fact collection\<close>
   785 
   786 lemma unit_mult_div_div [simp]:
   787   "is_unit a \<Longrightarrow> b * (1 div a) = b div a"
   788   by (erule is_unitE [of _ b]) simp
   789 
   790 lemma unit_div_mult_self [simp]:
   791   "is_unit a \<Longrightarrow> b div a * a = b"
   792   by (rule dvd_div_mult_self) auto
   793 
   794 lemma unit_div_1_div_1 [simp]:
   795   "is_unit a \<Longrightarrow> 1 div (1 div a) = a"
   796   by (erule is_unitE) simp
   797 
   798 lemma unit_div_mult_swap:
   799   "is_unit c \<Longrightarrow> a * (b div c) = (a * b) div c"
   800   by (erule unit_dvdE [of _ b]) (simp add: mult.left_commute [of _ c])
   801 
   802 lemma unit_div_commute:
   803   "is_unit b \<Longrightarrow> (a div b) * c = (a * c) div b"
   804   using unit_div_mult_swap [of b c a] by (simp add: ac_simps)
   805 
   806 lemma unit_eq_div1:
   807   "is_unit b \<Longrightarrow> a div b = c \<longleftrightarrow> a = c * b"
   808   by (auto elim: is_unitE)
   809 
   810 lemma unit_eq_div2:
   811   "is_unit b \<Longrightarrow> a = c div b \<longleftrightarrow> a * b = c"
   812   using unit_eq_div1 [of b c a] by auto
   813 
   814 lemma unit_mult_left_cancel:
   815   assumes "is_unit a"
   816   shows "a * b = a * c \<longleftrightarrow> b = c" (is "?P \<longleftrightarrow> ?Q")
   817   using assms mult_cancel_left [of a b c] by auto
   818 
   819 lemma unit_mult_right_cancel:
   820   "is_unit a \<Longrightarrow> b * a = c * a \<longleftrightarrow> b = c"
   821   using unit_mult_left_cancel [of a b c] by (auto simp add: ac_simps)
   822 
   823 lemma unit_div_cancel:
   824   assumes "is_unit a"
   825   shows "b div a = c div a \<longleftrightarrow> b = c"
   826 proof -
   827   from assms have "is_unit (1 div a)" by simp
   828   then have "b * (1 div a) = c * (1 div a) \<longleftrightarrow> b = c"
   829     by (rule unit_mult_right_cancel)
   830   with assms show ?thesis by simp
   831 qed
   832 
   833 lemma is_unit_div_mult2_eq:
   834   assumes "is_unit b" and "is_unit c"
   835   shows "a div (b * c) = a div b div c"
   836 proof -
   837   from assms have "is_unit (b * c)" by (simp add: unit_prod)
   838   then have "b * c dvd a"
   839     by (rule unit_imp_dvd)
   840   then show ?thesis
   841     by (rule dvd_div_mult2_eq)
   842 qed
   843 
   844 lemmas unit_simps = mult_unit_dvd_iff div_unit_dvd_iff dvd_mult_unit_iff
   845   dvd_div_unit_iff unit_div_mult_swap unit_div_commute
   846   unit_mult_left_cancel unit_mult_right_cancel unit_div_cancel
   847   unit_eq_div1 unit_eq_div2
   848 
   849 lemma is_unit_divide_mult_cancel_left:
   850   assumes "a \<noteq> 0" and "is_unit b"
   851   shows "a div (a * b) = 1 div b"
   852 proof -
   853   from assms have "a div (a * b) = a div a div b"
   854     by (simp add: mult_unit_dvd_iff dvd_div_mult2_eq)
   855   with assms show ?thesis by simp
   856 qed
   857 
   858 lemma is_unit_divide_mult_cancel_right:
   859   assumes "a \<noteq> 0" and "is_unit b"
   860   shows "a div (b * a) = 1 div b"
   861   using assms is_unit_divide_mult_cancel_left [of a b] by (simp add: ac_simps)
   862 
   863 end
   864 
   865 class normalization_semidom = algebraic_semidom +
   866   fixes normalize :: "'a \<Rightarrow> 'a"
   867     and unit_factor :: "'a \<Rightarrow> 'a"
   868   assumes unit_factor_mult_normalize [simp]: "unit_factor a * normalize a = a"
   869   assumes normalize_0 [simp]: "normalize 0 = 0"
   870     and unit_factor_0 [simp]: "unit_factor 0 = 0"
   871   assumes is_unit_normalize:
   872     "is_unit a  \<Longrightarrow> normalize a = 1"
   873   assumes unit_factor_is_unit [iff]: 
   874     "a \<noteq> 0 \<Longrightarrow> is_unit (unit_factor a)"
   875   assumes unit_factor_mult: "unit_factor (a * b) = unit_factor a * unit_factor b"
   876 begin
   877 
   878 text \<open>
   879   Class @{class normalization_semidom} cultivates the idea that
   880   each integral domain can be split into equivalence classes
   881   whose representants are associated, i.e. divide each other.
   882   @{const normalize} specifies a canonical representant for each equivalence
   883   class.  The rationale behind this is that it is easier to reason about equality
   884   than equivalences, hence we prefer to think about equality of normalized
   885   values rather than associated elements.
   886 \<close>
   887 
   888 lemma unit_factor_dvd [simp]:
   889   "a \<noteq> 0 \<Longrightarrow> unit_factor a dvd b"
   890   by (rule unit_imp_dvd) simp
   891 
   892 lemma unit_factor_self [simp]:
   893   "unit_factor a dvd a"
   894   by (cases "a = 0") simp_all 
   895   
   896 lemma normalize_mult_unit_factor [simp]:
   897   "normalize a * unit_factor a = a"
   898   using unit_factor_mult_normalize [of a] by (simp add: ac_simps)
   899 
   900 lemma normalize_eq_0_iff [simp]:
   901   "normalize a = 0 \<longleftrightarrow> a = 0" (is "?P \<longleftrightarrow> ?Q")
   902 proof
   903   assume ?P
   904   moreover have "unit_factor a * normalize a = a" by simp
   905   ultimately show ?Q by simp 
   906 next
   907   assume ?Q then show ?P by simp
   908 qed
   909 
   910 lemma unit_factor_eq_0_iff [simp]:
   911   "unit_factor a = 0 \<longleftrightarrow> a = 0" (is "?P \<longleftrightarrow> ?Q")
   912 proof
   913   assume ?P
   914   moreover have "unit_factor a * normalize a = a" by simp
   915   ultimately show ?Q by simp 
   916 next
   917   assume ?Q then show ?P by simp
   918 qed
   919 
   920 lemma is_unit_unit_factor:
   921   assumes "is_unit a" shows "unit_factor a = a"
   922 proof - 
   923   from assms have "normalize a = 1" by (rule is_unit_normalize)
   924   moreover from unit_factor_mult_normalize have "unit_factor a * normalize a = a" .
   925   ultimately show ?thesis by simp
   926 qed
   927 
   928 lemma unit_factor_1 [simp]:
   929   "unit_factor 1 = 1"
   930   by (rule is_unit_unit_factor) simp
   931 
   932 lemma normalize_1 [simp]:
   933   "normalize 1 = 1"
   934   by (rule is_unit_normalize) simp
   935 
   936 lemma normalize_1_iff:
   937   "normalize a = 1 \<longleftrightarrow> is_unit a" (is "?P \<longleftrightarrow> ?Q")
   938 proof
   939   assume ?Q then show ?P by (rule is_unit_normalize)
   940 next
   941   assume ?P
   942   then have "a \<noteq> 0" by auto
   943   from \<open>?P\<close> have "unit_factor a * normalize a = unit_factor a * 1"
   944     by simp
   945   then have "unit_factor a = a"
   946     by simp
   947   moreover have "is_unit (unit_factor a)"
   948     using \<open>a \<noteq> 0\<close> by simp
   949   ultimately show ?Q by simp
   950 qed
   951   
   952 lemma div_normalize [simp]:
   953   "a div normalize a = unit_factor a"
   954 proof (cases "a = 0")
   955   case True then show ?thesis by simp
   956 next
   957   case False then have "normalize a \<noteq> 0" by simp 
   958   with nonzero_mult_divide_cancel_right
   959   have "unit_factor a * normalize a div normalize a = unit_factor a" by blast
   960   then show ?thesis by simp
   961 qed
   962 
   963 lemma div_unit_factor [simp]:
   964   "a div unit_factor a = normalize a"
   965 proof (cases "a = 0")
   966   case True then show ?thesis by simp
   967 next
   968   case False then have "unit_factor a \<noteq> 0" by simp 
   969   with nonzero_mult_divide_cancel_left
   970   have "unit_factor a * normalize a div unit_factor a = normalize a" by blast
   971   then show ?thesis by simp
   972 qed
   973 
   974 lemma normalize_div [simp]:
   975   "normalize a div a = 1 div unit_factor a"
   976 proof (cases "a = 0")
   977   case True then show ?thesis by simp
   978 next
   979   case False
   980   have "normalize a div a = normalize a div (unit_factor a * normalize a)"
   981     by simp
   982   also have "\<dots> = 1 div unit_factor a"
   983     using False by (subst is_unit_divide_mult_cancel_right) simp_all
   984   finally show ?thesis .
   985 qed
   986 
   987 lemma mult_one_div_unit_factor [simp]:
   988   "a * (1 div unit_factor b) = a div unit_factor b"
   989   by (cases "b = 0") simp_all
   990 
   991 lemma normalize_mult:
   992   "normalize (a * b) = normalize a * normalize b"
   993 proof (cases "a = 0 \<or> b = 0")
   994   case True then show ?thesis by auto
   995 next
   996   case False
   997   from unit_factor_mult_normalize have "unit_factor (a * b) * normalize (a * b) = a * b" .
   998   then have "normalize (a * b) = a * b div unit_factor (a * b)" by simp
   999   also have "\<dots> = a * b div unit_factor (b * a)" by (simp add: ac_simps)
  1000   also have "\<dots> = a * b div unit_factor b div unit_factor a"
  1001     using False by (simp add: unit_factor_mult is_unit_div_mult2_eq [symmetric])
  1002   also have "\<dots> = a * (b div unit_factor b) div unit_factor a"
  1003     using False by (subst unit_div_mult_swap) simp_all
  1004   also have "\<dots> = normalize a * normalize b"
  1005     using False by (simp add: mult.commute [of a] mult.commute [of "normalize a"] unit_div_mult_swap [symmetric])
  1006   finally show ?thesis .
  1007 qed
  1008  
  1009 lemma unit_factor_idem [simp]:
  1010   "unit_factor (unit_factor a) = unit_factor a"
  1011   by (cases "a = 0") (auto intro: is_unit_unit_factor)
  1012 
  1013 lemma normalize_unit_factor [simp]:
  1014   "a \<noteq> 0 \<Longrightarrow> normalize (unit_factor a) = 1"
  1015   by (rule is_unit_normalize) simp
  1016   
  1017 lemma normalize_idem [simp]:
  1018   "normalize (normalize a) = normalize a"
  1019 proof (cases "a = 0")
  1020   case True then show ?thesis by simp
  1021 next
  1022   case False
  1023   have "normalize a = normalize (unit_factor a * normalize a)" by simp
  1024   also have "\<dots> = normalize (unit_factor a) * normalize (normalize a)"
  1025     by (simp only: normalize_mult)
  1026   finally show ?thesis using False by simp_all
  1027 qed
  1028 
  1029 lemma unit_factor_normalize [simp]:
  1030   assumes "a \<noteq> 0"
  1031   shows "unit_factor (normalize a) = 1"
  1032 proof -
  1033   from assms have "normalize a \<noteq> 0" by simp
  1034   have "unit_factor (normalize a) * normalize (normalize a) = normalize a"
  1035     by (simp only: unit_factor_mult_normalize)
  1036   then have "unit_factor (normalize a) * normalize a = normalize a"
  1037     by simp
  1038   with \<open>normalize a \<noteq> 0\<close>
  1039   have "unit_factor (normalize a) * normalize a div normalize a = normalize a div normalize a"
  1040     by simp
  1041   with \<open>normalize a \<noteq> 0\<close>
  1042   show ?thesis by simp
  1043 qed
  1044 
  1045 lemma dvd_unit_factor_div:
  1046   assumes "b dvd a"
  1047   shows "unit_factor (a div b) = unit_factor a div unit_factor b"
  1048 proof -
  1049   from assms have "a = a div b * b"
  1050     by simp
  1051   then have "unit_factor a = unit_factor (a div b * b)"
  1052     by simp
  1053   then show ?thesis
  1054     by (cases "b = 0") (simp_all add: unit_factor_mult)
  1055 qed
  1056 
  1057 lemma dvd_normalize_div:
  1058   assumes "b dvd a"
  1059   shows "normalize (a div b) = normalize a div normalize b"
  1060 proof -
  1061   from assms have "a = a div b * b"
  1062     by simp
  1063   then have "normalize a = normalize (a div b * b)"
  1064     by simp
  1065   then show ?thesis
  1066     by (cases "b = 0") (simp_all add: normalize_mult)
  1067 qed
  1068 
  1069 lemma normalize_dvd_iff [simp]:
  1070   "normalize a dvd b \<longleftrightarrow> a dvd b"
  1071 proof -
  1072   have "normalize a dvd b \<longleftrightarrow> unit_factor a * normalize a dvd b"
  1073     using mult_unit_dvd_iff [of "unit_factor a" "normalize a" b]
  1074       by (cases "a = 0") simp_all
  1075   then show ?thesis by simp
  1076 qed
  1077 
  1078 lemma dvd_normalize_iff [simp]:
  1079   "a dvd normalize b \<longleftrightarrow> a dvd b"
  1080 proof -
  1081   have "a dvd normalize  b \<longleftrightarrow> a dvd normalize b * unit_factor b"
  1082     using dvd_mult_unit_iff [of "unit_factor b" a "normalize b"]
  1083       by (cases "b = 0") simp_all
  1084   then show ?thesis by simp
  1085 qed
  1086 
  1087 text \<open>
  1088   We avoid an explicit definition of associated elements but prefer
  1089   explicit normalisation instead.  In theory we could define an abbreviation
  1090   like @{prop "associated a b \<longleftrightarrow> normalize a = normalize b"} but this is
  1091   counterproductive without suggestive infix syntax, which we do not want
  1092   to sacrifice for this purpose here.
  1093 \<close>
  1094 
  1095 lemma associatedI:
  1096   assumes "a dvd b" and "b dvd a"
  1097   shows "normalize a = normalize b"
  1098 proof (cases "a = 0 \<or> b = 0")
  1099   case True with assms show ?thesis by auto
  1100 next
  1101   case False
  1102   from \<open>a dvd b\<close> obtain c where b: "b = a * c" ..
  1103   moreover from \<open>b dvd a\<close> obtain d where a: "a = b * d" ..
  1104   ultimately have "b * 1 = b * (c * d)" by (simp add: ac_simps)
  1105   with False have "1 = c * d"
  1106     unfolding mult_cancel_left by simp
  1107   then have "is_unit c" and "is_unit d" by auto
  1108   with a b show ?thesis by (simp add: normalize_mult is_unit_normalize)
  1109 qed
  1110 
  1111 lemma associatedD1:
  1112   "normalize a = normalize b \<Longrightarrow> a dvd b"
  1113   using dvd_normalize_iff [of _ b, symmetric] normalize_dvd_iff [of a _, symmetric]
  1114   by simp
  1115 
  1116 lemma associatedD2:
  1117   "normalize a = normalize b \<Longrightarrow> b dvd a"
  1118   using dvd_normalize_iff [of _ a, symmetric] normalize_dvd_iff [of b _, symmetric]
  1119   by simp
  1120 
  1121 lemma associated_unit:
  1122   "normalize a = normalize b \<Longrightarrow> is_unit a \<Longrightarrow> is_unit b"
  1123   using dvd_unit_imp_unit by (auto dest!: associatedD1 associatedD2)
  1124 
  1125 lemma associated_iff_dvd:
  1126   "normalize a = normalize b \<longleftrightarrow> a dvd b \<and> b dvd a" (is "?P \<longleftrightarrow> ?Q")
  1127 proof
  1128   assume ?Q then show ?P by (auto intro!: associatedI)
  1129 next
  1130   assume ?P
  1131   then have "unit_factor a * normalize a = unit_factor a * normalize b"
  1132     by simp
  1133   then have *: "normalize b * unit_factor a = a"
  1134     by (simp add: ac_simps)
  1135   show ?Q
  1136   proof (cases "a = 0 \<or> b = 0")
  1137     case True with \<open>?P\<close> show ?thesis by auto
  1138   next
  1139     case False 
  1140     then have "b dvd normalize b * unit_factor a" and "normalize b * unit_factor a dvd b"
  1141       by (simp_all add: mult_unit_dvd_iff dvd_mult_unit_iff)
  1142     with * show ?thesis by simp
  1143   qed
  1144 qed
  1145 
  1146 lemma associated_eqI:
  1147   assumes "a dvd b" and "b dvd a"
  1148   assumes "normalize a = a" and "normalize b = b"
  1149   shows "a = b"
  1150 proof -
  1151   from assms have "normalize a = normalize b"
  1152     unfolding associated_iff_dvd by simp
  1153   with \<open>normalize a = a\<close> have "a = normalize b" by simp
  1154   with \<open>normalize b = b\<close> show "a = b" by simp
  1155 qed
  1156 
  1157 end
  1158 
  1159 class ordered_semiring = semiring + comm_monoid_add + ordered_ab_semigroup_add +
  1160   assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
  1161   assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"
  1162 begin
  1163 
  1164 lemma mult_mono:
  1165   "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * d"
  1166 apply (erule mult_right_mono [THEN order_trans], assumption)
  1167 apply (erule mult_left_mono, assumption)
  1168 done
  1169 
  1170 lemma mult_mono':
  1171   "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * d"
  1172 apply (rule mult_mono)
  1173 apply (fast intro: order_trans)+
  1174 done
  1175 
  1176 end
  1177 
  1178 class ordered_cancel_semiring = ordered_semiring + cancel_comm_monoid_add
  1179 begin
  1180 
  1181 subclass semiring_0_cancel ..
  1182 
  1183 lemma mult_nonneg_nonneg[simp]: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b"
  1184 using mult_left_mono [of 0 b a] by simp
  1185 
  1186 lemma mult_nonneg_nonpos: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> a * b \<le> 0"
  1187 using mult_left_mono [of b 0 a] by simp
  1188 
  1189 lemma mult_nonpos_nonneg: "a \<le> 0 \<Longrightarrow> 0 \<le> b \<Longrightarrow> a * b \<le> 0"
  1190 using mult_right_mono [of a 0 b] by simp
  1191 
  1192 text {* Legacy - use @{text mult_nonpos_nonneg} *}
  1193 lemma mult_nonneg_nonpos2: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> b * a \<le> 0"
  1194 by (drule mult_right_mono [of b 0], auto)
  1195 
  1196 lemma split_mult_neg_le: "(0 \<le> a & b \<le> 0) | (a \<le> 0 & 0 \<le> b) \<Longrightarrow> a * b \<le> 0"
  1197 by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)
  1198 
  1199 end
  1200 
  1201 class linordered_semiring = ordered_semiring + linordered_cancel_ab_semigroup_add
  1202 begin
  1203 
  1204 subclass ordered_cancel_semiring ..
  1205 
  1206 subclass ordered_comm_monoid_add ..
  1207 
  1208 lemma mult_left_less_imp_less:
  1209   "c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
  1210 by (force simp add: mult_left_mono not_le [symmetric])
  1211 
  1212 lemma mult_right_less_imp_less:
  1213   "a * c < b * c \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
  1214 by (force simp add: mult_right_mono not_le [symmetric])
  1215 
  1216 end
  1217 
  1218 class linordered_semiring_1 = linordered_semiring + semiring_1
  1219 begin
  1220 
  1221 lemma convex_bound_le:
  1222   assumes "x \<le> a" "y \<le> a" "0 \<le> u" "0 \<le> v" "u + v = 1"
  1223   shows "u * x + v * y \<le> a"
  1224 proof-
  1225   from assms have "u * x + v * y \<le> u * a + v * a"
  1226     by (simp add: add_mono mult_left_mono)
  1227   thus ?thesis using assms unfolding distrib_right[symmetric] by simp
  1228 qed
  1229 
  1230 end
  1231 
  1232 class linordered_semiring_strict = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add +
  1233   assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
  1234   assumes mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c"
  1235 begin
  1236 
  1237 subclass semiring_0_cancel ..
  1238 
  1239 subclass linordered_semiring
  1240 proof
  1241   fix a b c :: 'a
  1242   assume A: "a \<le> b" "0 \<le> c"
  1243   from A show "c * a \<le> c * b"
  1244     unfolding le_less
  1245     using mult_strict_left_mono by (cases "c = 0") auto
  1246   from A show "a * c \<le> b * c"
  1247     unfolding le_less
  1248     using mult_strict_right_mono by (cases "c = 0") auto
  1249 qed
  1250 
  1251 lemma mult_left_le_imp_le:
  1252   "c * a \<le> c * b \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
  1253 by (force simp add: mult_strict_left_mono _not_less [symmetric])
  1254 
  1255 lemma mult_right_le_imp_le:
  1256   "a * c \<le> b * c \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
  1257 by (force simp add: mult_strict_right_mono not_less [symmetric])
  1258 
  1259 lemma mult_pos_pos[simp]: "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a * b"
  1260 using mult_strict_left_mono [of 0 b a] by simp
  1261 
  1262 lemma mult_pos_neg: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> a * b < 0"
  1263 using mult_strict_left_mono [of b 0 a] by simp
  1264 
  1265 lemma mult_neg_pos: "a < 0 \<Longrightarrow> 0 < b \<Longrightarrow> a * b < 0"
  1266 using mult_strict_right_mono [of a 0 b] by simp
  1267 
  1268 text {* Legacy - use @{text mult_neg_pos} *}
  1269 lemma mult_pos_neg2: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> b * a < 0"
  1270 by (drule mult_strict_right_mono [of b 0], auto)
  1271 
  1272 lemma zero_less_mult_pos:
  1273   "0 < a * b \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"
  1274 apply (cases "b\<le>0")
  1275  apply (auto simp add: le_less not_less)
  1276 apply (drule_tac mult_pos_neg [of a b])
  1277  apply (auto dest: less_not_sym)
  1278 done
  1279 
  1280 lemma zero_less_mult_pos2:
  1281   "0 < b * a \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"
  1282 apply (cases "b\<le>0")
  1283  apply (auto simp add: le_less not_less)
  1284 apply (drule_tac mult_pos_neg2 [of a b])
  1285  apply (auto dest: less_not_sym)
  1286 done
  1287 
  1288 text{*Strict monotonicity in both arguments*}
  1289 lemma mult_strict_mono:
  1290   assumes "a < b" and "c < d" and "0 < b" and "0 \<le> c"
  1291   shows "a * c < b * d"
  1292   using assms apply (cases "c=0")
  1293   apply (simp)
  1294   apply (erule mult_strict_right_mono [THEN less_trans])
  1295   apply (force simp add: le_less)
  1296   apply (erule mult_strict_left_mono, assumption)
  1297   done
  1298 
  1299 text{*This weaker variant has more natural premises*}
  1300 lemma mult_strict_mono':
  1301   assumes "a < b" and "c < d" and "0 \<le> a" and "0 \<le> c"
  1302   shows "a * c < b * d"
  1303 by (rule mult_strict_mono) (insert assms, auto)
  1304 
  1305 lemma mult_less_le_imp_less:
  1306   assumes "a < b" and "c \<le> d" and "0 \<le> a" and "0 < c"
  1307   shows "a * c < b * d"
  1308   using assms apply (subgoal_tac "a * c < b * c")
  1309   apply (erule less_le_trans)
  1310   apply (erule mult_left_mono)
  1311   apply simp
  1312   apply (erule mult_strict_right_mono)
  1313   apply assumption
  1314   done
  1315 
  1316 lemma mult_le_less_imp_less:
  1317   assumes "a \<le> b" and "c < d" and "0 < a" and "0 \<le> c"
  1318   shows "a * c < b * d"
  1319   using assms apply (subgoal_tac "a * c \<le> b * c")
  1320   apply (erule le_less_trans)
  1321   apply (erule mult_strict_left_mono)
  1322   apply simp
  1323   apply (erule mult_right_mono)
  1324   apply simp
  1325   done
  1326 
  1327 end
  1328 
  1329 class linordered_semiring_1_strict = linordered_semiring_strict + semiring_1
  1330 begin
  1331 
  1332 subclass linordered_semiring_1 ..
  1333 
  1334 lemma convex_bound_lt:
  1335   assumes "x < a" "y < a" "0 \<le> u" "0 \<le> v" "u + v = 1"
  1336   shows "u * x + v * y < a"
  1337 proof -
  1338   from assms have "u * x + v * y < u * a + v * a"
  1339     by (cases "u = 0")
  1340        (auto intro!: add_less_le_mono mult_strict_left_mono mult_left_mono)
  1341   thus ?thesis using assms unfolding distrib_right[symmetric] by simp
  1342 qed
  1343 
  1344 end
  1345 
  1346 class ordered_comm_semiring = comm_semiring_0 + ordered_ab_semigroup_add +
  1347   assumes comm_mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
  1348 begin
  1349 
  1350 subclass ordered_semiring
  1351 proof
  1352   fix a b c :: 'a
  1353   assume "a \<le> b" "0 \<le> c"
  1354   thus "c * a \<le> c * b" by (rule comm_mult_left_mono)
  1355   thus "a * c \<le> b * c" by (simp only: mult.commute)
  1356 qed
  1357 
  1358 end
  1359 
  1360 class ordered_cancel_comm_semiring = ordered_comm_semiring + cancel_comm_monoid_add
  1361 begin
  1362 
  1363 subclass comm_semiring_0_cancel ..
  1364 subclass ordered_comm_semiring ..
  1365 subclass ordered_cancel_semiring ..
  1366 
  1367 end
  1368 
  1369 class linordered_comm_semiring_strict = comm_semiring_0 + linordered_cancel_ab_semigroup_add +
  1370   assumes comm_mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
  1371 begin
  1372 
  1373 subclass linordered_semiring_strict
  1374 proof
  1375   fix a b c :: 'a
  1376   assume "a < b" "0 < c"
  1377   thus "c * a < c * b" by (rule comm_mult_strict_left_mono)
  1378   thus "a * c < b * c" by (simp only: mult.commute)
  1379 qed
  1380 
  1381 subclass ordered_cancel_comm_semiring
  1382 proof
  1383   fix a b c :: 'a
  1384   assume "a \<le> b" "0 \<le> c"
  1385   thus "c * a \<le> c * b"
  1386     unfolding le_less
  1387     using mult_strict_left_mono by (cases "c = 0") auto
  1388 qed
  1389 
  1390 end
  1391 
  1392 class ordered_ring = ring + ordered_cancel_semiring
  1393 begin
  1394 
  1395 subclass ordered_ab_group_add ..
  1396 
  1397 lemma less_add_iff1:
  1398   "a * e + c < b * e + d \<longleftrightarrow> (a - b) * e + c < d"
  1399 by (simp add: algebra_simps)
  1400 
  1401 lemma less_add_iff2:
  1402   "a * e + c < b * e + d \<longleftrightarrow> c < (b - a) * e + d"
  1403 by (simp add: algebra_simps)
  1404 
  1405 lemma le_add_iff1:
  1406   "a * e + c \<le> b * e + d \<longleftrightarrow> (a - b) * e + c \<le> d"
  1407 by (simp add: algebra_simps)
  1408 
  1409 lemma le_add_iff2:
  1410   "a * e + c \<le> b * e + d \<longleftrightarrow> c \<le> (b - a) * e + d"
  1411 by (simp add: algebra_simps)
  1412 
  1413 lemma mult_left_mono_neg:
  1414   "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> c * a \<le> c * b"
  1415   apply (drule mult_left_mono [of _ _ "- c"])
  1416   apply simp_all
  1417   done
  1418 
  1419 lemma mult_right_mono_neg:
  1420   "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> a * c \<le> b * c"
  1421   apply (drule mult_right_mono [of _ _ "- c"])
  1422   apply simp_all
  1423   done
  1424 
  1425 lemma mult_nonpos_nonpos: "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> 0 \<le> a * b"
  1426 using mult_right_mono_neg [of a 0 b] by simp
  1427 
  1428 lemma split_mult_pos_le:
  1429   "(0 \<le> a \<and> 0 \<le> b) \<or> (a \<le> 0 \<and> b \<le> 0) \<Longrightarrow> 0 \<le> a * b"
  1430 by (auto simp add: mult_nonpos_nonpos)
  1431 
  1432 end
  1433 
  1434 class linordered_ring = ring + linordered_semiring + linordered_ab_group_add + abs_if
  1435 begin
  1436 
  1437 subclass ordered_ring ..
  1438 
  1439 subclass ordered_ab_group_add_abs
  1440 proof
  1441   fix a b
  1442   show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
  1443     by (auto simp add: abs_if not_le not_less algebra_simps simp del: add.commute dest: add_neg_neg add_nonneg_nonneg)
  1444 qed (auto simp add: abs_if)
  1445 
  1446 lemma zero_le_square [simp]: "0 \<le> a * a"
  1447   using linear [of 0 a]
  1448   by (auto simp add: mult_nonpos_nonpos)
  1449 
  1450 lemma not_square_less_zero [simp]: "\<not> (a * a < 0)"
  1451   by (simp add: not_less)
  1452 
  1453 end
  1454 
  1455 class linordered_ring_strict = ring + linordered_semiring_strict
  1456   + ordered_ab_group_add + abs_if
  1457 begin
  1458 
  1459 subclass linordered_ring ..
  1460 
  1461 lemma mult_strict_left_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> c * a < c * b"
  1462 using mult_strict_left_mono [of b a "- c"] by simp
  1463 
  1464 lemma mult_strict_right_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> a * c < b * c"
  1465 using mult_strict_right_mono [of b a "- c"] by simp
  1466 
  1467 lemma mult_neg_neg: "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> 0 < a * b"
  1468 using mult_strict_right_mono_neg [of a 0 b] by simp
  1469 
  1470 subclass ring_no_zero_divisors
  1471 proof
  1472   fix a b
  1473   assume "a \<noteq> 0" then have A: "a < 0 \<or> 0 < a" by (simp add: neq_iff)
  1474   assume "b \<noteq> 0" then have B: "b < 0 \<or> 0 < b" by (simp add: neq_iff)
  1475   have "a * b < 0 \<or> 0 < a * b"
  1476   proof (cases "a < 0")
  1477     case True note A' = this
  1478     show ?thesis proof (cases "b < 0")
  1479       case True with A'
  1480       show ?thesis by (auto dest: mult_neg_neg)
  1481     next
  1482       case False with B have "0 < b" by auto
  1483       with A' show ?thesis by (auto dest: mult_strict_right_mono)
  1484     qed
  1485   next
  1486     case False with A have A': "0 < a" by auto
  1487     show ?thesis proof (cases "b < 0")
  1488       case True with A'
  1489       show ?thesis by (auto dest: mult_strict_right_mono_neg)
  1490     next
  1491       case False with B have "0 < b" by auto
  1492       with A' show ?thesis by auto
  1493     qed
  1494   qed
  1495   then show "a * b \<noteq> 0" by (simp add: neq_iff)
  1496 qed
  1497 
  1498 lemma zero_less_mult_iff: "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0"
  1499   by (cases a 0 b 0 rule: linorder_cases[case_product linorder_cases])
  1500      (auto simp add: mult_neg_neg not_less le_less dest: zero_less_mult_pos zero_less_mult_pos2)
  1501 
  1502 lemma zero_le_mult_iff: "0 \<le> a * b \<longleftrightarrow> 0 \<le> a \<and> 0 \<le> b \<or> a \<le> 0 \<and> b \<le> 0"
  1503   by (auto simp add: eq_commute [of 0] le_less not_less zero_less_mult_iff)
  1504 
  1505 lemma mult_less_0_iff:
  1506   "a * b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b"
  1507   apply (insert zero_less_mult_iff [of "-a" b])
  1508   apply force
  1509   done
  1510 
  1511 lemma mult_le_0_iff:
  1512   "a * b \<le> 0 \<longleftrightarrow> 0 \<le> a \<and> b \<le> 0 \<or> a \<le> 0 \<and> 0 \<le> b"
  1513   apply (insert zero_le_mult_iff [of "-a" b])
  1514   apply force
  1515   done
  1516 
  1517 text{*Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"},
  1518    also with the relations @{text "\<le>"} and equality.*}
  1519 
  1520 text{*These ``disjunction'' versions produce two cases when the comparison is
  1521  an assumption, but effectively four when the comparison is a goal.*}
  1522 
  1523 lemma mult_less_cancel_right_disj:
  1524   "a * c < b * c \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"
  1525   apply (cases "c = 0")
  1526   apply (auto simp add: neq_iff mult_strict_right_mono
  1527                       mult_strict_right_mono_neg)
  1528   apply (auto simp add: not_less
  1529                       not_le [symmetric, of "a*c"]
  1530                       not_le [symmetric, of a])
  1531   apply (erule_tac [!] notE)
  1532   apply (auto simp add: less_imp_le mult_right_mono
  1533                       mult_right_mono_neg)
  1534   done
  1535 
  1536 lemma mult_less_cancel_left_disj:
  1537   "c * a < c * b \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"
  1538   apply (cases "c = 0")
  1539   apply (auto simp add: neq_iff mult_strict_left_mono
  1540                       mult_strict_left_mono_neg)
  1541   apply (auto simp add: not_less
  1542                       not_le [symmetric, of "c*a"]
  1543                       not_le [symmetric, of a])
  1544   apply (erule_tac [!] notE)
  1545   apply (auto simp add: less_imp_le mult_left_mono
  1546                       mult_left_mono_neg)
  1547   done
  1548 
  1549 text{*The ``conjunction of implication'' lemmas produce two cases when the
  1550 comparison is a goal, but give four when the comparison is an assumption.*}
  1551 
  1552 lemma mult_less_cancel_right:
  1553   "a * c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)"
  1554   using mult_less_cancel_right_disj [of a c b] by auto
  1555 
  1556 lemma mult_less_cancel_left:
  1557   "c * a < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)"
  1558   using mult_less_cancel_left_disj [of c a b] by auto
  1559 
  1560 lemma mult_le_cancel_right:
  1561    "a * c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
  1562 by (simp add: not_less [symmetric] mult_less_cancel_right_disj)
  1563 
  1564 lemma mult_le_cancel_left:
  1565   "c * a \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
  1566 by (simp add: not_less [symmetric] mult_less_cancel_left_disj)
  1567 
  1568 lemma mult_le_cancel_left_pos:
  1569   "0 < c \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> a \<le> b"
  1570 by (auto simp: mult_le_cancel_left)
  1571 
  1572 lemma mult_le_cancel_left_neg:
  1573   "c < 0 \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> b \<le> a"
  1574 by (auto simp: mult_le_cancel_left)
  1575 
  1576 lemma mult_less_cancel_left_pos:
  1577   "0 < c \<Longrightarrow> c * a < c * b \<longleftrightarrow> a < b"
  1578 by (auto simp: mult_less_cancel_left)
  1579 
  1580 lemma mult_less_cancel_left_neg:
  1581   "c < 0 \<Longrightarrow> c * a < c * b \<longleftrightarrow> b < a"
  1582 by (auto simp: mult_less_cancel_left)
  1583 
  1584 end
  1585 
  1586 lemmas mult_sign_intros =
  1587   mult_nonneg_nonneg mult_nonneg_nonpos
  1588   mult_nonpos_nonneg mult_nonpos_nonpos
  1589   mult_pos_pos mult_pos_neg
  1590   mult_neg_pos mult_neg_neg
  1591 
  1592 class ordered_comm_ring = comm_ring + ordered_comm_semiring
  1593 begin
  1594 
  1595 subclass ordered_ring ..
  1596 subclass ordered_cancel_comm_semiring ..
  1597 
  1598 end
  1599 
  1600 class linordered_semidom = semidom + linordered_comm_semiring_strict +
  1601   assumes zero_less_one [simp]: "0 < 1"
  1602   assumes le_add_diff_inverse2 [simp]: "b \<le> a \<Longrightarrow> a - b + b = a"
  1603 begin
  1604 
  1605 text {* Addition is the inverse of subtraction. *}
  1606 
  1607 lemma le_add_diff_inverse [simp]: "b \<le> a \<Longrightarrow> b + (a - b) = a"
  1608   by (frule le_add_diff_inverse2) (simp add: add.commute)
  1609 
  1610 lemma add_diff_inverse: "~ a<b \<Longrightarrow> b + (a - b) = a"
  1611   by simp
  1612 
  1613 lemma add_le_imp_le_diff: 
  1614   shows "i + k \<le> n \<Longrightarrow> i \<le> n - k"
  1615   apply (subst add_le_cancel_right [where c=k, symmetric])
  1616   apply (frule le_add_diff_inverse2)
  1617   apply (simp only: add.assoc [symmetric])
  1618   using add_implies_diff by fastforce
  1619 
  1620 lemma add_le_add_imp_diff_le: 
  1621   assumes a1: "i + k \<le> n"
  1622       and a2: "n \<le> j + k"
  1623   shows "\<lbrakk>i + k \<le> n; n \<le> j + k\<rbrakk> \<Longrightarrow> n - k \<le> j"
  1624 proof -
  1625   have "n - (i + k) + (i + k) = n"
  1626     using a1 by simp
  1627   moreover have "n - k = n - k - i + i"
  1628     using a1 by (simp add: add_le_imp_le_diff)
  1629   ultimately show ?thesis
  1630     using a2
  1631     apply (simp add: add.assoc [symmetric])
  1632     apply (rule add_le_imp_le_diff [of _ k "j+k", simplified add_diff_cancel_right'])
  1633     by (simp add: add.commute diff_diff_add)
  1634 qed
  1635 
  1636 lemma pos_add_strict:
  1637   shows "0 < a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
  1638   using add_strict_mono [of 0 a b c] by simp
  1639 
  1640 lemma zero_le_one [simp]: "0 \<le> 1"
  1641 by (rule zero_less_one [THEN less_imp_le])
  1642 
  1643 lemma not_one_le_zero [simp]: "\<not> 1 \<le> 0"
  1644 by (simp add: not_le)
  1645 
  1646 lemma not_one_less_zero [simp]: "\<not> 1 < 0"
  1647 by (simp add: not_less)
  1648 
  1649 lemma less_1_mult:
  1650   assumes "1 < m" and "1 < n"
  1651   shows "1 < m * n"
  1652   using assms mult_strict_mono [of 1 m 1 n]
  1653     by (simp add:  less_trans [OF zero_less_one])
  1654 
  1655 lemma mult_left_le: "c \<le> 1 \<Longrightarrow> 0 \<le> a \<Longrightarrow> a * c \<le> a"
  1656   using mult_left_mono[of c 1 a] by simp
  1657 
  1658 lemma mult_le_one: "a \<le> 1 \<Longrightarrow> 0 \<le> b \<Longrightarrow> b \<le> 1 \<Longrightarrow> a * b \<le> 1"
  1659   using mult_mono[of a 1 b 1] by simp
  1660 
  1661 end
  1662 
  1663 class linordered_idom = comm_ring_1 +
  1664   linordered_comm_semiring_strict + ordered_ab_group_add +
  1665   abs_if + sgn_if
  1666 begin
  1667 
  1668 subclass linordered_semiring_1_strict ..
  1669 subclass linordered_ring_strict ..
  1670 subclass ordered_comm_ring ..
  1671 subclass idom ..
  1672 
  1673 subclass linordered_semidom
  1674 proof
  1675   have "0 \<le> 1 * 1" by (rule zero_le_square)
  1676   thus "0 < 1" by (simp add: le_less)
  1677   show "\<And>b a. b \<le> a \<Longrightarrow> a - b + b = a"
  1678     by simp
  1679 qed
  1680 
  1681 lemma linorder_neqE_linordered_idom:
  1682   assumes "x \<noteq> y" obtains "x < y" | "y < x"
  1683   using assms by (rule neqE)
  1684 
  1685 text {* These cancellation simprules also produce two cases when the comparison is a goal. *}
  1686 
  1687 lemma mult_le_cancel_right1:
  1688   "c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)"
  1689 by (insert mult_le_cancel_right [of 1 c b], simp)
  1690 
  1691 lemma mult_le_cancel_right2:
  1692   "a * c \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)"
  1693 by (insert mult_le_cancel_right [of a c 1], simp)
  1694 
  1695 lemma mult_le_cancel_left1:
  1696   "c \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)"
  1697 by (insert mult_le_cancel_left [of c 1 b], simp)
  1698 
  1699 lemma mult_le_cancel_left2:
  1700   "c * a \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)"
  1701 by (insert mult_le_cancel_left [of c a 1], simp)
  1702 
  1703 lemma mult_less_cancel_right1:
  1704   "c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)"
  1705 by (insert mult_less_cancel_right [of 1 c b], simp)
  1706 
  1707 lemma mult_less_cancel_right2:
  1708   "a * c < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"
  1709 by (insert mult_less_cancel_right [of a c 1], simp)
  1710 
  1711 lemma mult_less_cancel_left1:
  1712   "c < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)"
  1713 by (insert mult_less_cancel_left [of c 1 b], simp)
  1714 
  1715 lemma mult_less_cancel_left2:
  1716   "c * a < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"
  1717 by (insert mult_less_cancel_left [of c a 1], simp)
  1718 
  1719 lemma sgn_sgn [simp]:
  1720   "sgn (sgn a) = sgn a"
  1721 unfolding sgn_if by simp
  1722 
  1723 lemma sgn_0_0:
  1724   "sgn a = 0 \<longleftrightarrow> a = 0"
  1725 unfolding sgn_if by simp
  1726 
  1727 lemma sgn_1_pos:
  1728   "sgn a = 1 \<longleftrightarrow> a > 0"
  1729 unfolding sgn_if by simp
  1730 
  1731 lemma sgn_1_neg:
  1732   "sgn a = - 1 \<longleftrightarrow> a < 0"
  1733 unfolding sgn_if by auto
  1734 
  1735 lemma sgn_pos [simp]:
  1736   "0 < a \<Longrightarrow> sgn a = 1"
  1737 unfolding sgn_1_pos .
  1738 
  1739 lemma sgn_neg [simp]:
  1740   "a < 0 \<Longrightarrow> sgn a = - 1"
  1741 unfolding sgn_1_neg .
  1742 
  1743 lemma sgn_times:
  1744   "sgn (a * b) = sgn a * sgn b"
  1745 by (auto simp add: sgn_if zero_less_mult_iff)
  1746 
  1747 lemma abs_sgn: "\<bar>k\<bar> = k * sgn k"
  1748 unfolding sgn_if abs_if by auto
  1749 
  1750 lemma sgn_greater [simp]:
  1751   "0 < sgn a \<longleftrightarrow> 0 < a"
  1752   unfolding sgn_if by auto
  1753 
  1754 lemma sgn_less [simp]:
  1755   "sgn a < 0 \<longleftrightarrow> a < 0"
  1756   unfolding sgn_if by auto
  1757 
  1758 lemma abs_dvd_iff [simp]: "\<bar>m\<bar> dvd k \<longleftrightarrow> m dvd k"
  1759   by (simp add: abs_if)
  1760 
  1761 lemma dvd_abs_iff [simp]: "m dvd \<bar>k\<bar> \<longleftrightarrow> m dvd k"
  1762   by (simp add: abs_if)
  1763 
  1764 lemma dvd_if_abs_eq:
  1765   "\<bar>l\<bar> = \<bar>k\<bar> \<Longrightarrow> l dvd k"
  1766 by(subst abs_dvd_iff[symmetric]) simp
  1767 
  1768 text {* The following lemmas can be proven in more general structures, but
  1769 are dangerous as simp rules in absence of @{thm neg_equal_zero},
  1770 @{thm neg_less_pos}, @{thm neg_less_eq_nonneg}. *}
  1771 
  1772 lemma equation_minus_iff_1 [simp, no_atp]:
  1773   "1 = - a \<longleftrightarrow> a = - 1"
  1774   by (fact equation_minus_iff)
  1775 
  1776 lemma minus_equation_iff_1 [simp, no_atp]:
  1777   "- a = 1 \<longleftrightarrow> a = - 1"
  1778   by (subst minus_equation_iff, auto)
  1779 
  1780 lemma le_minus_iff_1 [simp, no_atp]:
  1781   "1 \<le> - b \<longleftrightarrow> b \<le> - 1"
  1782   by (fact le_minus_iff)
  1783 
  1784 lemma minus_le_iff_1 [simp, no_atp]:
  1785   "- a \<le> 1 \<longleftrightarrow> - 1 \<le> a"
  1786   by (fact minus_le_iff)
  1787 
  1788 lemma less_minus_iff_1 [simp, no_atp]:
  1789   "1 < - b \<longleftrightarrow> b < - 1"
  1790   by (fact less_minus_iff)
  1791 
  1792 lemma minus_less_iff_1 [simp, no_atp]:
  1793   "- a < 1 \<longleftrightarrow> - 1 < a"
  1794   by (fact minus_less_iff)
  1795 
  1796 end
  1797 
  1798 text {* Simprules for comparisons where common factors can be cancelled. *}
  1799 
  1800 lemmas mult_compare_simps =
  1801     mult_le_cancel_right mult_le_cancel_left
  1802     mult_le_cancel_right1 mult_le_cancel_right2
  1803     mult_le_cancel_left1 mult_le_cancel_left2
  1804     mult_less_cancel_right mult_less_cancel_left
  1805     mult_less_cancel_right1 mult_less_cancel_right2
  1806     mult_less_cancel_left1 mult_less_cancel_left2
  1807     mult_cancel_right mult_cancel_left
  1808     mult_cancel_right1 mult_cancel_right2
  1809     mult_cancel_left1 mult_cancel_left2
  1810 
  1811 text {* Reasoning about inequalities with division *}
  1812 
  1813 context linordered_semidom
  1814 begin
  1815 
  1816 lemma less_add_one: "a < a + 1"
  1817 proof -
  1818   have "a + 0 < a + 1"
  1819     by (blast intro: zero_less_one add_strict_left_mono)
  1820   thus ?thesis by simp
  1821 qed
  1822 
  1823 lemma zero_less_two: "0 < 1 + 1"
  1824 by (blast intro: less_trans zero_less_one less_add_one)
  1825 
  1826 end
  1827 
  1828 context linordered_idom
  1829 begin
  1830 
  1831 lemma mult_right_le_one_le:
  1832   "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> x * y \<le> x"
  1833   by (rule mult_left_le)
  1834 
  1835 lemma mult_left_le_one_le:
  1836   "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> y * x \<le> x"
  1837   by (auto simp add: mult_le_cancel_right2)
  1838 
  1839 end
  1840 
  1841 text {* Absolute Value *}
  1842 
  1843 context linordered_idom
  1844 begin
  1845 
  1846 lemma mult_sgn_abs:
  1847   "sgn x * \<bar>x\<bar> = x"
  1848   unfolding abs_if sgn_if by auto
  1849 
  1850 lemma abs_one [simp]:
  1851   "\<bar>1\<bar> = 1"
  1852   by (simp add: abs_if)
  1853 
  1854 end
  1855 
  1856 class ordered_ring_abs = ordered_ring + ordered_ab_group_add_abs +
  1857   assumes abs_eq_mult:
  1858     "(0 \<le> a \<or> a \<le> 0) \<and> (0 \<le> b \<or> b \<le> 0) \<Longrightarrow> \<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>"
  1859 
  1860 context linordered_idom
  1861 begin
  1862 
  1863 subclass ordered_ring_abs proof
  1864 qed (auto simp add: abs_if not_less mult_less_0_iff)
  1865 
  1866 lemma abs_mult:
  1867   "\<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>"
  1868   by (rule abs_eq_mult) auto
  1869 
  1870 lemma abs_mult_self:
  1871   "\<bar>a\<bar> * \<bar>a\<bar> = a * a"
  1872   by (simp add: abs_if)
  1873 
  1874 lemma abs_mult_less:
  1875   "\<bar>a\<bar> < c \<Longrightarrow> \<bar>b\<bar> < d \<Longrightarrow> \<bar>a\<bar> * \<bar>b\<bar> < c * d"
  1876 proof -
  1877   assume ac: "\<bar>a\<bar> < c"
  1878   hence cpos: "0<c" by (blast intro: le_less_trans abs_ge_zero)
  1879   assume "\<bar>b\<bar> < d"
  1880   thus ?thesis by (simp add: ac cpos mult_strict_mono)
  1881 qed
  1882 
  1883 lemma abs_less_iff:
  1884   "\<bar>a\<bar> < b \<longleftrightarrow> a < b \<and> - a < b"
  1885   by (simp add: less_le abs_le_iff) (auto simp add: abs_if)
  1886 
  1887 lemma abs_mult_pos:
  1888   "0 \<le> x \<Longrightarrow> \<bar>y\<bar> * x = \<bar>y * x\<bar>"
  1889   by (simp add: abs_mult)
  1890 
  1891 lemma abs_diff_less_iff:
  1892   "\<bar>x - a\<bar> < r \<longleftrightarrow> a - r < x \<and> x < a + r"
  1893   by (auto simp add: diff_less_eq ac_simps abs_less_iff)
  1894 
  1895 lemma abs_diff_le_iff:
  1896    "\<bar>x - a\<bar> \<le> r \<longleftrightarrow> a - r \<le> x \<and> x \<le> a + r"
  1897   by (auto simp add: diff_le_eq ac_simps abs_le_iff)
  1898 
  1899 end
  1900 
  1901 hide_fact (open) comm_mult_left_mono comm_mult_strict_left_mono distrib
  1902 
  1903 code_identifier
  1904   code_module Rings \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
  1905 
  1906 end