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