src/HOL/Rings.thy
author haftmann
Wed Jul 08 20:19:12 2015 +0200 (2015-07-08)
changeset 60690 a9e45c9588c3
parent 60688 01488b559910
child 60758 d8d85a8172b5
permissions -rw-r--r--
tuned facts
     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 lemma divide_1 [simp]:
   633   "a div 1 = a"
   634   using nonzero_mult_divide_cancel_left [of 1 a] by simp
   635 
   636 lemma dvd_times_left_cancel_iff [simp]:
   637   assumes "a \<noteq> 0"
   638   shows "a * b dvd a * c \<longleftrightarrow> b dvd c" (is "?P \<longleftrightarrow> ?Q")
   639 proof
   640   assume ?P then obtain d where "a * c = a * b * d" ..
   641   with assms have "c = b * d" by (simp add: ac_simps)
   642   then show ?Q ..
   643 next
   644   assume ?Q then obtain d where "c = b * d" .. 
   645   then have "a * c = a * b * d" by (simp add: ac_simps)
   646   then show ?P ..
   647 qed
   648   
   649 lemma dvd_times_right_cancel_iff [simp]:
   650   assumes "a \<noteq> 0"
   651   shows "b * a dvd c * a \<longleftrightarrow> b dvd c" (is "?P \<longleftrightarrow> ?Q")
   652 using dvd_times_left_cancel_iff [of a b c] assms by (simp add: ac_simps)
   653   
   654 lemma div_dvd_iff_mult:
   655   assumes "b \<noteq> 0" and "b dvd a"
   656   shows "a div b dvd c \<longleftrightarrow> a dvd c * b"
   657 proof -
   658   from \<open>b dvd a\<close> obtain d where "a = b * d" ..
   659   with \<open>b \<noteq> 0\<close> show ?thesis by (simp add: ac_simps)
   660 qed
   661 
   662 lemma dvd_div_iff_mult:
   663   assumes "c \<noteq> 0" and "c dvd b"
   664   shows "a dvd b div c \<longleftrightarrow> a * c dvd b"
   665 proof -
   666   from \<open>c dvd b\<close> obtain d where "b = c * d" ..
   667   with \<open>c \<noteq> 0\<close> show ?thesis by (simp add: mult.commute [of a])
   668 qed
   669 
   670 end
   671 
   672 class idom_divide = idom + semidom_divide
   673 
   674 class algebraic_semidom = semidom_divide
   675 begin
   676 
   677 text \<open>
   678   Class @{class algebraic_semidom} enriches a integral domain
   679   by notions from algebra, like units in a ring.
   680   It is a separate class to avoid spoiling fields with notions
   681   which are degenerated there.
   682 \<close>
   683 
   684 lemma dvd_div_mult_self [simp]:
   685   "a dvd b \<Longrightarrow> b div a * a = b"
   686   by (cases "a = 0") (auto elim: dvdE simp add: ac_simps)
   687 
   688 lemma dvd_mult_div_cancel [simp]:
   689   "a dvd b \<Longrightarrow> a * (b div a) = b"
   690   using dvd_div_mult_self [of a b] by (simp add: ac_simps)
   691 
   692 lemma div_mult_swap:
   693   assumes "c dvd b"
   694   shows "a * (b div c) = (a * b) div c"
   695 proof (cases "c = 0")
   696   case True then show ?thesis by simp
   697 next
   698   case False from assms obtain d where "b = c * d" ..
   699   moreover from False have "a * divide (d * c) c = ((a * d) * c) div c"
   700     by simp
   701   ultimately show ?thesis by (simp add: ac_simps)
   702 qed
   703 
   704 lemma dvd_div_mult:
   705   assumes "c dvd b"
   706   shows "b div c * a = (b * a) div c"
   707   using assms div_mult_swap [of c b a] by (simp add: ac_simps)
   708 
   709 lemma dvd_div_mult2_eq:
   710   assumes "b * c dvd a"
   711   shows "a div (b * c) = a div b div c"
   712 using assms proof
   713   fix k
   714   assume "a = b * c * k"
   715   then show ?thesis
   716     by (cases "b = 0 \<or> c = 0") (auto, simp add: ac_simps)
   717 qed
   718 
   719 
   720 text \<open>Units: invertible elements in a ring\<close>
   721 
   722 abbreviation is_unit :: "'a \<Rightarrow> bool"
   723 where
   724   "is_unit a \<equiv> a dvd 1"
   725 
   726 lemma not_is_unit_0 [simp]:
   727   "\<not> is_unit 0"
   728   by simp
   729 
   730 lemma unit_imp_dvd [dest]:
   731   "is_unit b \<Longrightarrow> b dvd a"
   732   by (rule dvd_trans [of _ 1]) simp_all
   733 
   734 lemma unit_dvdE:
   735   assumes "is_unit a"
   736   obtains c where "a \<noteq> 0" and "b = a * c"
   737 proof -
   738   from assms have "a dvd b" by auto
   739   then obtain c where "b = a * c" ..
   740   moreover from assms have "a \<noteq> 0" by auto
   741   ultimately show thesis using that by blast
   742 qed
   743 
   744 lemma dvd_unit_imp_unit:
   745   "a dvd b \<Longrightarrow> is_unit b \<Longrightarrow> is_unit a"
   746   by (rule dvd_trans)
   747 
   748 lemma unit_div_1_unit [simp, intro]:
   749   assumes "is_unit a"
   750   shows "is_unit (1 div a)"
   751 proof -
   752   from assms have "1 = 1 div a * a" by simp
   753   then show "is_unit (1 div a)" by (rule dvdI)
   754 qed
   755 
   756 lemma is_unitE [elim?]:
   757   assumes "is_unit a"
   758   obtains b where "a \<noteq> 0" and "b \<noteq> 0"
   759     and "is_unit b" and "1 div a = b" and "1 div b = a"
   760     and "a * b = 1" and "c div a = c * b"
   761 proof (rule that)
   762   def b \<equiv> "1 div a"
   763   then show "1 div a = b" by simp
   764   from b_def `is_unit a` show "is_unit b" by simp
   765   from `is_unit a` and `is_unit b` show "a \<noteq> 0" and "b \<noteq> 0" by auto
   766   from b_def `is_unit a` show "a * b = 1" by simp
   767   then have "1 = a * b" ..
   768   with b_def `b \<noteq> 0` show "1 div b = a" by simp
   769   from `is_unit a` have "a dvd c" ..
   770   then obtain d where "c = a * d" ..
   771   with `a \<noteq> 0` `a * b = 1` show "c div a = c * b"
   772     by (simp add: mult.assoc mult.left_commute [of a])
   773 qed
   774 
   775 lemma unit_prod [intro]:
   776   "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a * b)"
   777   by (subst mult_1_left [of 1, symmetric]) (rule mult_dvd_mono)
   778 
   779 lemma unit_div [intro]:
   780   "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a div b)"
   781   by (erule is_unitE [of b a]) (simp add: ac_simps unit_prod)
   782 
   783 lemma mult_unit_dvd_iff:
   784   assumes "is_unit b"
   785   shows "a * b dvd c \<longleftrightarrow> a dvd c"
   786 proof
   787   assume "a * b dvd c"
   788   with assms show "a dvd c"
   789     by (simp add: dvd_mult_left)
   790 next
   791   assume "a dvd c"
   792   then obtain k where "c = a * k" ..
   793   with assms have "c = (a * b) * (1 div b * k)"
   794     by (simp add: mult_ac)
   795   then show "a * b dvd c" by (rule dvdI)
   796 qed
   797 
   798 lemma dvd_mult_unit_iff:
   799   assumes "is_unit b"
   800   shows "a dvd c * b \<longleftrightarrow> a dvd c"
   801 proof
   802   assume "a dvd c * b"
   803   with assms have "c * b dvd c * (b * (1 div b))"
   804     by (subst mult_assoc [symmetric]) simp
   805   also from `is_unit b` have "b * (1 div b) = 1" by (rule is_unitE) simp
   806   finally have "c * b dvd c" by simp
   807   with `a dvd c * b` show "a dvd c" by (rule dvd_trans)
   808 next
   809   assume "a dvd c"
   810   then show "a dvd c * b" by simp
   811 qed
   812 
   813 lemma div_unit_dvd_iff:
   814   "is_unit b \<Longrightarrow> a div b dvd c \<longleftrightarrow> a dvd c"
   815   by (erule is_unitE [of _ a]) (auto simp add: mult_unit_dvd_iff)
   816 
   817 lemma dvd_div_unit_iff:
   818   "is_unit b \<Longrightarrow> a dvd c div b \<longleftrightarrow> a dvd c"
   819   by (erule is_unitE [of _ c]) (simp add: dvd_mult_unit_iff)
   820 
   821 lemmas unit_dvd_iff = mult_unit_dvd_iff div_unit_dvd_iff
   822   dvd_mult_unit_iff dvd_div_unit_iff -- \<open>FIXME consider fact collection\<close>
   823 
   824 lemma unit_mult_div_div [simp]:
   825   "is_unit a \<Longrightarrow> b * (1 div a) = b div a"
   826   by (erule is_unitE [of _ b]) simp
   827 
   828 lemma unit_div_mult_self [simp]:
   829   "is_unit a \<Longrightarrow> b div a * a = b"
   830   by (rule dvd_div_mult_self) auto
   831 
   832 lemma unit_div_1_div_1 [simp]:
   833   "is_unit a \<Longrightarrow> 1 div (1 div a) = a"
   834   by (erule is_unitE) simp
   835 
   836 lemma unit_div_mult_swap:
   837   "is_unit c \<Longrightarrow> a * (b div c) = (a * b) div c"
   838   by (erule unit_dvdE [of _ b]) (simp add: mult.left_commute [of _ c])
   839 
   840 lemma unit_div_commute:
   841   "is_unit b \<Longrightarrow> (a div b) * c = (a * c) div b"
   842   using unit_div_mult_swap [of b c a] by (simp add: ac_simps)
   843 
   844 lemma unit_eq_div1:
   845   "is_unit b \<Longrightarrow> a div b = c \<longleftrightarrow> a = c * b"
   846   by (auto elim: is_unitE)
   847 
   848 lemma unit_eq_div2:
   849   "is_unit b \<Longrightarrow> a = c div b \<longleftrightarrow> a * b = c"
   850   using unit_eq_div1 [of b c a] by auto
   851 
   852 lemma unit_mult_left_cancel:
   853   assumes "is_unit a"
   854   shows "a * b = a * c \<longleftrightarrow> b = c" (is "?P \<longleftrightarrow> ?Q")
   855   using assms mult_cancel_left [of a b c] by auto
   856 
   857 lemma unit_mult_right_cancel:
   858   "is_unit a \<Longrightarrow> b * a = c * a \<longleftrightarrow> b = c"
   859   using unit_mult_left_cancel [of a b c] by (auto simp add: ac_simps)
   860 
   861 lemma unit_div_cancel:
   862   assumes "is_unit a"
   863   shows "b div a = c div a \<longleftrightarrow> b = c"
   864 proof -
   865   from assms have "is_unit (1 div a)" by simp
   866   then have "b * (1 div a) = c * (1 div a) \<longleftrightarrow> b = c"
   867     by (rule unit_mult_right_cancel)
   868   with assms show ?thesis by simp
   869 qed
   870 
   871 lemma is_unit_div_mult2_eq:
   872   assumes "is_unit b" and "is_unit c"
   873   shows "a div (b * c) = a div b div c"
   874 proof -
   875   from assms have "is_unit (b * c)" by (simp add: unit_prod)
   876   then have "b * c dvd a"
   877     by (rule unit_imp_dvd)
   878   then show ?thesis
   879     by (rule dvd_div_mult2_eq)
   880 qed
   881 
   882 lemmas unit_simps = mult_unit_dvd_iff div_unit_dvd_iff dvd_mult_unit_iff
   883   dvd_div_unit_iff unit_div_mult_swap unit_div_commute
   884   unit_mult_left_cancel unit_mult_right_cancel unit_div_cancel
   885   unit_eq_div1 unit_eq_div2
   886 
   887 lemma is_unit_divide_mult_cancel_left:
   888   assumes "a \<noteq> 0" and "is_unit b"
   889   shows "a div (a * b) = 1 div b"
   890 proof -
   891   from assms have "a div (a * b) = a div a div b"
   892     by (simp add: mult_unit_dvd_iff dvd_div_mult2_eq)
   893   with assms show ?thesis by simp
   894 qed
   895 
   896 lemma is_unit_divide_mult_cancel_right:
   897   assumes "a \<noteq> 0" and "is_unit b"
   898   shows "a div (b * a) = 1 div b"
   899   using assms is_unit_divide_mult_cancel_left [of a b] by (simp add: ac_simps)
   900 
   901 end
   902 
   903 class normalization_semidom = algebraic_semidom +
   904   fixes normalize :: "'a \<Rightarrow> 'a"
   905     and unit_factor :: "'a \<Rightarrow> 'a"
   906   assumes unit_factor_mult_normalize [simp]: "unit_factor a * normalize a = a"
   907   assumes normalize_0 [simp]: "normalize 0 = 0"
   908     and unit_factor_0 [simp]: "unit_factor 0 = 0"
   909   assumes is_unit_normalize:
   910     "is_unit a  \<Longrightarrow> normalize a = 1"
   911   assumes unit_factor_is_unit [iff]: 
   912     "a \<noteq> 0 \<Longrightarrow> is_unit (unit_factor a)"
   913   assumes unit_factor_mult: "unit_factor (a * b) = unit_factor a * unit_factor b"
   914 begin
   915 
   916 text \<open>
   917   Class @{class normalization_semidom} cultivates the idea that
   918   each integral domain can be split into equivalence classes
   919   whose representants are associated, i.e. divide each other.
   920   @{const normalize} specifies a canonical representant for each equivalence
   921   class.  The rationale behind this is that it is easier to reason about equality
   922   than equivalences, hence we prefer to think about equality of normalized
   923   values rather than associated elements.
   924 \<close>
   925 
   926 lemma unit_factor_dvd [simp]:
   927   "a \<noteq> 0 \<Longrightarrow> unit_factor a dvd b"
   928   by (rule unit_imp_dvd) simp
   929 
   930 lemma unit_factor_self [simp]:
   931   "unit_factor a dvd a"
   932   by (cases "a = 0") simp_all 
   933   
   934 lemma normalize_mult_unit_factor [simp]:
   935   "normalize a * unit_factor a = a"
   936   using unit_factor_mult_normalize [of a] by (simp add: ac_simps)
   937 
   938 lemma normalize_eq_0_iff [simp]:
   939   "normalize a = 0 \<longleftrightarrow> a = 0" (is "?P \<longleftrightarrow> ?Q")
   940 proof
   941   assume ?P
   942   moreover have "unit_factor a * normalize a = a" by simp
   943   ultimately show ?Q by simp 
   944 next
   945   assume ?Q then show ?P by simp
   946 qed
   947 
   948 lemma unit_factor_eq_0_iff [simp]:
   949   "unit_factor a = 0 \<longleftrightarrow> a = 0" (is "?P \<longleftrightarrow> ?Q")
   950 proof
   951   assume ?P
   952   moreover have "unit_factor a * normalize a = a" by simp
   953   ultimately show ?Q by simp 
   954 next
   955   assume ?Q then show ?P by simp
   956 qed
   957 
   958 lemma is_unit_unit_factor:
   959   assumes "is_unit a" shows "unit_factor a = a"
   960 proof - 
   961   from assms have "normalize a = 1" by (rule is_unit_normalize)
   962   moreover from unit_factor_mult_normalize have "unit_factor a * normalize a = a" .
   963   ultimately show ?thesis by simp
   964 qed
   965 
   966 lemma unit_factor_1 [simp]:
   967   "unit_factor 1 = 1"
   968   by (rule is_unit_unit_factor) simp
   969 
   970 lemma normalize_1 [simp]:
   971   "normalize 1 = 1"
   972   by (rule is_unit_normalize) simp
   973 
   974 lemma normalize_1_iff:
   975   "normalize a = 1 \<longleftrightarrow> is_unit a" (is "?P \<longleftrightarrow> ?Q")
   976 proof
   977   assume ?Q then show ?P by (rule is_unit_normalize)
   978 next
   979   assume ?P
   980   then have "a \<noteq> 0" by auto
   981   from \<open>?P\<close> have "unit_factor a * normalize a = unit_factor a * 1"
   982     by simp
   983   then have "unit_factor a = a"
   984     by simp
   985   moreover have "is_unit (unit_factor a)"
   986     using \<open>a \<noteq> 0\<close> by simp
   987   ultimately show ?Q by simp
   988 qed
   989   
   990 lemma div_normalize [simp]:
   991   "a div normalize a = unit_factor a"
   992 proof (cases "a = 0")
   993   case True then show ?thesis by simp
   994 next
   995   case False then have "normalize a \<noteq> 0" by simp 
   996   with nonzero_mult_divide_cancel_right
   997   have "unit_factor a * normalize a div normalize a = unit_factor a" by blast
   998   then show ?thesis by simp
   999 qed
  1000 
  1001 lemma div_unit_factor [simp]:
  1002   "a div unit_factor a = normalize a"
  1003 proof (cases "a = 0")
  1004   case True then show ?thesis by simp
  1005 next
  1006   case False then have "unit_factor a \<noteq> 0" by simp 
  1007   with nonzero_mult_divide_cancel_left
  1008   have "unit_factor a * normalize a div unit_factor a = normalize a" by blast
  1009   then show ?thesis by simp
  1010 qed
  1011 
  1012 lemma normalize_div [simp]:
  1013   "normalize a div a = 1 div unit_factor a"
  1014 proof (cases "a = 0")
  1015   case True then show ?thesis by simp
  1016 next
  1017   case False
  1018   have "normalize a div a = normalize a div (unit_factor a * normalize a)"
  1019     by simp
  1020   also have "\<dots> = 1 div unit_factor a"
  1021     using False by (subst is_unit_divide_mult_cancel_right) simp_all
  1022   finally show ?thesis .
  1023 qed
  1024 
  1025 lemma mult_one_div_unit_factor [simp]:
  1026   "a * (1 div unit_factor b) = a div unit_factor b"
  1027   by (cases "b = 0") simp_all
  1028 
  1029 lemma normalize_mult:
  1030   "normalize (a * b) = normalize a * normalize b"
  1031 proof (cases "a = 0 \<or> b = 0")
  1032   case True then show ?thesis by auto
  1033 next
  1034   case False
  1035   from unit_factor_mult_normalize have "unit_factor (a * b) * normalize (a * b) = a * b" .
  1036   then have "normalize (a * b) = a * b div unit_factor (a * b)" by simp
  1037   also have "\<dots> = a * b div unit_factor (b * a)" by (simp add: ac_simps)
  1038   also have "\<dots> = a * b div unit_factor b div unit_factor a"
  1039     using False by (simp add: unit_factor_mult is_unit_div_mult2_eq [symmetric])
  1040   also have "\<dots> = a * (b div unit_factor b) div unit_factor a"
  1041     using False by (subst unit_div_mult_swap) simp_all
  1042   also have "\<dots> = normalize a * normalize b"
  1043     using False by (simp add: mult.commute [of a] mult.commute [of "normalize a"] unit_div_mult_swap [symmetric])
  1044   finally show ?thesis .
  1045 qed
  1046  
  1047 lemma unit_factor_idem [simp]:
  1048   "unit_factor (unit_factor a) = unit_factor a"
  1049   by (cases "a = 0") (auto intro: is_unit_unit_factor)
  1050 
  1051 lemma normalize_unit_factor [simp]:
  1052   "a \<noteq> 0 \<Longrightarrow> normalize (unit_factor a) = 1"
  1053   by (rule is_unit_normalize) simp
  1054   
  1055 lemma normalize_idem [simp]:
  1056   "normalize (normalize a) = normalize a"
  1057 proof (cases "a = 0")
  1058   case True then show ?thesis by simp
  1059 next
  1060   case False
  1061   have "normalize a = normalize (unit_factor a * normalize a)" by simp
  1062   also have "\<dots> = normalize (unit_factor a) * normalize (normalize a)"
  1063     by (simp only: normalize_mult)
  1064   finally show ?thesis using False by simp_all
  1065 qed
  1066 
  1067 lemma unit_factor_normalize [simp]:
  1068   assumes "a \<noteq> 0"
  1069   shows "unit_factor (normalize a) = 1"
  1070 proof -
  1071   from assms have "normalize a \<noteq> 0" by simp
  1072   have "unit_factor (normalize a) * normalize (normalize a) = normalize a"
  1073     by (simp only: unit_factor_mult_normalize)
  1074   then have "unit_factor (normalize a) * normalize a = normalize a"
  1075     by simp
  1076   with \<open>normalize a \<noteq> 0\<close>
  1077   have "unit_factor (normalize a) * normalize a div normalize a = normalize a div normalize a"
  1078     by simp
  1079   with \<open>normalize a \<noteq> 0\<close>
  1080   show ?thesis by simp
  1081 qed
  1082 
  1083 lemma dvd_unit_factor_div:
  1084   assumes "b dvd a"
  1085   shows "unit_factor (a div b) = unit_factor a div unit_factor b"
  1086 proof -
  1087   from assms have "a = a div b * b"
  1088     by simp
  1089   then have "unit_factor a = unit_factor (a div b * b)"
  1090     by simp
  1091   then show ?thesis
  1092     by (cases "b = 0") (simp_all add: unit_factor_mult)
  1093 qed
  1094 
  1095 lemma dvd_normalize_div:
  1096   assumes "b dvd a"
  1097   shows "normalize (a div b) = normalize a div normalize b"
  1098 proof -
  1099   from assms have "a = a div b * b"
  1100     by simp
  1101   then have "normalize a = normalize (a div b * b)"
  1102     by simp
  1103   then show ?thesis
  1104     by (cases "b = 0") (simp_all add: normalize_mult)
  1105 qed
  1106 
  1107 lemma normalize_dvd_iff [simp]:
  1108   "normalize a dvd b \<longleftrightarrow> a dvd b"
  1109 proof -
  1110   have "normalize a dvd b \<longleftrightarrow> unit_factor a * normalize a dvd b"
  1111     using mult_unit_dvd_iff [of "unit_factor a" "normalize a" b]
  1112       by (cases "a = 0") simp_all
  1113   then show ?thesis by simp
  1114 qed
  1115 
  1116 lemma dvd_normalize_iff [simp]:
  1117   "a dvd normalize b \<longleftrightarrow> a dvd b"
  1118 proof -
  1119   have "a dvd normalize  b \<longleftrightarrow> a dvd normalize b * unit_factor b"
  1120     using dvd_mult_unit_iff [of "unit_factor b" a "normalize b"]
  1121       by (cases "b = 0") simp_all
  1122   then show ?thesis by simp
  1123 qed
  1124 
  1125 text \<open>
  1126   We avoid an explicit definition of associated elements but prefer
  1127   explicit normalisation instead.  In theory we could define an abbreviation
  1128   like @{prop "associated a b \<longleftrightarrow> normalize a = normalize b"} but this is
  1129   counterproductive without suggestive infix syntax, which we do not want
  1130   to sacrifice for this purpose here.
  1131 \<close>
  1132 
  1133 lemma associatedI:
  1134   assumes "a dvd b" and "b dvd a"
  1135   shows "normalize a = normalize b"
  1136 proof (cases "a = 0 \<or> b = 0")
  1137   case True with assms show ?thesis by auto
  1138 next
  1139   case False
  1140   from \<open>a dvd b\<close> obtain c where b: "b = a * c" ..
  1141   moreover from \<open>b dvd a\<close> obtain d where a: "a = b * d" ..
  1142   ultimately have "b * 1 = b * (c * d)" by (simp add: ac_simps)
  1143   with False have "1 = c * d"
  1144     unfolding mult_cancel_left by simp
  1145   then have "is_unit c" and "is_unit d" by auto
  1146   with a b show ?thesis by (simp add: normalize_mult is_unit_normalize)
  1147 qed
  1148 
  1149 lemma associatedD1:
  1150   "normalize a = normalize b \<Longrightarrow> a dvd b"
  1151   using dvd_normalize_iff [of _ b, symmetric] normalize_dvd_iff [of a _, symmetric]
  1152   by simp
  1153 
  1154 lemma associatedD2:
  1155   "normalize a = normalize b \<Longrightarrow> b dvd a"
  1156   using dvd_normalize_iff [of _ a, symmetric] normalize_dvd_iff [of b _, symmetric]
  1157   by simp
  1158 
  1159 lemma associated_unit:
  1160   "normalize a = normalize b \<Longrightarrow> is_unit a \<Longrightarrow> is_unit b"
  1161   using dvd_unit_imp_unit by (auto dest!: associatedD1 associatedD2)
  1162 
  1163 lemma associated_iff_dvd:
  1164   "normalize a = normalize b \<longleftrightarrow> a dvd b \<and> b dvd a" (is "?P \<longleftrightarrow> ?Q")
  1165 proof
  1166   assume ?Q then show ?P by (auto intro!: associatedI)
  1167 next
  1168   assume ?P
  1169   then have "unit_factor a * normalize a = unit_factor a * normalize b"
  1170     by simp
  1171   then have *: "normalize b * unit_factor a = a"
  1172     by (simp add: ac_simps)
  1173   show ?Q
  1174   proof (cases "a = 0 \<or> b = 0")
  1175     case True with \<open>?P\<close> show ?thesis by auto
  1176   next
  1177     case False 
  1178     then have "b dvd normalize b * unit_factor a" and "normalize b * unit_factor a dvd b"
  1179       by (simp_all add: mult_unit_dvd_iff dvd_mult_unit_iff)
  1180     with * show ?thesis by simp
  1181   qed
  1182 qed
  1183 
  1184 lemma associated_eqI:
  1185   assumes "a dvd b" and "b dvd a"
  1186   assumes "normalize a = a" and "normalize b = b"
  1187   shows "a = b"
  1188 proof -
  1189   from assms have "normalize a = normalize b"
  1190     unfolding associated_iff_dvd by simp
  1191   with \<open>normalize a = a\<close> have "a = normalize b" by simp
  1192   with \<open>normalize b = b\<close> show "a = b" by simp
  1193 qed
  1194 
  1195 end
  1196 
  1197 class ordered_semiring = semiring + comm_monoid_add + ordered_ab_semigroup_add +
  1198   assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
  1199   assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"
  1200 begin
  1201 
  1202 lemma mult_mono:
  1203   "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * d"
  1204 apply (erule mult_right_mono [THEN order_trans], assumption)
  1205 apply (erule mult_left_mono, assumption)
  1206 done
  1207 
  1208 lemma mult_mono':
  1209   "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * d"
  1210 apply (rule mult_mono)
  1211 apply (fast intro: order_trans)+
  1212 done
  1213 
  1214 end
  1215 
  1216 class ordered_cancel_semiring = ordered_semiring + cancel_comm_monoid_add
  1217 begin
  1218 
  1219 subclass semiring_0_cancel ..
  1220 
  1221 lemma mult_nonneg_nonneg[simp]: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b"
  1222 using mult_left_mono [of 0 b a] by simp
  1223 
  1224 lemma mult_nonneg_nonpos: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> a * b \<le> 0"
  1225 using mult_left_mono [of b 0 a] by simp
  1226 
  1227 lemma mult_nonpos_nonneg: "a \<le> 0 \<Longrightarrow> 0 \<le> b \<Longrightarrow> a * b \<le> 0"
  1228 using mult_right_mono [of a 0 b] by simp
  1229 
  1230 text {* Legacy - use @{text mult_nonpos_nonneg} *}
  1231 lemma mult_nonneg_nonpos2: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> b * a \<le> 0"
  1232 by (drule mult_right_mono [of b 0], auto)
  1233 
  1234 lemma split_mult_neg_le: "(0 \<le> a & b \<le> 0) | (a \<le> 0 & 0 \<le> b) \<Longrightarrow> a * b \<le> 0"
  1235 by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)
  1236 
  1237 end
  1238 
  1239 class linordered_semiring = ordered_semiring + linordered_cancel_ab_semigroup_add
  1240 begin
  1241 
  1242 subclass ordered_cancel_semiring ..
  1243 
  1244 subclass ordered_comm_monoid_add ..
  1245 
  1246 lemma mult_left_less_imp_less:
  1247   "c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
  1248 by (force simp add: mult_left_mono not_le [symmetric])
  1249 
  1250 lemma mult_right_less_imp_less:
  1251   "a * c < b * c \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
  1252 by (force simp add: mult_right_mono not_le [symmetric])
  1253 
  1254 end
  1255 
  1256 class linordered_semiring_1 = linordered_semiring + semiring_1
  1257 begin
  1258 
  1259 lemma convex_bound_le:
  1260   assumes "x \<le> a" "y \<le> a" "0 \<le> u" "0 \<le> v" "u + v = 1"
  1261   shows "u * x + v * y \<le> a"
  1262 proof-
  1263   from assms have "u * x + v * y \<le> u * a + v * a"
  1264     by (simp add: add_mono mult_left_mono)
  1265   thus ?thesis using assms unfolding distrib_right[symmetric] by simp
  1266 qed
  1267 
  1268 end
  1269 
  1270 class linordered_semiring_strict = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add +
  1271   assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
  1272   assumes mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c"
  1273 begin
  1274 
  1275 subclass semiring_0_cancel ..
  1276 
  1277 subclass linordered_semiring
  1278 proof
  1279   fix a b c :: 'a
  1280   assume A: "a \<le> b" "0 \<le> c"
  1281   from A show "c * a \<le> c * b"
  1282     unfolding le_less
  1283     using mult_strict_left_mono by (cases "c = 0") auto
  1284   from A show "a * c \<le> b * c"
  1285     unfolding le_less
  1286     using mult_strict_right_mono by (cases "c = 0") auto
  1287 qed
  1288 
  1289 lemma mult_left_le_imp_le:
  1290   "c * a \<le> c * b \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
  1291 by (force simp add: mult_strict_left_mono _not_less [symmetric])
  1292 
  1293 lemma mult_right_le_imp_le:
  1294   "a * c \<le> b * c \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
  1295 by (force simp add: mult_strict_right_mono not_less [symmetric])
  1296 
  1297 lemma mult_pos_pos[simp]: "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a * b"
  1298 using mult_strict_left_mono [of 0 b a] by simp
  1299 
  1300 lemma mult_pos_neg: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> a * b < 0"
  1301 using mult_strict_left_mono [of b 0 a] by simp
  1302 
  1303 lemma mult_neg_pos: "a < 0 \<Longrightarrow> 0 < b \<Longrightarrow> a * b < 0"
  1304 using mult_strict_right_mono [of a 0 b] by simp
  1305 
  1306 text {* Legacy - use @{text mult_neg_pos} *}
  1307 lemma mult_pos_neg2: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> b * a < 0"
  1308 by (drule mult_strict_right_mono [of b 0], auto)
  1309 
  1310 lemma zero_less_mult_pos:
  1311   "0 < a * b \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"
  1312 apply (cases "b\<le>0")
  1313  apply (auto simp add: le_less not_less)
  1314 apply (drule_tac mult_pos_neg [of a b])
  1315  apply (auto dest: less_not_sym)
  1316 done
  1317 
  1318 lemma zero_less_mult_pos2:
  1319   "0 < b * a \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"
  1320 apply (cases "b\<le>0")
  1321  apply (auto simp add: le_less not_less)
  1322 apply (drule_tac mult_pos_neg2 [of a b])
  1323  apply (auto dest: less_not_sym)
  1324 done
  1325 
  1326 text{*Strict monotonicity in both arguments*}
  1327 lemma mult_strict_mono:
  1328   assumes "a < b" and "c < d" and "0 < b" and "0 \<le> c"
  1329   shows "a * c < b * d"
  1330   using assms apply (cases "c=0")
  1331   apply (simp)
  1332   apply (erule mult_strict_right_mono [THEN less_trans])
  1333   apply (force simp add: le_less)
  1334   apply (erule mult_strict_left_mono, assumption)
  1335   done
  1336 
  1337 text{*This weaker variant has more natural premises*}
  1338 lemma mult_strict_mono':
  1339   assumes "a < b" and "c < d" and "0 \<le> a" and "0 \<le> c"
  1340   shows "a * c < b * d"
  1341 by (rule mult_strict_mono) (insert assms, auto)
  1342 
  1343 lemma mult_less_le_imp_less:
  1344   assumes "a < b" and "c \<le> d" and "0 \<le> a" and "0 < c"
  1345   shows "a * c < b * d"
  1346   using assms apply (subgoal_tac "a * c < b * c")
  1347   apply (erule less_le_trans)
  1348   apply (erule mult_left_mono)
  1349   apply simp
  1350   apply (erule mult_strict_right_mono)
  1351   apply assumption
  1352   done
  1353 
  1354 lemma mult_le_less_imp_less:
  1355   assumes "a \<le> b" and "c < d" and "0 < a" and "0 \<le> c"
  1356   shows "a * c < b * d"
  1357   using assms apply (subgoal_tac "a * c \<le> b * c")
  1358   apply (erule le_less_trans)
  1359   apply (erule mult_strict_left_mono)
  1360   apply simp
  1361   apply (erule mult_right_mono)
  1362   apply simp
  1363   done
  1364 
  1365 end
  1366 
  1367 class linordered_semiring_1_strict = linordered_semiring_strict + semiring_1
  1368 begin
  1369 
  1370 subclass linordered_semiring_1 ..
  1371 
  1372 lemma convex_bound_lt:
  1373   assumes "x < a" "y < a" "0 \<le> u" "0 \<le> v" "u + v = 1"
  1374   shows "u * x + v * y < a"
  1375 proof -
  1376   from assms have "u * x + v * y < u * a + v * a"
  1377     by (cases "u = 0")
  1378        (auto intro!: add_less_le_mono mult_strict_left_mono mult_left_mono)
  1379   thus ?thesis using assms unfolding distrib_right[symmetric] by simp
  1380 qed
  1381 
  1382 end
  1383 
  1384 class ordered_comm_semiring = comm_semiring_0 + ordered_ab_semigroup_add +
  1385   assumes comm_mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
  1386 begin
  1387 
  1388 subclass ordered_semiring
  1389 proof
  1390   fix a b c :: 'a
  1391   assume "a \<le> b" "0 \<le> c"
  1392   thus "c * a \<le> c * b" by (rule comm_mult_left_mono)
  1393   thus "a * c \<le> b * c" by (simp only: mult.commute)
  1394 qed
  1395 
  1396 end
  1397 
  1398 class ordered_cancel_comm_semiring = ordered_comm_semiring + cancel_comm_monoid_add
  1399 begin
  1400 
  1401 subclass comm_semiring_0_cancel ..
  1402 subclass ordered_comm_semiring ..
  1403 subclass ordered_cancel_semiring ..
  1404 
  1405 end
  1406 
  1407 class linordered_comm_semiring_strict = comm_semiring_0 + linordered_cancel_ab_semigroup_add +
  1408   assumes comm_mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
  1409 begin
  1410 
  1411 subclass linordered_semiring_strict
  1412 proof
  1413   fix a b c :: 'a
  1414   assume "a < b" "0 < c"
  1415   thus "c * a < c * b" by (rule comm_mult_strict_left_mono)
  1416   thus "a * c < b * c" by (simp only: mult.commute)
  1417 qed
  1418 
  1419 subclass ordered_cancel_comm_semiring
  1420 proof
  1421   fix a b c :: 'a
  1422   assume "a \<le> b" "0 \<le> c"
  1423   thus "c * a \<le> c * b"
  1424     unfolding le_less
  1425     using mult_strict_left_mono by (cases "c = 0") auto
  1426 qed
  1427 
  1428 end
  1429 
  1430 class ordered_ring = ring + ordered_cancel_semiring
  1431 begin
  1432 
  1433 subclass ordered_ab_group_add ..
  1434 
  1435 lemma less_add_iff1:
  1436   "a * e + c < b * e + d \<longleftrightarrow> (a - b) * e + c < d"
  1437 by (simp add: algebra_simps)
  1438 
  1439 lemma less_add_iff2:
  1440   "a * e + c < b * e + d \<longleftrightarrow> c < (b - a) * e + d"
  1441 by (simp add: algebra_simps)
  1442 
  1443 lemma le_add_iff1:
  1444   "a * e + c \<le> b * e + d \<longleftrightarrow> (a - b) * e + c \<le> d"
  1445 by (simp add: algebra_simps)
  1446 
  1447 lemma le_add_iff2:
  1448   "a * e + c \<le> b * e + d \<longleftrightarrow> c \<le> (b - a) * e + d"
  1449 by (simp add: algebra_simps)
  1450 
  1451 lemma mult_left_mono_neg:
  1452   "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> c * a \<le> c * b"
  1453   apply (drule mult_left_mono [of _ _ "- c"])
  1454   apply simp_all
  1455   done
  1456 
  1457 lemma mult_right_mono_neg:
  1458   "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> a * c \<le> b * c"
  1459   apply (drule mult_right_mono [of _ _ "- c"])
  1460   apply simp_all
  1461   done
  1462 
  1463 lemma mult_nonpos_nonpos: "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> 0 \<le> a * b"
  1464 using mult_right_mono_neg [of a 0 b] by simp
  1465 
  1466 lemma split_mult_pos_le:
  1467   "(0 \<le> a \<and> 0 \<le> b) \<or> (a \<le> 0 \<and> b \<le> 0) \<Longrightarrow> 0 \<le> a * b"
  1468 by (auto simp add: mult_nonpos_nonpos)
  1469 
  1470 end
  1471 
  1472 class linordered_ring = ring + linordered_semiring + linordered_ab_group_add + abs_if
  1473 begin
  1474 
  1475 subclass ordered_ring ..
  1476 
  1477 subclass ordered_ab_group_add_abs
  1478 proof
  1479   fix a b
  1480   show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
  1481     by (auto simp add: abs_if not_le not_less algebra_simps simp del: add.commute dest: add_neg_neg add_nonneg_nonneg)
  1482 qed (auto simp add: abs_if)
  1483 
  1484 lemma zero_le_square [simp]: "0 \<le> a * a"
  1485   using linear [of 0 a]
  1486   by (auto simp add: mult_nonpos_nonpos)
  1487 
  1488 lemma not_square_less_zero [simp]: "\<not> (a * a < 0)"
  1489   by (simp add: not_less)
  1490 
  1491 end
  1492 
  1493 class linordered_ring_strict = ring + linordered_semiring_strict
  1494   + ordered_ab_group_add + abs_if
  1495 begin
  1496 
  1497 subclass linordered_ring ..
  1498 
  1499 lemma mult_strict_left_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> c * a < c * b"
  1500 using mult_strict_left_mono [of b a "- c"] by simp
  1501 
  1502 lemma mult_strict_right_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> a * c < b * c"
  1503 using mult_strict_right_mono [of b a "- c"] by simp
  1504 
  1505 lemma mult_neg_neg: "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> 0 < a * b"
  1506 using mult_strict_right_mono_neg [of a 0 b] by simp
  1507 
  1508 subclass ring_no_zero_divisors
  1509 proof
  1510   fix a b
  1511   assume "a \<noteq> 0" then have A: "a < 0 \<or> 0 < a" by (simp add: neq_iff)
  1512   assume "b \<noteq> 0" then have B: "b < 0 \<or> 0 < b" by (simp add: neq_iff)
  1513   have "a * b < 0 \<or> 0 < a * b"
  1514   proof (cases "a < 0")
  1515     case True note A' = this
  1516     show ?thesis proof (cases "b < 0")
  1517       case True with A'
  1518       show ?thesis by (auto dest: mult_neg_neg)
  1519     next
  1520       case False with B have "0 < b" by auto
  1521       with A' show ?thesis by (auto dest: mult_strict_right_mono)
  1522     qed
  1523   next
  1524     case False with A have A': "0 < a" by auto
  1525     show ?thesis proof (cases "b < 0")
  1526       case True with A'
  1527       show ?thesis by (auto dest: mult_strict_right_mono_neg)
  1528     next
  1529       case False with B have "0 < b" by auto
  1530       with A' show ?thesis by auto
  1531     qed
  1532   qed
  1533   then show "a * b \<noteq> 0" by (simp add: neq_iff)
  1534 qed
  1535 
  1536 lemma zero_less_mult_iff: "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0"
  1537   by (cases a 0 b 0 rule: linorder_cases[case_product linorder_cases])
  1538      (auto simp add: mult_neg_neg not_less le_less dest: zero_less_mult_pos zero_less_mult_pos2)
  1539 
  1540 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"
  1541   by (auto simp add: eq_commute [of 0] le_less not_less zero_less_mult_iff)
  1542 
  1543 lemma mult_less_0_iff:
  1544   "a * b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b"
  1545   apply (insert zero_less_mult_iff [of "-a" b])
  1546   apply force
  1547   done
  1548 
  1549 lemma mult_le_0_iff:
  1550   "a * b \<le> 0 \<longleftrightarrow> 0 \<le> a \<and> b \<le> 0 \<or> a \<le> 0 \<and> 0 \<le> b"
  1551   apply (insert zero_le_mult_iff [of "-a" b])
  1552   apply force
  1553   done
  1554 
  1555 text{*Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"},
  1556    also with the relations @{text "\<le>"} and equality.*}
  1557 
  1558 text{*These ``disjunction'' versions produce two cases when the comparison is
  1559  an assumption, but effectively four when the comparison is a goal.*}
  1560 
  1561 lemma mult_less_cancel_right_disj:
  1562   "a * c < b * c \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"
  1563   apply (cases "c = 0")
  1564   apply (auto simp add: neq_iff mult_strict_right_mono
  1565                       mult_strict_right_mono_neg)
  1566   apply (auto simp add: not_less
  1567                       not_le [symmetric, of "a*c"]
  1568                       not_le [symmetric, of a])
  1569   apply (erule_tac [!] notE)
  1570   apply (auto simp add: less_imp_le mult_right_mono
  1571                       mult_right_mono_neg)
  1572   done
  1573 
  1574 lemma mult_less_cancel_left_disj:
  1575   "c * a < c * b \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"
  1576   apply (cases "c = 0")
  1577   apply (auto simp add: neq_iff mult_strict_left_mono
  1578                       mult_strict_left_mono_neg)
  1579   apply (auto simp add: not_less
  1580                       not_le [symmetric, of "c*a"]
  1581                       not_le [symmetric, of a])
  1582   apply (erule_tac [!] notE)
  1583   apply (auto simp add: less_imp_le mult_left_mono
  1584                       mult_left_mono_neg)
  1585   done
  1586 
  1587 text{*The ``conjunction of implication'' lemmas produce two cases when the
  1588 comparison is a goal, but give four when the comparison is an assumption.*}
  1589 
  1590 lemma mult_less_cancel_right:
  1591   "a * c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)"
  1592   using mult_less_cancel_right_disj [of a c b] by auto
  1593 
  1594 lemma mult_less_cancel_left:
  1595   "c * a < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)"
  1596   using mult_less_cancel_left_disj [of c a b] by auto
  1597 
  1598 lemma mult_le_cancel_right:
  1599    "a * c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
  1600 by (simp add: not_less [symmetric] mult_less_cancel_right_disj)
  1601 
  1602 lemma mult_le_cancel_left:
  1603   "c * a \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
  1604 by (simp add: not_less [symmetric] mult_less_cancel_left_disj)
  1605 
  1606 lemma mult_le_cancel_left_pos:
  1607   "0 < c \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> a \<le> b"
  1608 by (auto simp: mult_le_cancel_left)
  1609 
  1610 lemma mult_le_cancel_left_neg:
  1611   "c < 0 \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> b \<le> a"
  1612 by (auto simp: mult_le_cancel_left)
  1613 
  1614 lemma mult_less_cancel_left_pos:
  1615   "0 < c \<Longrightarrow> c * a < c * b \<longleftrightarrow> a < b"
  1616 by (auto simp: mult_less_cancel_left)
  1617 
  1618 lemma mult_less_cancel_left_neg:
  1619   "c < 0 \<Longrightarrow> c * a < c * b \<longleftrightarrow> b < a"
  1620 by (auto simp: mult_less_cancel_left)
  1621 
  1622 end
  1623 
  1624 lemmas mult_sign_intros =
  1625   mult_nonneg_nonneg mult_nonneg_nonpos
  1626   mult_nonpos_nonneg mult_nonpos_nonpos
  1627   mult_pos_pos mult_pos_neg
  1628   mult_neg_pos mult_neg_neg
  1629 
  1630 class ordered_comm_ring = comm_ring + ordered_comm_semiring
  1631 begin
  1632 
  1633 subclass ordered_ring ..
  1634 subclass ordered_cancel_comm_semiring ..
  1635 
  1636 end
  1637 
  1638 class linordered_semidom = semidom + linordered_comm_semiring_strict +
  1639   assumes zero_less_one [simp]: "0 < 1"
  1640   assumes le_add_diff_inverse2 [simp]: "b \<le> a \<Longrightarrow> a - b + b = a"
  1641 begin
  1642 
  1643 text {* Addition is the inverse of subtraction. *}
  1644 
  1645 lemma le_add_diff_inverse [simp]: "b \<le> a \<Longrightarrow> b + (a - b) = a"
  1646   by (frule le_add_diff_inverse2) (simp add: add.commute)
  1647 
  1648 lemma add_diff_inverse: "~ a<b \<Longrightarrow> b + (a - b) = a"
  1649   by simp
  1650 
  1651 lemma add_le_imp_le_diff: 
  1652   shows "i + k \<le> n \<Longrightarrow> i \<le> n - k"
  1653   apply (subst add_le_cancel_right [where c=k, symmetric])
  1654   apply (frule le_add_diff_inverse2)
  1655   apply (simp only: add.assoc [symmetric])
  1656   using add_implies_diff by fastforce
  1657 
  1658 lemma add_le_add_imp_diff_le: 
  1659   assumes a1: "i + k \<le> n"
  1660       and a2: "n \<le> j + k"
  1661   shows "\<lbrakk>i + k \<le> n; n \<le> j + k\<rbrakk> \<Longrightarrow> n - k \<le> j"
  1662 proof -
  1663   have "n - (i + k) + (i + k) = n"
  1664     using a1 by simp
  1665   moreover have "n - k = n - k - i + i"
  1666     using a1 by (simp add: add_le_imp_le_diff)
  1667   ultimately show ?thesis
  1668     using a2
  1669     apply (simp add: add.assoc [symmetric])
  1670     apply (rule add_le_imp_le_diff [of _ k "j+k", simplified add_diff_cancel_right'])
  1671     by (simp add: add.commute diff_diff_add)
  1672 qed
  1673 
  1674 lemma pos_add_strict:
  1675   shows "0 < a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
  1676   using add_strict_mono [of 0 a b c] by simp
  1677 
  1678 lemma zero_le_one [simp]: "0 \<le> 1"
  1679 by (rule zero_less_one [THEN less_imp_le])
  1680 
  1681 lemma not_one_le_zero [simp]: "\<not> 1 \<le> 0"
  1682 by (simp add: not_le)
  1683 
  1684 lemma not_one_less_zero [simp]: "\<not> 1 < 0"
  1685 by (simp add: not_less)
  1686 
  1687 lemma less_1_mult:
  1688   assumes "1 < m" and "1 < n"
  1689   shows "1 < m * n"
  1690   using assms mult_strict_mono [of 1 m 1 n]
  1691     by (simp add:  less_trans [OF zero_less_one])
  1692 
  1693 lemma mult_left_le: "c \<le> 1 \<Longrightarrow> 0 \<le> a \<Longrightarrow> a * c \<le> a"
  1694   using mult_left_mono[of c 1 a] by simp
  1695 
  1696 lemma mult_le_one: "a \<le> 1 \<Longrightarrow> 0 \<le> b \<Longrightarrow> b \<le> 1 \<Longrightarrow> a * b \<le> 1"
  1697   using mult_mono[of a 1 b 1] by simp
  1698 
  1699 end
  1700 
  1701 class linordered_idom = comm_ring_1 +
  1702   linordered_comm_semiring_strict + ordered_ab_group_add +
  1703   abs_if + sgn_if
  1704 begin
  1705 
  1706 subclass linordered_semiring_1_strict ..
  1707 subclass linordered_ring_strict ..
  1708 subclass ordered_comm_ring ..
  1709 subclass idom ..
  1710 
  1711 subclass linordered_semidom
  1712 proof
  1713   have "0 \<le> 1 * 1" by (rule zero_le_square)
  1714   thus "0 < 1" by (simp add: le_less)
  1715   show "\<And>b a. b \<le> a \<Longrightarrow> a - b + b = a"
  1716     by simp
  1717 qed
  1718 
  1719 lemma linorder_neqE_linordered_idom:
  1720   assumes "x \<noteq> y" obtains "x < y" | "y < x"
  1721   using assms by (rule neqE)
  1722 
  1723 text {* These cancellation simprules also produce two cases when the comparison is a goal. *}
  1724 
  1725 lemma mult_le_cancel_right1:
  1726   "c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)"
  1727 by (insert mult_le_cancel_right [of 1 c b], simp)
  1728 
  1729 lemma mult_le_cancel_right2:
  1730   "a * c \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)"
  1731 by (insert mult_le_cancel_right [of a c 1], simp)
  1732 
  1733 lemma mult_le_cancel_left1:
  1734   "c \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)"
  1735 by (insert mult_le_cancel_left [of c 1 b], simp)
  1736 
  1737 lemma mult_le_cancel_left2:
  1738   "c * a \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)"
  1739 by (insert mult_le_cancel_left [of c a 1], simp)
  1740 
  1741 lemma mult_less_cancel_right1:
  1742   "c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)"
  1743 by (insert mult_less_cancel_right [of 1 c b], simp)
  1744 
  1745 lemma mult_less_cancel_right2:
  1746   "a * c < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"
  1747 by (insert mult_less_cancel_right [of a c 1], simp)
  1748 
  1749 lemma mult_less_cancel_left1:
  1750   "c < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)"
  1751 by (insert mult_less_cancel_left [of c 1 b], simp)
  1752 
  1753 lemma mult_less_cancel_left2:
  1754   "c * a < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"
  1755 by (insert mult_less_cancel_left [of c a 1], simp)
  1756 
  1757 lemma sgn_sgn [simp]:
  1758   "sgn (sgn a) = sgn a"
  1759 unfolding sgn_if by simp
  1760 
  1761 lemma sgn_0_0:
  1762   "sgn a = 0 \<longleftrightarrow> a = 0"
  1763 unfolding sgn_if by simp
  1764 
  1765 lemma sgn_1_pos:
  1766   "sgn a = 1 \<longleftrightarrow> a > 0"
  1767 unfolding sgn_if by simp
  1768 
  1769 lemma sgn_1_neg:
  1770   "sgn a = - 1 \<longleftrightarrow> a < 0"
  1771 unfolding sgn_if by auto
  1772 
  1773 lemma sgn_pos [simp]:
  1774   "0 < a \<Longrightarrow> sgn a = 1"
  1775 unfolding sgn_1_pos .
  1776 
  1777 lemma sgn_neg [simp]:
  1778   "a < 0 \<Longrightarrow> sgn a = - 1"
  1779 unfolding sgn_1_neg .
  1780 
  1781 lemma sgn_times:
  1782   "sgn (a * b) = sgn a * sgn b"
  1783 by (auto simp add: sgn_if zero_less_mult_iff)
  1784 
  1785 lemma abs_sgn: "\<bar>k\<bar> = k * sgn k"
  1786 unfolding sgn_if abs_if by auto
  1787 
  1788 lemma sgn_greater [simp]:
  1789   "0 < sgn a \<longleftrightarrow> 0 < a"
  1790   unfolding sgn_if by auto
  1791 
  1792 lemma sgn_less [simp]:
  1793   "sgn a < 0 \<longleftrightarrow> a < 0"
  1794   unfolding sgn_if by auto
  1795 
  1796 lemma abs_dvd_iff [simp]: "\<bar>m\<bar> dvd k \<longleftrightarrow> m dvd k"
  1797   by (simp add: abs_if)
  1798 
  1799 lemma dvd_abs_iff [simp]: "m dvd \<bar>k\<bar> \<longleftrightarrow> m dvd k"
  1800   by (simp add: abs_if)
  1801 
  1802 lemma dvd_if_abs_eq:
  1803   "\<bar>l\<bar> = \<bar>k\<bar> \<Longrightarrow> l dvd k"
  1804 by(subst abs_dvd_iff[symmetric]) simp
  1805 
  1806 text {* The following lemmas can be proven in more general structures, but
  1807 are dangerous as simp rules in absence of @{thm neg_equal_zero},
  1808 @{thm neg_less_pos}, @{thm neg_less_eq_nonneg}. *}
  1809 
  1810 lemma equation_minus_iff_1 [simp, no_atp]:
  1811   "1 = - a \<longleftrightarrow> a = - 1"
  1812   by (fact equation_minus_iff)
  1813 
  1814 lemma minus_equation_iff_1 [simp, no_atp]:
  1815   "- a = 1 \<longleftrightarrow> a = - 1"
  1816   by (subst minus_equation_iff, auto)
  1817 
  1818 lemma le_minus_iff_1 [simp, no_atp]:
  1819   "1 \<le> - b \<longleftrightarrow> b \<le> - 1"
  1820   by (fact le_minus_iff)
  1821 
  1822 lemma minus_le_iff_1 [simp, no_atp]:
  1823   "- a \<le> 1 \<longleftrightarrow> - 1 \<le> a"
  1824   by (fact minus_le_iff)
  1825 
  1826 lemma less_minus_iff_1 [simp, no_atp]:
  1827   "1 < - b \<longleftrightarrow> b < - 1"
  1828   by (fact less_minus_iff)
  1829 
  1830 lemma minus_less_iff_1 [simp, no_atp]:
  1831   "- a < 1 \<longleftrightarrow> - 1 < a"
  1832   by (fact minus_less_iff)
  1833 
  1834 end
  1835 
  1836 text {* Simprules for comparisons where common factors can be cancelled. *}
  1837 
  1838 lemmas mult_compare_simps =
  1839     mult_le_cancel_right mult_le_cancel_left
  1840     mult_le_cancel_right1 mult_le_cancel_right2
  1841     mult_le_cancel_left1 mult_le_cancel_left2
  1842     mult_less_cancel_right mult_less_cancel_left
  1843     mult_less_cancel_right1 mult_less_cancel_right2
  1844     mult_less_cancel_left1 mult_less_cancel_left2
  1845     mult_cancel_right mult_cancel_left
  1846     mult_cancel_right1 mult_cancel_right2
  1847     mult_cancel_left1 mult_cancel_left2
  1848 
  1849 text {* Reasoning about inequalities with division *}
  1850 
  1851 context linordered_semidom
  1852 begin
  1853 
  1854 lemma less_add_one: "a < a + 1"
  1855 proof -
  1856   have "a + 0 < a + 1"
  1857     by (blast intro: zero_less_one add_strict_left_mono)
  1858   thus ?thesis by simp
  1859 qed
  1860 
  1861 lemma zero_less_two: "0 < 1 + 1"
  1862 by (blast intro: less_trans zero_less_one less_add_one)
  1863 
  1864 end
  1865 
  1866 context linordered_idom
  1867 begin
  1868 
  1869 lemma mult_right_le_one_le:
  1870   "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> x * y \<le> x"
  1871   by (rule mult_left_le)
  1872 
  1873 lemma mult_left_le_one_le:
  1874   "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> y * x \<le> x"
  1875   by (auto simp add: mult_le_cancel_right2)
  1876 
  1877 end
  1878 
  1879 text {* Absolute Value *}
  1880 
  1881 context linordered_idom
  1882 begin
  1883 
  1884 lemma mult_sgn_abs:
  1885   "sgn x * \<bar>x\<bar> = x"
  1886   unfolding abs_if sgn_if by auto
  1887 
  1888 lemma abs_one [simp]:
  1889   "\<bar>1\<bar> = 1"
  1890   by (simp add: abs_if)
  1891 
  1892 end
  1893 
  1894 class ordered_ring_abs = ordered_ring + ordered_ab_group_add_abs +
  1895   assumes abs_eq_mult:
  1896     "(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>"
  1897 
  1898 context linordered_idom
  1899 begin
  1900 
  1901 subclass ordered_ring_abs proof
  1902 qed (auto simp add: abs_if not_less mult_less_0_iff)
  1903 
  1904 lemma abs_mult:
  1905   "\<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>"
  1906   by (rule abs_eq_mult) auto
  1907 
  1908 lemma abs_mult_self:
  1909   "\<bar>a\<bar> * \<bar>a\<bar> = a * a"
  1910   by (simp add: abs_if)
  1911 
  1912 lemma abs_mult_less:
  1913   "\<bar>a\<bar> < c \<Longrightarrow> \<bar>b\<bar> < d \<Longrightarrow> \<bar>a\<bar> * \<bar>b\<bar> < c * d"
  1914 proof -
  1915   assume ac: "\<bar>a\<bar> < c"
  1916   hence cpos: "0<c" by (blast intro: le_less_trans abs_ge_zero)
  1917   assume "\<bar>b\<bar> < d"
  1918   thus ?thesis by (simp add: ac cpos mult_strict_mono)
  1919 qed
  1920 
  1921 lemma abs_less_iff:
  1922   "\<bar>a\<bar> < b \<longleftrightarrow> a < b \<and> - a < b"
  1923   by (simp add: less_le abs_le_iff) (auto simp add: abs_if)
  1924 
  1925 lemma abs_mult_pos:
  1926   "0 \<le> x \<Longrightarrow> \<bar>y\<bar> * x = \<bar>y * x\<bar>"
  1927   by (simp add: abs_mult)
  1928 
  1929 lemma abs_diff_less_iff:
  1930   "\<bar>x - a\<bar> < r \<longleftrightarrow> a - r < x \<and> x < a + r"
  1931   by (auto simp add: diff_less_eq ac_simps abs_less_iff)
  1932 
  1933 lemma abs_diff_le_iff:
  1934    "\<bar>x - a\<bar> \<le> r \<longleftrightarrow> a - r \<le> x \<and> x \<le> a + r"
  1935   by (auto simp add: diff_le_eq ac_simps abs_le_iff)
  1936 
  1937 end
  1938 
  1939 hide_fact (open) comm_mult_left_mono comm_mult_strict_left_mono distrib
  1940 
  1941 code_identifier
  1942   code_module Rings \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
  1943 
  1944 end