src/HOL/Rings.thy
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (21 months ago)
changeset 66695 91500c024c7f
parent 65811 2653f1cd8775
child 66793 deabce3ccf1f
permissions -rw-r--r--
tuned;
     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   then have "- a div b = (b * - c) div b"
   744     by simp
   745   from False also have "\<dots> = - c"
   746     by (rule nonzero_mult_div_cancel_left)  
   747   with False \<open>a = b * c\<close> show ?thesis
   748     by simp
   749 qed
   750 
   751 lemma dvd_div_neg:
   752   assumes "b dvd a"
   753   shows "a div - b = - (a div b)"
   754 proof (cases "b = 0")
   755   case True
   756   then show ?thesis by simp
   757 next
   758   case False
   759   then have "- b \<noteq> 0"
   760     by simp
   761   from assms obtain c where "a = b * c" ..
   762   then have "a div - b = (- b * - c) div - b"
   763     by simp
   764   from \<open>- b \<noteq> 0\<close> also have "\<dots> = - c"
   765     by (rule nonzero_mult_div_cancel_left)  
   766   with False \<open>a = b * c\<close> show ?thesis
   767     by simp
   768 qed
   769 
   770 end
   771 
   772 class algebraic_semidom = semidom_divide
   773 begin
   774 
   775 text \<open>
   776   Class @{class algebraic_semidom} enriches a integral domain
   777   by notions from algebra, like units in a ring.
   778   It is a separate class to avoid spoiling fields with notions
   779   which are degenerated there.
   780 \<close>
   781 
   782 lemma dvd_times_left_cancel_iff [simp]:
   783   assumes "a \<noteq> 0"
   784   shows "a * b dvd a * c \<longleftrightarrow> b dvd c"
   785     (is "?lhs \<longleftrightarrow> ?rhs")
   786 proof
   787   assume ?lhs
   788   then obtain d where "a * c = a * b * d" ..
   789   with assms have "c = b * d" by (simp add: ac_simps)
   790   then show ?rhs ..
   791 next
   792   assume ?rhs
   793   then obtain d where "c = b * d" ..
   794   then have "a * c = a * b * d" by (simp add: ac_simps)
   795   then show ?lhs ..
   796 qed
   797 
   798 lemma dvd_times_right_cancel_iff [simp]:
   799   assumes "a \<noteq> 0"
   800   shows "b * a dvd c * a \<longleftrightarrow> b dvd c"
   801   using dvd_times_left_cancel_iff [of a b c] assms by (simp add: ac_simps)
   802 
   803 lemma div_dvd_iff_mult:
   804   assumes "b \<noteq> 0" and "b dvd a"
   805   shows "a div b dvd c \<longleftrightarrow> a dvd c * b"
   806 proof -
   807   from \<open>b dvd a\<close> obtain d where "a = b * d" ..
   808   with \<open>b \<noteq> 0\<close> show ?thesis by (simp add: ac_simps)
   809 qed
   810 
   811 lemma dvd_div_iff_mult:
   812   assumes "c \<noteq> 0" and "c dvd b"
   813   shows "a dvd b div c \<longleftrightarrow> a * c dvd b"
   814 proof -
   815   from \<open>c dvd b\<close> obtain d where "b = c * d" ..
   816   with \<open>c \<noteq> 0\<close> show ?thesis by (simp add: mult.commute [of a])
   817 qed
   818 
   819 lemma div_dvd_div [simp]:
   820   assumes "a dvd b" and "a dvd c"
   821   shows "b div a dvd c div a \<longleftrightarrow> b dvd c"
   822 proof (cases "a = 0")
   823   case True
   824   with assms show ?thesis by simp
   825 next
   826   case False
   827   moreover from assms obtain k l where "b = a * k" and "c = a * l"
   828     by (auto elim!: dvdE)
   829   ultimately show ?thesis by simp
   830 qed
   831 
   832 lemma div_add [simp]:
   833   assumes "c dvd a" and "c dvd b"
   834   shows "(a + b) div c = a div c + b div c"
   835 proof (cases "c = 0")
   836   case True
   837   then show ?thesis by simp
   838 next
   839   case False
   840   moreover from assms obtain k l where "a = c * k" and "b = c * l"
   841     by (auto elim!: dvdE)
   842   moreover have "c * k + c * l = c * (k + l)"
   843     by (simp add: algebra_simps)
   844   ultimately show ?thesis
   845     by simp
   846 qed
   847 
   848 lemma div_mult_div_if_dvd:
   849   assumes "b dvd a" and "d dvd c"
   850   shows "(a div b) * (c div d) = (a * c) div (b * d)"
   851 proof (cases "b = 0 \<or> c = 0")
   852   case True
   853   with assms show ?thesis by auto
   854 next
   855   case False
   856   moreover from assms obtain k l where "a = b * k" and "c = d * l"
   857     by (auto elim!: dvdE)
   858   moreover have "b * k * (d * l) div (b * d) = (b * d) * (k * l) div (b * d)"
   859     by (simp add: ac_simps)
   860   ultimately show ?thesis by simp
   861 qed
   862 
   863 lemma dvd_div_eq_mult:
   864   assumes "a \<noteq> 0" and "a dvd b"
   865   shows "b div a = c \<longleftrightarrow> b = c * a"
   866     (is "?lhs \<longleftrightarrow> ?rhs")
   867 proof
   868   assume ?rhs
   869   then show ?lhs by (simp add: assms)
   870 next
   871   assume ?lhs
   872   then have "b div a * a = c * a" by simp
   873   moreover from assms have "b div a * a = b"
   874     by (auto elim!: dvdE simp add: ac_simps)
   875   ultimately show ?rhs by simp
   876 qed
   877 
   878 lemma dvd_div_mult_self [simp]: "a dvd b \<Longrightarrow> b div a * a = b"
   879   by (cases "a = 0") (auto elim: dvdE simp add: ac_simps)
   880 
   881 lemma dvd_mult_div_cancel [simp]: "a dvd b \<Longrightarrow> a * (b div a) = b"
   882   using dvd_div_mult_self [of a b] by (simp add: ac_simps)
   883 
   884 lemma div_mult_swap:
   885   assumes "c dvd b"
   886   shows "a * (b div c) = (a * b) div c"
   887 proof (cases "c = 0")
   888   case True
   889   then show ?thesis by simp
   890 next
   891   case False
   892   from assms obtain d where "b = c * d" ..
   893   moreover from False have "a * divide (d * c) c = ((a * d) * c) div c"
   894     by simp
   895   ultimately show ?thesis by (simp add: ac_simps)
   896 qed
   897 
   898 lemma dvd_div_mult: "c dvd b \<Longrightarrow> b div c * a = (b * a) div c"
   899   using div_mult_swap [of c b a] by (simp add: ac_simps)
   900 
   901 lemma dvd_div_mult2_eq:
   902   assumes "b * c dvd a"
   903   shows "a div (b * c) = a div b div c"
   904 proof -
   905   from assms obtain k where "a = b * c * k" ..
   906   then show ?thesis
   907     by (cases "b = 0 \<or> c = 0") (auto, simp add: ac_simps)
   908 qed
   909 
   910 lemma dvd_div_div_eq_mult:
   911   assumes "a \<noteq> 0" "c \<noteq> 0" and "a dvd b" "c dvd d"
   912   shows "b div a = d div c \<longleftrightarrow> b * c = a * d"
   913     (is "?lhs \<longleftrightarrow> ?rhs")
   914 proof -
   915   from assms have "a * c \<noteq> 0" by simp
   916   then have "?lhs \<longleftrightarrow> b div a * (a * c) = d div c * (a * c)"
   917     by simp
   918   also have "\<dots> \<longleftrightarrow> (a * (b div a)) * c = (c * (d div c)) * a"
   919     by (simp add: ac_simps)
   920   also have "\<dots> \<longleftrightarrow> (a * b div a) * c = (c * d div c) * a"
   921     using assms by (simp add: div_mult_swap)
   922   also have "\<dots> \<longleftrightarrow> ?rhs"
   923     using assms by (simp add: ac_simps)
   924   finally show ?thesis .
   925 qed
   926 
   927 lemma dvd_mult_imp_div:
   928   assumes "a * c dvd b"
   929   shows "a dvd b div c"
   930 proof (cases "c = 0")
   931   case True then show ?thesis by simp
   932 next
   933   case False
   934   from \<open>a * c dvd b\<close> obtain d where "b = a * c * d" ..
   935   with False show ?thesis
   936     by (simp add: mult.commute [of a] mult.assoc)
   937 qed
   938 
   939 lemma div_div_eq_right:
   940   assumes "c dvd b" "b dvd a"
   941   shows   "a div (b div c) = a div b * c"
   942 proof (cases "c = 0 \<or> b = 0")
   943   case True
   944   then show ?thesis
   945     by auto
   946 next
   947   case False
   948   from assms obtain r s where "b = c * r" and "a = c * r * s"
   949     by (blast elim: dvdE)
   950   moreover with False have "r \<noteq> 0"
   951     by auto
   952   ultimately show ?thesis using False
   953     by simp (simp add: mult.commute [of _ r] mult.assoc mult.commute [of c])
   954 qed
   955 
   956 lemma div_div_div_same:
   957   assumes "d dvd b" "b dvd a"
   958   shows   "(a div d) div (b div d) = a div b"
   959 proof (cases "b = 0 \<or> d = 0")
   960   case True
   961   with assms show ?thesis
   962     by auto
   963 next
   964   case False
   965   from assms obtain r s
   966     where "a = d * r * s" and "b = d * r"
   967     by (blast elim: dvdE)
   968   with False show ?thesis
   969     by simp (simp add: ac_simps)
   970 qed
   971 
   972 
   973 text \<open>Units: invertible elements in a ring\<close>
   974 
   975 abbreviation is_unit :: "'a \<Rightarrow> bool"
   976   where "is_unit a \<equiv> a dvd 1"
   977 
   978 lemma not_is_unit_0 [simp]: "\<not> is_unit 0"
   979   by simp
   980 
   981 lemma unit_imp_dvd [dest]: "is_unit b \<Longrightarrow> b dvd a"
   982   by (rule dvd_trans [of _ 1]) simp_all
   983 
   984 lemma unit_dvdE:
   985   assumes "is_unit a"
   986   obtains c where "a \<noteq> 0" and "b = a * c"
   987 proof -
   988   from assms have "a dvd b" by auto
   989   then obtain c where "b = a * c" ..
   990   moreover from assms have "a \<noteq> 0" by auto
   991   ultimately show thesis using that by blast
   992 qed
   993 
   994 lemma dvd_unit_imp_unit: "a dvd b \<Longrightarrow> is_unit b \<Longrightarrow> is_unit a"
   995   by (rule dvd_trans)
   996 
   997 lemma unit_div_1_unit [simp, intro]:
   998   assumes "is_unit a"
   999   shows "is_unit (1 div a)"
  1000 proof -
  1001   from assms have "1 = 1 div a * a" by simp
  1002   then show "is_unit (1 div a)" by (rule dvdI)
  1003 qed
  1004 
  1005 lemma is_unitE [elim?]:
  1006   assumes "is_unit a"
  1007   obtains b where "a \<noteq> 0" and "b \<noteq> 0"
  1008     and "is_unit b" and "1 div a = b" and "1 div b = a"
  1009     and "a * b = 1" and "c div a = c * b"
  1010 proof (rule that)
  1011   define b where "b = 1 div a"
  1012   then show "1 div a = b" by simp
  1013   from assms b_def show "is_unit b" by simp
  1014   with assms show "a \<noteq> 0" and "b \<noteq> 0" by auto
  1015   from assms b_def show "a * b = 1" by simp
  1016   then have "1 = a * b" ..
  1017   with b_def \<open>b \<noteq> 0\<close> show "1 div b = a" by simp
  1018   from assms have "a dvd c" ..
  1019   then obtain d where "c = a * d" ..
  1020   with \<open>a \<noteq> 0\<close> \<open>a * b = 1\<close> show "c div a = c * b"
  1021     by (simp add: mult.assoc mult.left_commute [of a])
  1022 qed
  1023 
  1024 lemma unit_prod [intro]: "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a * b)"
  1025   by (subst mult_1_left [of 1, symmetric]) (rule mult_dvd_mono)
  1026 
  1027 lemma is_unit_mult_iff: "is_unit (a * b) \<longleftrightarrow> is_unit a \<and> is_unit b"
  1028   by (auto dest: dvd_mult_left dvd_mult_right)
  1029 
  1030 lemma unit_div [intro]: "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a div b)"
  1031   by (erule is_unitE [of b a]) (simp add: ac_simps unit_prod)
  1032 
  1033 lemma mult_unit_dvd_iff:
  1034   assumes "is_unit b"
  1035   shows "a * b dvd c \<longleftrightarrow> a dvd c"
  1036 proof
  1037   assume "a * b dvd c"
  1038   with assms show "a dvd c"
  1039     by (simp add: dvd_mult_left)
  1040 next
  1041   assume "a dvd c"
  1042   then obtain k where "c = a * k" ..
  1043   with assms have "c = (a * b) * (1 div b * k)"
  1044     by (simp add: mult_ac)
  1045   then show "a * b dvd c" by (rule dvdI)
  1046 qed
  1047 
  1048 lemma mult_unit_dvd_iff': "is_unit a \<Longrightarrow> (a * b) dvd c \<longleftrightarrow> b dvd c"
  1049   using mult_unit_dvd_iff [of a b c] by (simp add: ac_simps)
  1050 
  1051 lemma dvd_mult_unit_iff:
  1052   assumes "is_unit b"
  1053   shows "a dvd c * b \<longleftrightarrow> a dvd c"
  1054 proof
  1055   assume "a dvd c * b"
  1056   with assms have "c * b dvd c * (b * (1 div b))"
  1057     by (subst mult_assoc [symmetric]) simp
  1058   also from assms have "b * (1 div b) = 1"
  1059     by (rule is_unitE) simp
  1060   finally have "c * b dvd c" by simp
  1061   with \<open>a dvd c * b\<close> show "a dvd c" by (rule dvd_trans)
  1062 next
  1063   assume "a dvd c"
  1064   then show "a dvd c * b" by simp
  1065 qed
  1066 
  1067 lemma dvd_mult_unit_iff': "is_unit b \<Longrightarrow> a dvd b * c \<longleftrightarrow> a dvd c"
  1068   using dvd_mult_unit_iff [of b a c] by (simp add: ac_simps)
  1069 
  1070 lemma div_unit_dvd_iff: "is_unit b \<Longrightarrow> a div b dvd c \<longleftrightarrow> a dvd c"
  1071   by (erule is_unitE [of _ a]) (auto simp add: mult_unit_dvd_iff)
  1072 
  1073 lemma dvd_div_unit_iff: "is_unit b \<Longrightarrow> a dvd c div b \<longleftrightarrow> a dvd c"
  1074   by (erule is_unitE [of _ c]) (simp add: dvd_mult_unit_iff)
  1075 
  1076 lemmas unit_dvd_iff = mult_unit_dvd_iff mult_unit_dvd_iff'
  1077   dvd_mult_unit_iff dvd_mult_unit_iff' 
  1078   div_unit_dvd_iff dvd_div_unit_iff (* FIXME consider named_theorems *)
  1079 
  1080 lemma unit_mult_div_div [simp]: "is_unit a \<Longrightarrow> b * (1 div a) = b div a"
  1081   by (erule is_unitE [of _ b]) simp
  1082 
  1083 lemma unit_div_mult_self [simp]: "is_unit a \<Longrightarrow> b div a * a = b"
  1084   by (rule dvd_div_mult_self) auto
  1085 
  1086 lemma unit_div_1_div_1 [simp]: "is_unit a \<Longrightarrow> 1 div (1 div a) = a"
  1087   by (erule is_unitE) simp
  1088 
  1089 lemma unit_div_mult_swap: "is_unit c \<Longrightarrow> a * (b div c) = (a * b) div c"
  1090   by (erule unit_dvdE [of _ b]) (simp add: mult.left_commute [of _ c])
  1091 
  1092 lemma unit_div_commute: "is_unit b \<Longrightarrow> (a div b) * c = (a * c) div b"
  1093   using unit_div_mult_swap [of b c a] by (simp add: ac_simps)
  1094 
  1095 lemma unit_eq_div1: "is_unit b \<Longrightarrow> a div b = c \<longleftrightarrow> a = c * b"
  1096   by (auto elim: is_unitE)
  1097 
  1098 lemma unit_eq_div2: "is_unit b \<Longrightarrow> a = c div b \<longleftrightarrow> a * b = c"
  1099   using unit_eq_div1 [of b c a] by auto
  1100 
  1101 lemma unit_mult_left_cancel: "is_unit a \<Longrightarrow> a * b = a * c \<longleftrightarrow> b = c"
  1102   using mult_cancel_left [of a b c] by auto
  1103 
  1104 lemma unit_mult_right_cancel: "is_unit a \<Longrightarrow> b * a = c * a \<longleftrightarrow> b = c"
  1105   using unit_mult_left_cancel [of a b c] by (auto simp add: ac_simps)
  1106 
  1107 lemma unit_div_cancel:
  1108   assumes "is_unit a"
  1109   shows "b div a = c div a \<longleftrightarrow> b = c"
  1110 proof -
  1111   from assms have "is_unit (1 div a)" by simp
  1112   then have "b * (1 div a) = c * (1 div a) \<longleftrightarrow> b = c"
  1113     by (rule unit_mult_right_cancel)
  1114   with assms show ?thesis by simp
  1115 qed
  1116 
  1117 lemma is_unit_div_mult2_eq:
  1118   assumes "is_unit b" and "is_unit c"
  1119   shows "a div (b * c) = a div b div c"
  1120 proof -
  1121   from assms have "is_unit (b * c)"
  1122     by (simp add: unit_prod)
  1123   then have "b * c dvd a"
  1124     by (rule unit_imp_dvd)
  1125   then show ?thesis
  1126     by (rule dvd_div_mult2_eq)
  1127 qed
  1128 
  1129 lemmas unit_simps = mult_unit_dvd_iff div_unit_dvd_iff dvd_mult_unit_iff
  1130   dvd_div_unit_iff unit_div_mult_swap unit_div_commute
  1131   unit_mult_left_cancel unit_mult_right_cancel unit_div_cancel
  1132   unit_eq_div1 unit_eq_div2
  1133 
  1134 lemma is_unit_div_mult_cancel_left:
  1135   assumes "a \<noteq> 0" and "is_unit b"
  1136   shows "a div (a * b) = 1 div b"
  1137 proof -
  1138   from assms have "a div (a * b) = a div a div b"
  1139     by (simp add: mult_unit_dvd_iff dvd_div_mult2_eq)
  1140   with assms show ?thesis by simp
  1141 qed
  1142 
  1143 lemma is_unit_div_mult_cancel_right:
  1144   assumes "a \<noteq> 0" and "is_unit b"
  1145   shows "a div (b * a) = 1 div b"
  1146   using assms is_unit_div_mult_cancel_left [of a b] by (simp add: ac_simps)
  1147 
  1148 lemma unit_div_eq_0_iff:
  1149   assumes "is_unit b"
  1150   shows "a div b = 0 \<longleftrightarrow> a = 0"
  1151   by (rule dvd_div_eq_0_iff) (insert assms, auto)  
  1152 
  1153 lemma div_mult_unit2:
  1154   "is_unit c \<Longrightarrow> b dvd a \<Longrightarrow> a div (b * c) = a div b div c"
  1155   by (rule dvd_div_mult2_eq) (simp_all add: mult_unit_dvd_iff)
  1156 
  1157 end
  1158 
  1159 class unit_factor =
  1160   fixes unit_factor :: "'a \<Rightarrow> 'a"
  1161 
  1162 class semidom_divide_unit_factor = semidom_divide + unit_factor +
  1163   assumes unit_factor_0 [simp]: "unit_factor 0 = 0"
  1164     and is_unit_unit_factor: "a dvd 1 \<Longrightarrow> unit_factor a = a"
  1165     and unit_factor_is_unit: "a \<noteq> 0 \<Longrightarrow> unit_factor a dvd 1"
  1166     and unit_factor_mult: "unit_factor (a * b) = unit_factor a * unit_factor b"
  1167   -- \<open>This fine-grained hierarchy will later on allow lean normalization of polynomials\<close>
  1168   
  1169 class normalization_semidom = algebraic_semidom + semidom_divide_unit_factor +
  1170   fixes normalize :: "'a \<Rightarrow> 'a"
  1171   assumes unit_factor_mult_normalize [simp]: "unit_factor a * normalize a = a"
  1172     and normalize_0 [simp]: "normalize 0 = 0"
  1173 begin
  1174 
  1175 text \<open>
  1176   Class @{class normalization_semidom} cultivates the idea that each integral
  1177   domain can be split into equivalence classes whose representants are
  1178   associated, i.e. divide each other. @{const normalize} specifies a canonical
  1179   representant for each equivalence class. The rationale behind this is that
  1180   it is easier to reason about equality than equivalences, hence we prefer to
  1181   think about equality of normalized values rather than associated elements.
  1182 \<close>
  1183 
  1184 declare unit_factor_is_unit [iff]
  1185   
  1186 lemma unit_factor_dvd [simp]: "a \<noteq> 0 \<Longrightarrow> unit_factor a dvd b"
  1187   by (rule unit_imp_dvd) simp
  1188 
  1189 lemma unit_factor_self [simp]: "unit_factor a dvd a"
  1190   by (cases "a = 0") simp_all
  1191 
  1192 lemma normalize_mult_unit_factor [simp]: "normalize a * unit_factor a = a"
  1193   using unit_factor_mult_normalize [of a] by (simp add: ac_simps)
  1194 
  1195 lemma normalize_eq_0_iff [simp]: "normalize a = 0 \<longleftrightarrow> a = 0"
  1196   (is "?lhs \<longleftrightarrow> ?rhs")
  1197 proof
  1198   assume ?lhs
  1199   moreover have "unit_factor a * normalize a = a" by simp
  1200   ultimately show ?rhs by simp
  1201 next
  1202   assume ?rhs
  1203   then show ?lhs by simp
  1204 qed
  1205 
  1206 lemma unit_factor_eq_0_iff [simp]: "unit_factor a = 0 \<longleftrightarrow> a = 0"
  1207   (is "?lhs \<longleftrightarrow> ?rhs")
  1208 proof
  1209   assume ?lhs
  1210   moreover have "unit_factor a * normalize a = a" by simp
  1211   ultimately show ?rhs by simp
  1212 next
  1213   assume ?rhs
  1214   then show ?lhs by simp
  1215 qed
  1216 
  1217 lemma div_unit_factor [simp]: "a div unit_factor a = normalize a"
  1218 proof (cases "a = 0")
  1219   case True
  1220   then show ?thesis by simp
  1221 next
  1222   case False
  1223   then have "unit_factor a \<noteq> 0"
  1224     by simp
  1225   with nonzero_mult_div_cancel_left
  1226   have "unit_factor a * normalize a div unit_factor a = normalize a"
  1227     by blast
  1228   then show ?thesis by simp
  1229 qed
  1230 
  1231 lemma normalize_div [simp]: "normalize a div a = 1 div unit_factor a"
  1232 proof (cases "a = 0")
  1233   case True
  1234   then show ?thesis by simp
  1235 next
  1236   case False
  1237   have "normalize a div a = normalize a div (unit_factor a * normalize a)"
  1238     by simp
  1239   also have "\<dots> = 1 div unit_factor a"
  1240     using False by (subst is_unit_div_mult_cancel_right) simp_all
  1241   finally show ?thesis .
  1242 qed
  1243 
  1244 lemma is_unit_normalize:
  1245   assumes "is_unit a"
  1246   shows "normalize a = 1"
  1247 proof -
  1248   from assms have "unit_factor a = a"
  1249     by (rule is_unit_unit_factor)
  1250   moreover from assms have "a \<noteq> 0"
  1251     by auto
  1252   moreover have "normalize a = a div unit_factor a"
  1253     by simp
  1254   ultimately show ?thesis
  1255     by simp
  1256 qed
  1257 
  1258 lemma unit_factor_1 [simp]: "unit_factor 1 = 1"
  1259   by (rule is_unit_unit_factor) simp
  1260 
  1261 lemma normalize_1 [simp]: "normalize 1 = 1"
  1262   by (rule is_unit_normalize) simp
  1263 
  1264 lemma normalize_1_iff: "normalize a = 1 \<longleftrightarrow> is_unit a"
  1265   (is "?lhs \<longleftrightarrow> ?rhs")
  1266 proof
  1267   assume ?rhs
  1268   then show ?lhs by (rule is_unit_normalize)
  1269 next
  1270   assume ?lhs
  1271   then have "unit_factor a * normalize a = unit_factor a * 1"
  1272     by simp
  1273   then have "unit_factor a = a"
  1274     by simp
  1275   moreover
  1276   from \<open>?lhs\<close> have "a \<noteq> 0" by auto
  1277   then have "is_unit (unit_factor a)" by simp
  1278   ultimately show ?rhs by simp
  1279 qed
  1280 
  1281 lemma div_normalize [simp]: "a div normalize a = unit_factor a"
  1282 proof (cases "a = 0")
  1283   case True
  1284   then show ?thesis by simp
  1285 next
  1286   case False
  1287   then have "normalize a \<noteq> 0" by simp
  1288   with nonzero_mult_div_cancel_right
  1289   have "unit_factor a * normalize a div normalize a = unit_factor a" by blast
  1290   then show ?thesis by simp
  1291 qed
  1292 
  1293 lemma mult_one_div_unit_factor [simp]: "a * (1 div unit_factor b) = a div unit_factor b"
  1294   by (cases "b = 0") simp_all
  1295 
  1296 lemma inv_unit_factor_eq_0_iff [simp]:
  1297   "1 div unit_factor a = 0 \<longleftrightarrow> a = 0"
  1298   (is "?lhs \<longleftrightarrow> ?rhs")
  1299 proof
  1300   assume ?lhs
  1301   then have "a * (1 div unit_factor a) = a * 0"
  1302     by simp
  1303   then show ?rhs
  1304     by simp
  1305 next
  1306   assume ?rhs
  1307   then show ?lhs by simp
  1308 qed
  1309 
  1310 lemma normalize_mult: "normalize (a * b) = normalize a * normalize b"
  1311 proof (cases "a = 0 \<or> b = 0")
  1312   case True
  1313   then show ?thesis by auto
  1314 next
  1315   case False
  1316   have "unit_factor (a * b) * normalize (a * b) = a * b"
  1317     by (rule unit_factor_mult_normalize)
  1318   then have "normalize (a * b) = a * b div unit_factor (a * b)"
  1319     by simp
  1320   also have "\<dots> = a * b div unit_factor (b * a)"
  1321     by (simp add: ac_simps)
  1322   also have "\<dots> = a * b div unit_factor b div unit_factor a"
  1323     using False by (simp add: unit_factor_mult is_unit_div_mult2_eq [symmetric])
  1324   also have "\<dots> = a * (b div unit_factor b) div unit_factor a"
  1325     using False by (subst unit_div_mult_swap) simp_all
  1326   also have "\<dots> = normalize a * normalize b"
  1327     using False
  1328     by (simp add: mult.commute [of a] mult.commute [of "normalize a"] unit_div_mult_swap [symmetric])
  1329   finally show ?thesis .
  1330 qed
  1331 
  1332 lemma unit_factor_idem [simp]: "unit_factor (unit_factor a) = unit_factor a"
  1333   by (cases "a = 0") (auto intro: is_unit_unit_factor)
  1334 
  1335 lemma normalize_unit_factor [simp]: "a \<noteq> 0 \<Longrightarrow> normalize (unit_factor a) = 1"
  1336   by (rule is_unit_normalize) simp
  1337 
  1338 lemma normalize_idem [simp]: "normalize (normalize a) = normalize a"
  1339 proof (cases "a = 0")
  1340   case True
  1341   then show ?thesis by simp
  1342 next
  1343   case False
  1344   have "normalize a = normalize (unit_factor a * normalize a)"
  1345     by simp
  1346   also have "\<dots> = normalize (unit_factor a) * normalize (normalize a)"
  1347     by (simp only: normalize_mult)
  1348   finally show ?thesis
  1349     using False by simp_all
  1350 qed
  1351 
  1352 lemma unit_factor_normalize [simp]:
  1353   assumes "a \<noteq> 0"
  1354   shows "unit_factor (normalize a) = 1"
  1355 proof -
  1356   from assms have *: "normalize a \<noteq> 0"
  1357     by simp
  1358   have "unit_factor (normalize a) * normalize (normalize a) = normalize a"
  1359     by (simp only: unit_factor_mult_normalize)
  1360   then have "unit_factor (normalize a) * normalize a = normalize a"
  1361     by simp
  1362   with * have "unit_factor (normalize a) * normalize a div normalize a = normalize a div normalize a"
  1363     by simp
  1364   with * show ?thesis
  1365     by simp
  1366 qed
  1367 
  1368 lemma dvd_unit_factor_div:
  1369   assumes "b dvd a"
  1370   shows "unit_factor (a div b) = unit_factor a div unit_factor b"
  1371 proof -
  1372   from assms have "a = a div b * b"
  1373     by simp
  1374   then have "unit_factor a = unit_factor (a div b * b)"
  1375     by simp
  1376   then show ?thesis
  1377     by (cases "b = 0") (simp_all add: unit_factor_mult)
  1378 qed
  1379 
  1380 lemma dvd_normalize_div:
  1381   assumes "b dvd a"
  1382   shows "normalize (a div b) = normalize a div normalize b"
  1383 proof -
  1384   from assms have "a = a div b * b"
  1385     by simp
  1386   then have "normalize a = normalize (a div b * b)"
  1387     by simp
  1388   then show ?thesis
  1389     by (cases "b = 0") (simp_all add: normalize_mult)
  1390 qed
  1391 
  1392 lemma normalize_dvd_iff [simp]: "normalize a dvd b \<longleftrightarrow> a dvd b"
  1393 proof -
  1394   have "normalize a dvd b \<longleftrightarrow> unit_factor a * normalize a dvd b"
  1395     using mult_unit_dvd_iff [of "unit_factor a" "normalize a" b]
  1396       by (cases "a = 0") simp_all
  1397   then show ?thesis by simp
  1398 qed
  1399 
  1400 lemma dvd_normalize_iff [simp]: "a dvd normalize b \<longleftrightarrow> a dvd b"
  1401 proof -
  1402   have "a dvd normalize  b \<longleftrightarrow> a dvd normalize b * unit_factor b"
  1403     using dvd_mult_unit_iff [of "unit_factor b" a "normalize b"]
  1404       by (cases "b = 0") simp_all
  1405   then show ?thesis by simp
  1406 qed
  1407 
  1408 lemma normalize_idem_imp_unit_factor_eq:
  1409   assumes "normalize a = a"
  1410   shows "unit_factor a = of_bool (a \<noteq> 0)"
  1411 proof (cases "a = 0")
  1412   case True
  1413   then show ?thesis
  1414     by simp
  1415 next
  1416   case False
  1417   then show ?thesis
  1418     using assms unit_factor_normalize [of a] by simp
  1419 qed
  1420 
  1421 lemma normalize_idem_imp_is_unit_iff:
  1422   assumes "normalize a = a"
  1423   shows "is_unit a \<longleftrightarrow> a = 1"
  1424   using assms by (cases "a = 0") (auto dest: is_unit_normalize)
  1425 
  1426 text \<open>
  1427   We avoid an explicit definition of associated elements but prefer explicit
  1428   normalisation instead. In theory we could define an abbreviation like @{prop
  1429   "associated a b \<longleftrightarrow> normalize a = normalize b"} but this is counterproductive
  1430   without suggestive infix syntax, which we do not want to sacrifice for this
  1431   purpose here.
  1432 \<close>
  1433 
  1434 lemma associatedI:
  1435   assumes "a dvd b" and "b dvd a"
  1436   shows "normalize a = normalize b"
  1437 proof (cases "a = 0 \<or> b = 0")
  1438   case True
  1439   with assms show ?thesis by auto
  1440 next
  1441   case False
  1442   from \<open>a dvd b\<close> obtain c where b: "b = a * c" ..
  1443   moreover from \<open>b dvd a\<close> obtain d where a: "a = b * d" ..
  1444   ultimately have "b * 1 = b * (c * d)"
  1445     by (simp add: ac_simps)
  1446   with False have "1 = c * d"
  1447     unfolding mult_cancel_left by simp
  1448   then have "is_unit c" and "is_unit d"
  1449     by auto
  1450   with a b show ?thesis
  1451     by (simp add: normalize_mult is_unit_normalize)
  1452 qed
  1453 
  1454 lemma associatedD1: "normalize a = normalize b \<Longrightarrow> a dvd b"
  1455   using dvd_normalize_iff [of _ b, symmetric] normalize_dvd_iff [of a _, symmetric]
  1456   by simp
  1457 
  1458 lemma associatedD2: "normalize a = normalize b \<Longrightarrow> b dvd a"
  1459   using dvd_normalize_iff [of _ a, symmetric] normalize_dvd_iff [of b _, symmetric]
  1460   by simp
  1461 
  1462 lemma associated_unit: "normalize a = normalize b \<Longrightarrow> is_unit a \<Longrightarrow> is_unit b"
  1463   using dvd_unit_imp_unit by (auto dest!: associatedD1 associatedD2)
  1464 
  1465 lemma associated_iff_dvd: "normalize a = normalize b \<longleftrightarrow> a dvd b \<and> b dvd a"
  1466   (is "?lhs \<longleftrightarrow> ?rhs")
  1467 proof
  1468   assume ?rhs
  1469   then show ?lhs by (auto intro!: associatedI)
  1470 next
  1471   assume ?lhs
  1472   then have "unit_factor a * normalize a = unit_factor a * normalize b"
  1473     by simp
  1474   then have *: "normalize b * unit_factor a = a"
  1475     by (simp add: ac_simps)
  1476   show ?rhs
  1477   proof (cases "a = 0 \<or> b = 0")
  1478     case True
  1479     with \<open>?lhs\<close> show ?thesis by auto
  1480   next
  1481     case False
  1482     then have "b dvd normalize b * unit_factor a" and "normalize b * unit_factor a dvd b"
  1483       by (simp_all add: mult_unit_dvd_iff dvd_mult_unit_iff)
  1484     with * show ?thesis by simp
  1485   qed
  1486 qed
  1487 
  1488 lemma associated_eqI:
  1489   assumes "a dvd b" and "b dvd a"
  1490   assumes "normalize a = a" and "normalize b = b"
  1491   shows "a = b"
  1492 proof -
  1493   from assms have "normalize a = normalize b"
  1494     unfolding associated_iff_dvd by simp
  1495   with \<open>normalize a = a\<close> have "a = normalize b"
  1496     by simp
  1497   with \<open>normalize b = b\<close> show "a = b"
  1498     by simp
  1499 qed
  1500 
  1501 lemma normalize_unit_factor_eqI:
  1502   assumes "normalize a = normalize b"
  1503     and "unit_factor a = unit_factor b"
  1504   shows "a = b"
  1505 proof -
  1506   from assms have "unit_factor a * normalize a = unit_factor b * normalize b"
  1507     by simp
  1508   then show ?thesis
  1509     by simp
  1510 qed
  1511 
  1512 end
  1513 
  1514 
  1515 text \<open>Syntactic division remainder operator\<close>
  1516 
  1517 class modulo = dvd + divide +
  1518   fixes modulo :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "mod" 70)
  1519 
  1520 text \<open>Arbitrary quotient and remainder partitions\<close>
  1521 
  1522 class semiring_modulo = comm_semiring_1_cancel + divide + modulo +
  1523   assumes div_mult_mod_eq: "a div b * b + a mod b = a"
  1524 begin
  1525 
  1526 lemma mod_div_decomp:
  1527   fixes a b
  1528   obtains q r where "q = a div b" and "r = a mod b"
  1529     and "a = q * b + r"
  1530 proof -
  1531   from div_mult_mod_eq have "a = a div b * b + a mod b" by simp
  1532   moreover have "a div b = a div b" ..
  1533   moreover have "a mod b = a mod b" ..
  1534   note that ultimately show thesis by blast
  1535 qed
  1536 
  1537 lemma mult_div_mod_eq: "b * (a div b) + a mod b = a"
  1538   using div_mult_mod_eq [of a b] by (simp add: ac_simps)
  1539 
  1540 lemma mod_div_mult_eq: "a mod b + a div b * b = a"
  1541   using div_mult_mod_eq [of a b] by (simp add: ac_simps)
  1542 
  1543 lemma mod_mult_div_eq: "a mod b + b * (a div b) = a"
  1544   using div_mult_mod_eq [of a b] by (simp add: ac_simps)
  1545 
  1546 lemma minus_div_mult_eq_mod: "a - a div b * b = a mod b"
  1547   by (rule add_implies_diff [symmetric]) (fact mod_div_mult_eq)
  1548 
  1549 lemma minus_mult_div_eq_mod: "a - b * (a div b) = a mod b"
  1550   by (rule add_implies_diff [symmetric]) (fact mod_mult_div_eq)
  1551 
  1552 lemma minus_mod_eq_div_mult: "a - a mod b = a div b * b"
  1553   by (rule add_implies_diff [symmetric]) (fact div_mult_mod_eq)
  1554 
  1555 lemma minus_mod_eq_mult_div: "a - a mod b = b * (a div b)"
  1556   by (rule add_implies_diff [symmetric]) (fact mult_div_mod_eq)
  1557 
  1558 end
  1559 
  1560 
  1561 class ordered_semiring = semiring + ordered_comm_monoid_add +
  1562   assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
  1563   assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"
  1564 begin
  1565 
  1566 lemma mult_mono: "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * d"
  1567   apply (erule (1) mult_right_mono [THEN order_trans])
  1568   apply (erule (1) mult_left_mono)
  1569   done
  1570 
  1571 lemma mult_mono': "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * d"
  1572   by (rule mult_mono) (fast intro: order_trans)+
  1573 
  1574 end
  1575 
  1576 class ordered_semiring_0 = semiring_0 + ordered_semiring
  1577 begin
  1578 
  1579 lemma mult_nonneg_nonneg [simp]: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b"
  1580   using mult_left_mono [of 0 b a] by simp
  1581 
  1582 lemma mult_nonneg_nonpos: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> a * b \<le> 0"
  1583   using mult_left_mono [of b 0 a] by simp
  1584 
  1585 lemma mult_nonpos_nonneg: "a \<le> 0 \<Longrightarrow> 0 \<le> b \<Longrightarrow> a * b \<le> 0"
  1586   using mult_right_mono [of a 0 b] by simp
  1587 
  1588 text \<open>Legacy -- use @{thm [source] mult_nonpos_nonneg}.\<close>
  1589 lemma mult_nonneg_nonpos2: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> b * a \<le> 0"
  1590   by (drule mult_right_mono [of b 0]) auto
  1591 
  1592 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"
  1593   by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)
  1594 
  1595 end
  1596 
  1597 class ordered_cancel_semiring = ordered_semiring + cancel_comm_monoid_add
  1598 begin
  1599 
  1600 subclass semiring_0_cancel ..
  1601 
  1602 subclass ordered_semiring_0 ..
  1603 
  1604 end
  1605 
  1606 class linordered_semiring = ordered_semiring + linordered_cancel_ab_semigroup_add
  1607 begin
  1608 
  1609 subclass ordered_cancel_semiring ..
  1610 
  1611 subclass ordered_cancel_comm_monoid_add ..
  1612 
  1613 subclass ordered_ab_semigroup_monoid_add_imp_le ..
  1614 
  1615 lemma mult_left_less_imp_less: "c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
  1616   by (force simp add: mult_left_mono not_le [symmetric])
  1617 
  1618 lemma mult_right_less_imp_less: "a * c < b * c \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
  1619   by (force simp add: mult_right_mono not_le [symmetric])
  1620 
  1621 end
  1622 
  1623 class linordered_semiring_1 = linordered_semiring + semiring_1
  1624 begin
  1625 
  1626 lemma convex_bound_le:
  1627   assumes "x \<le> a" "y \<le> a" "0 \<le> u" "0 \<le> v" "u + v = 1"
  1628   shows "u * x + v * y \<le> a"
  1629 proof-
  1630   from assms have "u * x + v * y \<le> u * a + v * a"
  1631     by (simp add: add_mono mult_left_mono)
  1632   with assms show ?thesis
  1633     unfolding distrib_right[symmetric] by simp
  1634 qed
  1635 
  1636 end
  1637 
  1638 class linordered_semiring_strict = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add +
  1639   assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
  1640   assumes mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c"
  1641 begin
  1642 
  1643 subclass semiring_0_cancel ..
  1644 
  1645 subclass linordered_semiring
  1646 proof
  1647   fix a b c :: 'a
  1648   assume *: "a \<le> b" "0 \<le> c"
  1649   then show "c * a \<le> c * b"
  1650     unfolding le_less
  1651     using mult_strict_left_mono by (cases "c = 0") auto
  1652   from * show "a * c \<le> b * c"
  1653     unfolding le_less
  1654     using mult_strict_right_mono by (cases "c = 0") auto
  1655 qed
  1656 
  1657 lemma mult_left_le_imp_le: "c * a \<le> c * b \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
  1658   by (auto simp add: mult_strict_left_mono _not_less [symmetric])
  1659 
  1660 lemma mult_right_le_imp_le: "a * c \<le> b * c \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
  1661   by (auto simp add: mult_strict_right_mono not_less [symmetric])
  1662 
  1663 lemma mult_pos_pos[simp]: "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a * b"
  1664   using mult_strict_left_mono [of 0 b a] by simp
  1665 
  1666 lemma mult_pos_neg: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> a * b < 0"
  1667   using mult_strict_left_mono [of b 0 a] by simp
  1668 
  1669 lemma mult_neg_pos: "a < 0 \<Longrightarrow> 0 < b \<Longrightarrow> a * b < 0"
  1670   using mult_strict_right_mono [of a 0 b] by simp
  1671 
  1672 text \<open>Legacy -- use @{thm [source] mult_neg_pos}.\<close>
  1673 lemma mult_pos_neg2: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> b * a < 0"
  1674   by (drule mult_strict_right_mono [of b 0]) auto
  1675 
  1676 lemma zero_less_mult_pos: "0 < a * b \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"
  1677   apply (cases "b \<le> 0")
  1678    apply (auto simp add: le_less not_less)
  1679   apply (drule_tac mult_pos_neg [of a b])
  1680    apply (auto dest: less_not_sym)
  1681   done
  1682 
  1683 lemma zero_less_mult_pos2: "0 < b * a \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"
  1684   apply (cases "b \<le> 0")
  1685    apply (auto simp add: le_less not_less)
  1686   apply (drule_tac mult_pos_neg2 [of a b])
  1687    apply (auto dest: less_not_sym)
  1688   done
  1689 
  1690 text \<open>Strict monotonicity in both arguments\<close>
  1691 lemma mult_strict_mono:
  1692   assumes "a < b" and "c < d" and "0 < b" and "0 \<le> c"
  1693   shows "a * c < b * d"
  1694   using assms
  1695   apply (cases "c = 0")
  1696    apply simp
  1697   apply (erule mult_strict_right_mono [THEN less_trans])
  1698    apply (auto simp add: le_less)
  1699   apply (erule (1) mult_strict_left_mono)
  1700   done
  1701 
  1702 text \<open>This weaker variant has more natural premises\<close>
  1703 lemma mult_strict_mono':
  1704   assumes "a < b" and "c < d" and "0 \<le> a" and "0 \<le> c"
  1705   shows "a * c < b * d"
  1706   by (rule mult_strict_mono) (insert assms, auto)
  1707 
  1708 lemma mult_less_le_imp_less:
  1709   assumes "a < b" and "c \<le> d" and "0 \<le> a" and "0 < c"
  1710   shows "a * c < b * d"
  1711   using assms
  1712   apply (subgoal_tac "a * c < b * c")
  1713    apply (erule less_le_trans)
  1714    apply (erule mult_left_mono)
  1715    apply simp
  1716   apply (erule (1) mult_strict_right_mono)
  1717   done
  1718 
  1719 lemma mult_le_less_imp_less:
  1720   assumes "a \<le> b" and "c < d" and "0 < a" and "0 \<le> c"
  1721   shows "a * c < b * d"
  1722   using assms
  1723   apply (subgoal_tac "a * c \<le> b * c")
  1724    apply (erule le_less_trans)
  1725    apply (erule mult_strict_left_mono)
  1726    apply simp
  1727   apply (erule (1) mult_right_mono)
  1728   done
  1729 
  1730 end
  1731 
  1732 class linordered_semiring_1_strict = linordered_semiring_strict + semiring_1
  1733 begin
  1734 
  1735 subclass linordered_semiring_1 ..
  1736 
  1737 lemma convex_bound_lt:
  1738   assumes "x < a" "y < a" "0 \<le> u" "0 \<le> v" "u + v = 1"
  1739   shows "u * x + v * y < a"
  1740 proof -
  1741   from assms have "u * x + v * y < u * a + v * a"
  1742     by (cases "u = 0") (auto intro!: add_less_le_mono mult_strict_left_mono mult_left_mono)
  1743   with assms show ?thesis
  1744     unfolding distrib_right[symmetric] by simp
  1745 qed
  1746 
  1747 end
  1748 
  1749 class ordered_comm_semiring = comm_semiring_0 + ordered_ab_semigroup_add +
  1750   assumes comm_mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
  1751 begin
  1752 
  1753 subclass ordered_semiring
  1754 proof
  1755   fix a b c :: 'a
  1756   assume "a \<le> b" "0 \<le> c"
  1757   then show "c * a \<le> c * b" by (rule comm_mult_left_mono)
  1758   then show "a * c \<le> b * c" by (simp only: mult.commute)
  1759 qed
  1760 
  1761 end
  1762 
  1763 class ordered_cancel_comm_semiring = ordered_comm_semiring + cancel_comm_monoid_add
  1764 begin
  1765 
  1766 subclass comm_semiring_0_cancel ..
  1767 subclass ordered_comm_semiring ..
  1768 subclass ordered_cancel_semiring ..
  1769 
  1770 end
  1771 
  1772 class linordered_comm_semiring_strict = comm_semiring_0 + linordered_cancel_ab_semigroup_add +
  1773   assumes comm_mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
  1774 begin
  1775 
  1776 subclass linordered_semiring_strict
  1777 proof
  1778   fix a b c :: 'a
  1779   assume "a < b" "0 < c"
  1780   then show "c * a < c * b"
  1781     by (rule comm_mult_strict_left_mono)
  1782   then show "a * c < b * c"
  1783     by (simp only: mult.commute)
  1784 qed
  1785 
  1786 subclass ordered_cancel_comm_semiring
  1787 proof
  1788   fix a b c :: 'a
  1789   assume "a \<le> b" "0 \<le> c"
  1790   then show "c * a \<le> c * b"
  1791     unfolding le_less
  1792     using mult_strict_left_mono by (cases "c = 0") auto
  1793 qed
  1794 
  1795 end
  1796 
  1797 class ordered_ring = ring + ordered_cancel_semiring
  1798 begin
  1799 
  1800 subclass ordered_ab_group_add ..
  1801 
  1802 lemma less_add_iff1: "a * e + c < b * e + d \<longleftrightarrow> (a - b) * e + c < d"
  1803   by (simp add: algebra_simps)
  1804 
  1805 lemma less_add_iff2: "a * e + c < b * e + d \<longleftrightarrow> c < (b - a) * e + d"
  1806   by (simp add: algebra_simps)
  1807 
  1808 lemma le_add_iff1: "a * e + c \<le> b * e + d \<longleftrightarrow> (a - b) * e + c \<le> d"
  1809   by (simp add: algebra_simps)
  1810 
  1811 lemma le_add_iff2: "a * e + c \<le> b * e + d \<longleftrightarrow> c \<le> (b - a) * e + d"
  1812   by (simp add: algebra_simps)
  1813 
  1814 lemma mult_left_mono_neg: "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> c * a \<le> c * b"
  1815   apply (drule mult_left_mono [of _ _ "- c"])
  1816   apply simp_all
  1817   done
  1818 
  1819 lemma mult_right_mono_neg: "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> a * c \<le> b * c"
  1820   apply (drule mult_right_mono [of _ _ "- c"])
  1821   apply simp_all
  1822   done
  1823 
  1824 lemma mult_nonpos_nonpos: "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> 0 \<le> a * b"
  1825   using mult_right_mono_neg [of a 0 b] by simp
  1826 
  1827 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"
  1828   by (auto simp add: mult_nonpos_nonpos)
  1829 
  1830 end
  1831 
  1832 class abs_if = minus + uminus + ord + zero + abs +
  1833   assumes abs_if: "\<bar>a\<bar> = (if a < 0 then - a else a)"
  1834 
  1835 class linordered_ring = ring + linordered_semiring + linordered_ab_group_add + abs_if
  1836 begin
  1837 
  1838 subclass ordered_ring ..
  1839 
  1840 subclass ordered_ab_group_add_abs
  1841 proof
  1842   fix a b
  1843   show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
  1844     by (auto simp add: abs_if not_le not_less algebra_simps
  1845         simp del: add.commute dest: add_neg_neg add_nonneg_nonneg)
  1846 qed (auto simp: abs_if)
  1847 
  1848 lemma zero_le_square [simp]: "0 \<le> a * a"
  1849   using linear [of 0 a] by (auto simp add: mult_nonpos_nonpos)
  1850 
  1851 lemma not_square_less_zero [simp]: "\<not> (a * a < 0)"
  1852   by (simp add: not_less)
  1853 
  1854 proposition abs_eq_iff: "\<bar>x\<bar> = \<bar>y\<bar> \<longleftrightarrow> x = y \<or> x = -y"
  1855   by (auto simp add: abs_if split: if_split_asm)
  1856 
  1857 lemma abs_eq_iff':
  1858   "\<bar>a\<bar> = b \<longleftrightarrow> b \<ge> 0 \<and> (a = b \<or> a = - b)"
  1859   by (cases "a \<ge> 0") auto
  1860 
  1861 lemma eq_abs_iff':
  1862   "a = \<bar>b\<bar> \<longleftrightarrow> a \<ge> 0 \<and> (b = a \<or> b = - a)"
  1863   using abs_eq_iff' [of b a] by auto
  1864 
  1865 lemma sum_squares_ge_zero: "0 \<le> x * x + y * y"
  1866   by (intro add_nonneg_nonneg zero_le_square)
  1867 
  1868 lemma not_sum_squares_lt_zero: "\<not> x * x + y * y < 0"
  1869   by (simp add: not_less sum_squares_ge_zero)
  1870 
  1871 end
  1872 
  1873 class linordered_ring_strict = ring + linordered_semiring_strict
  1874   + ordered_ab_group_add + abs_if
  1875 begin
  1876 
  1877 subclass linordered_ring ..
  1878 
  1879 lemma mult_strict_left_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> c * a < c * b"
  1880   using mult_strict_left_mono [of b a "- c"] by simp
  1881 
  1882 lemma mult_strict_right_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> a * c < b * c"
  1883   using mult_strict_right_mono [of b a "- c"] by simp
  1884 
  1885 lemma mult_neg_neg: "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> 0 < a * b"
  1886   using mult_strict_right_mono_neg [of a 0 b] by simp
  1887 
  1888 subclass ring_no_zero_divisors
  1889 proof
  1890   fix a b
  1891   assume "a \<noteq> 0"
  1892   then have a: "a < 0 \<or> 0 < a" by (simp add: neq_iff)
  1893   assume "b \<noteq> 0"
  1894   then have b: "b < 0 \<or> 0 < b" by (simp add: neq_iff)
  1895   have "a * b < 0 \<or> 0 < a * b"
  1896   proof (cases "a < 0")
  1897     case True
  1898     show ?thesis
  1899     proof (cases "b < 0")
  1900       case True
  1901       with \<open>a < 0\<close> show ?thesis by (auto dest: mult_neg_neg)
  1902     next
  1903       case False
  1904       with b have "0 < b" by auto
  1905       with \<open>a < 0\<close> show ?thesis by (auto dest: mult_strict_right_mono)
  1906     qed
  1907   next
  1908     case False
  1909     with a have "0 < a" by auto
  1910     show ?thesis
  1911     proof (cases "b < 0")
  1912       case True
  1913       with \<open>0 < a\<close> show ?thesis
  1914         by (auto dest: mult_strict_right_mono_neg)
  1915     next
  1916       case False
  1917       with b have "0 < b" by auto
  1918       with \<open>0 < a\<close> show ?thesis by auto
  1919     qed
  1920   qed
  1921   then show "a * b \<noteq> 0"
  1922     by (simp add: neq_iff)
  1923 qed
  1924 
  1925 lemma zero_less_mult_iff: "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0"
  1926   by (cases a 0 b 0 rule: linorder_cases[case_product linorder_cases])
  1927      (auto simp add: mult_neg_neg not_less le_less dest: zero_less_mult_pos zero_less_mult_pos2)
  1928 
  1929 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"
  1930   by (auto simp add: eq_commute [of 0] le_less not_less zero_less_mult_iff)
  1931 
  1932 lemma mult_less_0_iff: "a * b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b"
  1933   using zero_less_mult_iff [of "- a" b] by auto
  1934 
  1935 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"
  1936   using zero_le_mult_iff [of "- a" b] by auto
  1937 
  1938 text \<open>
  1939   Cancellation laws for @{term "c * a < c * b"} and @{term "a * c < b * c"},
  1940   also with the relations \<open>\<le>\<close> and equality.
  1941 \<close>
  1942 
  1943 text \<open>
  1944   These ``disjunction'' versions produce two cases when the comparison is
  1945   an assumption, but effectively four when the comparison is a goal.
  1946 \<close>
  1947 
  1948 lemma mult_less_cancel_right_disj: "a * c < b * c \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"
  1949   apply (cases "c = 0")
  1950    apply (auto simp add: neq_iff mult_strict_right_mono mult_strict_right_mono_neg)
  1951      apply (auto simp add: not_less not_le [symmetric, of "a*c"] not_le [symmetric, of a])
  1952      apply (erule_tac [!] notE)
  1953      apply (auto simp add: less_imp_le mult_right_mono mult_right_mono_neg)
  1954   done
  1955 
  1956 lemma mult_less_cancel_left_disj: "c * a < c * b \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"
  1957   apply (cases "c = 0")
  1958    apply (auto simp add: neq_iff mult_strict_left_mono mult_strict_left_mono_neg)
  1959      apply (auto simp add: not_less not_le [symmetric, of "c * a"] not_le [symmetric, of a])
  1960      apply (erule_tac [!] notE)
  1961      apply (auto simp add: less_imp_le mult_left_mono mult_left_mono_neg)
  1962   done
  1963 
  1964 text \<open>
  1965   The ``conjunction of implication'' lemmas produce two cases when the
  1966   comparison is a goal, but give four when the comparison is an assumption.
  1967 \<close>
  1968 
  1969 lemma mult_less_cancel_right: "a * c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)"
  1970   using mult_less_cancel_right_disj [of a c b] by auto
  1971 
  1972 lemma mult_less_cancel_left: "c * a < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)"
  1973   using mult_less_cancel_left_disj [of c a b] by auto
  1974 
  1975 lemma mult_le_cancel_right: "a * c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
  1976   by (simp add: not_less [symmetric] mult_less_cancel_right_disj)
  1977 
  1978 lemma mult_le_cancel_left: "c * a \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
  1979   by (simp add: not_less [symmetric] mult_less_cancel_left_disj)
  1980 
  1981 lemma mult_le_cancel_left_pos: "0 < c \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> a \<le> b"
  1982   by (auto simp: mult_le_cancel_left)
  1983 
  1984 lemma mult_le_cancel_left_neg: "c < 0 \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> b \<le> a"
  1985   by (auto simp: mult_le_cancel_left)
  1986 
  1987 lemma mult_less_cancel_left_pos: "0 < c \<Longrightarrow> c * a < c * b \<longleftrightarrow> a < b"
  1988   by (auto simp: mult_less_cancel_left)
  1989 
  1990 lemma mult_less_cancel_left_neg: "c < 0 \<Longrightarrow> c * a < c * b \<longleftrightarrow> b < a"
  1991   by (auto simp: mult_less_cancel_left)
  1992 
  1993 end
  1994 
  1995 lemmas mult_sign_intros =
  1996   mult_nonneg_nonneg mult_nonneg_nonpos
  1997   mult_nonpos_nonneg mult_nonpos_nonpos
  1998   mult_pos_pos mult_pos_neg
  1999   mult_neg_pos mult_neg_neg
  2000 
  2001 class ordered_comm_ring = comm_ring + ordered_comm_semiring
  2002 begin
  2003 
  2004 subclass ordered_ring ..
  2005 subclass ordered_cancel_comm_semiring ..
  2006 
  2007 end
  2008 
  2009 class zero_less_one = order + zero + one +
  2010   assumes zero_less_one [simp]: "0 < 1"
  2011 
  2012 class linordered_nonzero_semiring = ordered_comm_semiring + monoid_mult + linorder + zero_less_one
  2013 begin
  2014 
  2015 subclass zero_neq_one
  2016   by standard (insert zero_less_one, blast)
  2017 
  2018 subclass comm_semiring_1
  2019   by standard (rule mult_1_left)
  2020 
  2021 lemma zero_le_one [simp]: "0 \<le> 1"
  2022   by (rule zero_less_one [THEN less_imp_le])
  2023 
  2024 lemma not_one_le_zero [simp]: "\<not> 1 \<le> 0"
  2025   by (simp add: not_le)
  2026 
  2027 lemma not_one_less_zero [simp]: "\<not> 1 < 0"
  2028   by (simp add: not_less)
  2029 
  2030 lemma mult_left_le: "c \<le> 1 \<Longrightarrow> 0 \<le> a \<Longrightarrow> a * c \<le> a"
  2031   using mult_left_mono[of c 1 a] by simp
  2032 
  2033 lemma mult_le_one: "a \<le> 1 \<Longrightarrow> 0 \<le> b \<Longrightarrow> b \<le> 1 \<Longrightarrow> a * b \<le> 1"
  2034   using mult_mono[of a 1 b 1] by simp
  2035 
  2036 lemma zero_less_two: "0 < 1 + 1"
  2037   using add_pos_pos[OF zero_less_one zero_less_one] .
  2038 
  2039 end
  2040 
  2041 class linordered_semidom = semidom + linordered_comm_semiring_strict + zero_less_one +
  2042   assumes le_add_diff_inverse2 [simp]: "b \<le> a \<Longrightarrow> a - b + b = a"
  2043 begin
  2044 
  2045 subclass linordered_nonzero_semiring ..
  2046 
  2047 text \<open>Addition is the inverse of subtraction.\<close>
  2048 
  2049 lemma le_add_diff_inverse [simp]: "b \<le> a \<Longrightarrow> b + (a - b) = a"
  2050   by (frule le_add_diff_inverse2) (simp add: add.commute)
  2051 
  2052 lemma add_diff_inverse: "\<not> a < b \<Longrightarrow> b + (a - b) = a"
  2053   by simp
  2054 
  2055 lemma add_le_imp_le_diff: "i + k \<le> n \<Longrightarrow> i \<le> n - k"
  2056   apply (subst add_le_cancel_right [where c=k, symmetric])
  2057   apply (frule le_add_diff_inverse2)
  2058   apply (simp only: add.assoc [symmetric])
  2059   using add_implies_diff
  2060   apply fastforce
  2061   done
  2062 
  2063 lemma add_le_add_imp_diff_le:
  2064   assumes 1: "i + k \<le> n"
  2065     and 2: "n \<le> j + k"
  2066   shows "i + k \<le> n \<Longrightarrow> n \<le> j + k \<Longrightarrow> n - k \<le> j"
  2067 proof -
  2068   have "n - (i + k) + (i + k) = n"
  2069     using 1 by simp
  2070   moreover have "n - k = n - k - i + i"
  2071     using 1 by (simp add: add_le_imp_le_diff)
  2072   ultimately show ?thesis
  2073     using 2
  2074     apply (simp add: add.assoc [symmetric])
  2075     apply (rule add_le_imp_le_diff [of _ k "j + k", simplified add_diff_cancel_right'])
  2076     apply (simp add: add.commute diff_diff_add)
  2077     done
  2078 qed
  2079 
  2080 lemma less_1_mult: "1 < m \<Longrightarrow> 1 < n \<Longrightarrow> 1 < m * n"
  2081   using mult_strict_mono [of 1 m 1 n] by (simp add: less_trans [OF zero_less_one])
  2082 
  2083 end
  2084 
  2085 class linordered_idom =
  2086   comm_ring_1 + linordered_comm_semiring_strict + ordered_ab_group_add + abs_if + sgn +
  2087   assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
  2088 begin
  2089 
  2090 subclass linordered_semiring_1_strict ..
  2091 subclass linordered_ring_strict ..
  2092 subclass ordered_comm_ring ..
  2093 subclass idom ..
  2094 
  2095 subclass linordered_semidom
  2096 proof
  2097   have "0 \<le> 1 * 1" by (rule zero_le_square)
  2098   then show "0 < 1" by (simp add: le_less)
  2099   show "b \<le> a \<Longrightarrow> a - b + b = a" for a b by simp
  2100 qed
  2101 
  2102 subclass idom_abs_sgn
  2103   by standard
  2104     (auto simp add: sgn_if abs_if zero_less_mult_iff)
  2105 
  2106 lemma linorder_neqE_linordered_idom:
  2107   assumes "x \<noteq> y"
  2108   obtains "x < y" | "y < x"
  2109   using assms by (rule neqE)
  2110 
  2111 text \<open>These cancellation simp rules also produce two cases when the comparison is a goal.\<close>
  2112 
  2113 lemma mult_le_cancel_right1: "c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)"
  2114   using mult_le_cancel_right [of 1 c b] by simp
  2115 
  2116 lemma mult_le_cancel_right2: "a * c \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)"
  2117   using mult_le_cancel_right [of a c 1] by simp
  2118 
  2119 lemma mult_le_cancel_left1: "c \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)"
  2120   using mult_le_cancel_left [of c 1 b] by simp
  2121 
  2122 lemma mult_le_cancel_left2: "c * a \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)"
  2123   using mult_le_cancel_left [of c a 1] by simp
  2124 
  2125 lemma mult_less_cancel_right1: "c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)"
  2126   using mult_less_cancel_right [of 1 c b] by simp
  2127 
  2128 lemma mult_less_cancel_right2: "a * c < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"
  2129   using mult_less_cancel_right [of a c 1] by simp
  2130 
  2131 lemma mult_less_cancel_left1: "c < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)"
  2132   using mult_less_cancel_left [of c 1 b] by simp
  2133 
  2134 lemma mult_less_cancel_left2: "c * a < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"
  2135   using mult_less_cancel_left [of c a 1] by simp
  2136 
  2137 lemma sgn_0_0: "sgn a = 0 \<longleftrightarrow> a = 0"
  2138   by (fact sgn_eq_0_iff)
  2139 
  2140 lemma sgn_1_pos: "sgn a = 1 \<longleftrightarrow> a > 0"
  2141   unfolding sgn_if by simp
  2142 
  2143 lemma sgn_1_neg: "sgn a = - 1 \<longleftrightarrow> a < 0"
  2144   unfolding sgn_if by auto
  2145 
  2146 lemma sgn_pos [simp]: "0 < a \<Longrightarrow> sgn a = 1"
  2147   by (simp only: sgn_1_pos)
  2148 
  2149 lemma sgn_neg [simp]: "a < 0 \<Longrightarrow> sgn a = - 1"
  2150   by (simp only: sgn_1_neg)
  2151 
  2152 lemma abs_sgn: "\<bar>k\<bar> = k * sgn k"
  2153   unfolding sgn_if abs_if by auto
  2154 
  2155 lemma sgn_greater [simp]: "0 < sgn a \<longleftrightarrow> 0 < a"
  2156   unfolding sgn_if by auto
  2157 
  2158 lemma sgn_less [simp]: "sgn a < 0 \<longleftrightarrow> a < 0"
  2159   unfolding sgn_if by auto
  2160 
  2161 lemma abs_sgn_eq_1 [simp]:
  2162   "a \<noteq> 0 \<Longrightarrow> \<bar>sgn a\<bar> = 1"
  2163   by simp
  2164 
  2165 lemma abs_sgn_eq: "\<bar>sgn a\<bar> = (if a = 0 then 0 else 1)"
  2166   by (simp add: sgn_if)
  2167 
  2168 lemma sgn_mult_self_eq [simp]:
  2169   "sgn a * sgn a = of_bool (a \<noteq> 0)"
  2170   by (cases "a > 0") simp_all
  2171 
  2172 lemma abs_mult_self_eq [simp]:
  2173   "\<bar>a\<bar> * \<bar>a\<bar> = a * a"
  2174   by (cases "a > 0") simp_all
  2175 
  2176 lemma same_sgn_sgn_add:
  2177   "sgn (a + b) = sgn a" if "sgn b = sgn a"
  2178 proof (cases a 0 rule: linorder_cases)
  2179   case equal
  2180   with that show ?thesis
  2181     by simp
  2182 next
  2183   case less
  2184   with that have "b < 0"
  2185     by (simp add: sgn_1_neg)
  2186   with \<open>a < 0\<close> have "a + b < 0"
  2187     by (rule add_neg_neg)
  2188   with \<open>a < 0\<close> show ?thesis
  2189     by simp
  2190 next
  2191   case greater
  2192   with that have "b > 0"
  2193     by (simp add: sgn_1_pos)
  2194   with \<open>a > 0\<close> have "a + b > 0"
  2195     by (rule add_pos_pos)
  2196   with \<open>a > 0\<close> show ?thesis
  2197     by simp
  2198 qed
  2199 
  2200 lemma same_sgn_abs_add:
  2201   "\<bar>a + b\<bar> = \<bar>a\<bar> + \<bar>b\<bar>" if "sgn b = sgn a"
  2202 proof -
  2203   have "a + b = sgn a * \<bar>a\<bar> + sgn b * \<bar>b\<bar>"
  2204     by (simp add: sgn_mult_abs)
  2205   also have "\<dots> = sgn a * (\<bar>a\<bar> + \<bar>b\<bar>)"
  2206     using that by (simp add: algebra_simps)
  2207   finally show ?thesis
  2208     by (auto simp add: abs_mult)
  2209 qed
  2210 
  2211 lemma abs_dvd_iff [simp]: "\<bar>m\<bar> dvd k \<longleftrightarrow> m dvd k"
  2212   by (simp add: abs_if)
  2213 
  2214 lemma dvd_abs_iff [simp]: "m dvd \<bar>k\<bar> \<longleftrightarrow> m dvd k"
  2215   by (simp add: abs_if)
  2216 
  2217 lemma dvd_if_abs_eq: "\<bar>l\<bar> = \<bar>k\<bar> \<Longrightarrow> l dvd k"
  2218   by (subst abs_dvd_iff [symmetric]) simp
  2219 
  2220 text \<open>
  2221   The following lemmas can be proven in more general structures, but
  2222   are dangerous as simp rules in absence of @{thm neg_equal_zero},
  2223   @{thm neg_less_pos}, @{thm neg_less_eq_nonneg}.
  2224 \<close>
  2225 
  2226 lemma equation_minus_iff_1 [simp, no_atp]: "1 = - a \<longleftrightarrow> a = - 1"
  2227   by (fact equation_minus_iff)
  2228 
  2229 lemma minus_equation_iff_1 [simp, no_atp]: "- a = 1 \<longleftrightarrow> a = - 1"
  2230   by (subst minus_equation_iff, auto)
  2231 
  2232 lemma le_minus_iff_1 [simp, no_atp]: "1 \<le> - b \<longleftrightarrow> b \<le> - 1"
  2233   by (fact le_minus_iff)
  2234 
  2235 lemma minus_le_iff_1 [simp, no_atp]: "- a \<le> 1 \<longleftrightarrow> - 1 \<le> a"
  2236   by (fact minus_le_iff)
  2237 
  2238 lemma less_minus_iff_1 [simp, no_atp]: "1 < - b \<longleftrightarrow> b < - 1"
  2239   by (fact less_minus_iff)
  2240 
  2241 lemma minus_less_iff_1 [simp, no_atp]: "- a < 1 \<longleftrightarrow> - 1 < a"
  2242   by (fact minus_less_iff)
  2243 
  2244 end
  2245 
  2246 text \<open>Simprules for comparisons where common factors can be cancelled.\<close>
  2247 
  2248 lemmas mult_compare_simps =
  2249   mult_le_cancel_right mult_le_cancel_left
  2250   mult_le_cancel_right1 mult_le_cancel_right2
  2251   mult_le_cancel_left1 mult_le_cancel_left2
  2252   mult_less_cancel_right mult_less_cancel_left
  2253   mult_less_cancel_right1 mult_less_cancel_right2
  2254   mult_less_cancel_left1 mult_less_cancel_left2
  2255   mult_cancel_right mult_cancel_left
  2256   mult_cancel_right1 mult_cancel_right2
  2257   mult_cancel_left1 mult_cancel_left2
  2258 
  2259 
  2260 text \<open>Reasoning about inequalities with division\<close>
  2261 
  2262 context linordered_semidom
  2263 begin
  2264 
  2265 lemma less_add_one: "a < a + 1"
  2266 proof -
  2267   have "a + 0 < a + 1"
  2268     by (blast intro: zero_less_one add_strict_left_mono)
  2269   then show ?thesis by simp
  2270 qed
  2271 
  2272 end
  2273 
  2274 context linordered_idom
  2275 begin
  2276 
  2277 lemma mult_right_le_one_le: "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> x * y \<le> x"
  2278   by (rule mult_left_le)
  2279 
  2280 lemma mult_left_le_one_le: "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> y * x \<le> x"
  2281   by (auto simp add: mult_le_cancel_right2)
  2282 
  2283 end
  2284 
  2285 text \<open>Absolute Value\<close>
  2286 
  2287 context linordered_idom
  2288 begin
  2289 
  2290 lemma mult_sgn_abs: "sgn x * \<bar>x\<bar> = x"
  2291   by (fact sgn_mult_abs)
  2292 
  2293 lemma abs_one: "\<bar>1\<bar> = 1"
  2294   by (fact abs_1)
  2295 
  2296 end
  2297 
  2298 class ordered_ring_abs = ordered_ring + ordered_ab_group_add_abs +
  2299   assumes abs_eq_mult:
  2300     "(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>"
  2301 
  2302 context linordered_idom
  2303 begin
  2304 
  2305 subclass ordered_ring_abs
  2306   by standard (auto simp: abs_if not_less mult_less_0_iff)
  2307 
  2308 lemma abs_mult_self [simp]: "\<bar>a\<bar> * \<bar>a\<bar> = a * a"
  2309   by (simp add: abs_if)
  2310 
  2311 lemma abs_mult_less:
  2312   assumes ac: "\<bar>a\<bar> < c"
  2313     and bd: "\<bar>b\<bar> < d"
  2314   shows "\<bar>a\<bar> * \<bar>b\<bar> < c * d"
  2315 proof -
  2316   from ac have "0 < c"
  2317     by (blast intro: le_less_trans abs_ge_zero)
  2318   with bd show ?thesis by (simp add: ac mult_strict_mono)
  2319 qed
  2320 
  2321 lemma abs_less_iff: "\<bar>a\<bar> < b \<longleftrightarrow> a < b \<and> - a < b"
  2322   by (simp add: less_le abs_le_iff) (auto simp add: abs_if)
  2323 
  2324 lemma abs_mult_pos: "0 \<le> x \<Longrightarrow> \<bar>y\<bar> * x = \<bar>y * x\<bar>"
  2325   by (simp add: abs_mult)
  2326 
  2327 lemma abs_diff_less_iff: "\<bar>x - a\<bar> < r \<longleftrightarrow> a - r < x \<and> x < a + r"
  2328   by (auto simp add: diff_less_eq ac_simps abs_less_iff)
  2329 
  2330 lemma abs_diff_le_iff: "\<bar>x - a\<bar> \<le> r \<longleftrightarrow> a - r \<le> x \<and> x \<le> a + r"
  2331   by (auto simp add: diff_le_eq ac_simps abs_le_iff)
  2332 
  2333 lemma abs_add_one_gt_zero: "0 < 1 + \<bar>x\<bar>"
  2334   by (auto simp: abs_if not_less intro: zero_less_one add_strict_increasing less_trans)
  2335 
  2336 end
  2337 
  2338 subsection \<open>Dioids\<close>
  2339 
  2340 text \<open>
  2341   Dioids are the alternative extensions of semirings, a semiring can
  2342   either be a ring or a dioid but never both.
  2343 \<close>
  2344 
  2345 class dioid = semiring_1 + canonically_ordered_monoid_add
  2346 begin
  2347 
  2348 subclass ordered_semiring
  2349   by standard (auto simp: le_iff_add distrib_left distrib_right)
  2350 
  2351 end
  2352 
  2353 
  2354 hide_fact (open) comm_mult_left_mono comm_mult_strict_left_mono distrib
  2355 
  2356 code_identifier
  2357   code_module Rings \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
  2358 
  2359 end