src/HOL/Rings.thy
author haftmann
Sat Dec 17 15:22:14 2016 +0100 (2016-12-17)
changeset 64592 7759f1766189
parent 64591 240a39af9ec4
child 64713 9638c07283bc
permissions -rw-r--r--
more fine-grained type class hierarchy for div and mod
     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 normalization_semidom = algebraic_semidom +
  1160   fixes normalize :: "'a \<Rightarrow> 'a"
  1161     and unit_factor :: "'a \<Rightarrow> 'a"
  1162   assumes unit_factor_mult_normalize [simp]: "unit_factor a * normalize a = a"
  1163     and normalize_0 [simp]: "normalize 0 = 0"
  1164     and unit_factor_0 [simp]: "unit_factor 0 = 0"
  1165     and is_unit_normalize: "is_unit a  \<Longrightarrow> normalize a = 1"
  1166     and unit_factor_is_unit [iff]: "a \<noteq> 0 \<Longrightarrow> is_unit (unit_factor a)"
  1167     and unit_factor_mult: "unit_factor (a * b) = unit_factor a * unit_factor b"
  1168 begin
  1169 
  1170 text \<open>
  1171   Class @{class normalization_semidom} cultivates the idea that each integral
  1172   domain can be split into equivalence classes whose representants are
  1173   associated, i.e. divide each other. @{const normalize} specifies a canonical
  1174   representant for each equivalence class. The rationale behind this is that
  1175   it is easier to reason about equality than equivalences, hence we prefer to
  1176   think about equality of normalized values rather than associated elements.
  1177 \<close>
  1178 
  1179 lemma unit_factor_dvd [simp]: "a \<noteq> 0 \<Longrightarrow> unit_factor a dvd b"
  1180   by (rule unit_imp_dvd) simp
  1181 
  1182 lemma unit_factor_self [simp]: "unit_factor a dvd a"
  1183   by (cases "a = 0") simp_all
  1184 
  1185 lemma normalize_mult_unit_factor [simp]: "normalize a * unit_factor a = a"
  1186   using unit_factor_mult_normalize [of a] by (simp add: ac_simps)
  1187 
  1188 lemma normalize_eq_0_iff [simp]: "normalize a = 0 \<longleftrightarrow> a = 0"
  1189   (is "?lhs \<longleftrightarrow> ?rhs")
  1190 proof
  1191   assume ?lhs
  1192   moreover have "unit_factor a * normalize a = a" by simp
  1193   ultimately show ?rhs by simp
  1194 next
  1195   assume ?rhs
  1196   then show ?lhs by simp
  1197 qed
  1198 
  1199 lemma unit_factor_eq_0_iff [simp]: "unit_factor a = 0 \<longleftrightarrow> a = 0"
  1200   (is "?lhs \<longleftrightarrow> ?rhs")
  1201 proof
  1202   assume ?lhs
  1203   moreover have "unit_factor a * normalize a = a" by simp
  1204   ultimately show ?rhs by simp
  1205 next
  1206   assume ?rhs
  1207   then show ?lhs by simp
  1208 qed
  1209 
  1210 lemma is_unit_unit_factor:
  1211   assumes "is_unit a"
  1212   shows "unit_factor a = a"
  1213 proof -
  1214   from assms have "normalize a = 1" by (rule is_unit_normalize)
  1215   moreover from unit_factor_mult_normalize have "unit_factor a * normalize a = a" .
  1216   ultimately show ?thesis by simp
  1217 qed
  1218 
  1219 lemma unit_factor_1 [simp]: "unit_factor 1 = 1"
  1220   by (rule is_unit_unit_factor) simp
  1221 
  1222 lemma normalize_1 [simp]: "normalize 1 = 1"
  1223   by (rule is_unit_normalize) simp
  1224 
  1225 lemma normalize_1_iff: "normalize a = 1 \<longleftrightarrow> is_unit a"
  1226   (is "?lhs \<longleftrightarrow> ?rhs")
  1227 proof
  1228   assume ?rhs
  1229   then show ?lhs by (rule is_unit_normalize)
  1230 next
  1231   assume ?lhs
  1232   then have "unit_factor a * normalize a = unit_factor a * 1"
  1233     by simp
  1234   then have "unit_factor a = a"
  1235     by simp
  1236   moreover
  1237   from \<open>?lhs\<close> have "a \<noteq> 0" by auto
  1238   then have "is_unit (unit_factor a)" by simp
  1239   ultimately show ?rhs by simp
  1240 qed
  1241 
  1242 lemma div_normalize [simp]: "a div normalize a = unit_factor a"
  1243 proof (cases "a = 0")
  1244   case True
  1245   then show ?thesis by simp
  1246 next
  1247   case False
  1248   then have "normalize a \<noteq> 0" by simp
  1249   with nonzero_mult_div_cancel_right
  1250   have "unit_factor a * normalize a div normalize a = unit_factor a" by blast
  1251   then show ?thesis by simp
  1252 qed
  1253 
  1254 lemma div_unit_factor [simp]: "a div unit_factor a = normalize a"
  1255 proof (cases "a = 0")
  1256   case True
  1257   then show ?thesis by simp
  1258 next
  1259   case False
  1260   then have "unit_factor a \<noteq> 0" by simp
  1261   with nonzero_mult_div_cancel_left
  1262   have "unit_factor a * normalize a div unit_factor a = normalize a"
  1263     by blast
  1264   then show ?thesis by simp
  1265 qed
  1266 
  1267 lemma normalize_div [simp]: "normalize a div a = 1 div unit_factor a"
  1268 proof (cases "a = 0")
  1269   case True
  1270   then show ?thesis by simp
  1271 next
  1272   case False
  1273   have "normalize a div a = normalize a div (unit_factor a * normalize a)"
  1274     by simp
  1275   also have "\<dots> = 1 div unit_factor a"
  1276     using False by (subst is_unit_div_mult_cancel_right) simp_all
  1277   finally show ?thesis .
  1278 qed
  1279 
  1280 lemma mult_one_div_unit_factor [simp]: "a * (1 div unit_factor b) = a div unit_factor b"
  1281   by (cases "b = 0") simp_all
  1282 
  1283 lemma inv_unit_factor_eq_0_iff [simp]:
  1284   "1 div unit_factor a = 0 \<longleftrightarrow> a = 0"
  1285   (is "?lhs \<longleftrightarrow> ?rhs")
  1286 proof
  1287   assume ?lhs
  1288   then have "a * (1 div unit_factor a) = a * 0"
  1289     by simp
  1290   then show ?rhs
  1291     by simp
  1292 next
  1293   assume ?rhs
  1294   then show ?lhs by simp
  1295 qed
  1296 
  1297 lemma normalize_mult: "normalize (a * b) = normalize a * normalize b"
  1298 proof (cases "a = 0 \<or> b = 0")
  1299   case True
  1300   then show ?thesis by auto
  1301 next
  1302   case False
  1303   have "unit_factor (a * b) * normalize (a * b) = a * b"
  1304     by (rule unit_factor_mult_normalize)
  1305   then have "normalize (a * b) = a * b div unit_factor (a * b)"
  1306     by simp
  1307   also have "\<dots> = a * b div unit_factor (b * a)"
  1308     by (simp add: ac_simps)
  1309   also have "\<dots> = a * b div unit_factor b div unit_factor a"
  1310     using False by (simp add: unit_factor_mult is_unit_div_mult2_eq [symmetric])
  1311   also have "\<dots> = a * (b div unit_factor b) div unit_factor a"
  1312     using False by (subst unit_div_mult_swap) simp_all
  1313   also have "\<dots> = normalize a * normalize b"
  1314     using False
  1315     by (simp add: mult.commute [of a] mult.commute [of "normalize a"] unit_div_mult_swap [symmetric])
  1316   finally show ?thesis .
  1317 qed
  1318 
  1319 lemma unit_factor_idem [simp]: "unit_factor (unit_factor a) = unit_factor a"
  1320   by (cases "a = 0") (auto intro: is_unit_unit_factor)
  1321 
  1322 lemma normalize_unit_factor [simp]: "a \<noteq> 0 \<Longrightarrow> normalize (unit_factor a) = 1"
  1323   by (rule is_unit_normalize) simp
  1324 
  1325 lemma normalize_idem [simp]: "normalize (normalize a) = normalize a"
  1326 proof (cases "a = 0")
  1327   case True
  1328   then show ?thesis by simp
  1329 next
  1330   case False
  1331   have "normalize a = normalize (unit_factor a * normalize a)"
  1332     by simp
  1333   also have "\<dots> = normalize (unit_factor a) * normalize (normalize a)"
  1334     by (simp only: normalize_mult)
  1335   finally show ?thesis
  1336     using False by simp_all
  1337 qed
  1338 
  1339 lemma unit_factor_normalize [simp]:
  1340   assumes "a \<noteq> 0"
  1341   shows "unit_factor (normalize a) = 1"
  1342 proof -
  1343   from assms have *: "normalize a \<noteq> 0"
  1344     by simp
  1345   have "unit_factor (normalize a) * normalize (normalize a) = normalize a"
  1346     by (simp only: unit_factor_mult_normalize)
  1347   then have "unit_factor (normalize a) * normalize a = normalize a"
  1348     by simp
  1349   with * have "unit_factor (normalize a) * normalize a div normalize a = normalize a div normalize a"
  1350     by simp
  1351   with * show ?thesis
  1352     by simp
  1353 qed
  1354 
  1355 lemma dvd_unit_factor_div:
  1356   assumes "b dvd a"
  1357   shows "unit_factor (a div b) = unit_factor a div unit_factor b"
  1358 proof -
  1359   from assms have "a = a div b * b"
  1360     by simp
  1361   then have "unit_factor a = unit_factor (a div b * b)"
  1362     by simp
  1363   then show ?thesis
  1364     by (cases "b = 0") (simp_all add: unit_factor_mult)
  1365 qed
  1366 
  1367 lemma dvd_normalize_div:
  1368   assumes "b dvd a"
  1369   shows "normalize (a div b) = normalize a div normalize b"
  1370 proof -
  1371   from assms have "a = a div b * b"
  1372     by simp
  1373   then have "normalize a = normalize (a div b * b)"
  1374     by simp
  1375   then show ?thesis
  1376     by (cases "b = 0") (simp_all add: normalize_mult)
  1377 qed
  1378 
  1379 lemma normalize_dvd_iff [simp]: "normalize a dvd b \<longleftrightarrow> a dvd b"
  1380 proof -
  1381   have "normalize a dvd b \<longleftrightarrow> unit_factor a * normalize a dvd b"
  1382     using mult_unit_dvd_iff [of "unit_factor a" "normalize a" b]
  1383       by (cases "a = 0") simp_all
  1384   then show ?thesis by simp
  1385 qed
  1386 
  1387 lemma dvd_normalize_iff [simp]: "a dvd normalize b \<longleftrightarrow> a dvd b"
  1388 proof -
  1389   have "a dvd normalize  b \<longleftrightarrow> a dvd normalize b * unit_factor b"
  1390     using dvd_mult_unit_iff [of "unit_factor b" a "normalize b"]
  1391       by (cases "b = 0") simp_all
  1392   then show ?thesis by simp
  1393 qed
  1394 
  1395 text \<open>
  1396   We avoid an explicit definition of associated elements but prefer explicit
  1397   normalisation instead. In theory we could define an abbreviation like @{prop
  1398   "associated a b \<longleftrightarrow> normalize a = normalize b"} but this is counterproductive
  1399   without suggestive infix syntax, which we do not want to sacrifice for this
  1400   purpose here.
  1401 \<close>
  1402 
  1403 lemma associatedI:
  1404   assumes "a dvd b" and "b dvd a"
  1405   shows "normalize a = normalize b"
  1406 proof (cases "a = 0 \<or> b = 0")
  1407   case True
  1408   with assms show ?thesis by auto
  1409 next
  1410   case False
  1411   from \<open>a dvd b\<close> obtain c where b: "b = a * c" ..
  1412   moreover from \<open>b dvd a\<close> obtain d where a: "a = b * d" ..
  1413   ultimately have "b * 1 = b * (c * d)"
  1414     by (simp add: ac_simps)
  1415   with False have "1 = c * d"
  1416     unfolding mult_cancel_left by simp
  1417   then have "is_unit c" and "is_unit d"
  1418     by auto
  1419   with a b show ?thesis
  1420     by (simp add: normalize_mult is_unit_normalize)
  1421 qed
  1422 
  1423 lemma associatedD1: "normalize a = normalize b \<Longrightarrow> a dvd b"
  1424   using dvd_normalize_iff [of _ b, symmetric] normalize_dvd_iff [of a _, symmetric]
  1425   by simp
  1426 
  1427 lemma associatedD2: "normalize a = normalize b \<Longrightarrow> b dvd a"
  1428   using dvd_normalize_iff [of _ a, symmetric] normalize_dvd_iff [of b _, symmetric]
  1429   by simp
  1430 
  1431 lemma associated_unit: "normalize a = normalize b \<Longrightarrow> is_unit a \<Longrightarrow> is_unit b"
  1432   using dvd_unit_imp_unit by (auto dest!: associatedD1 associatedD2)
  1433 
  1434 lemma associated_iff_dvd: "normalize a = normalize b \<longleftrightarrow> a dvd b \<and> b dvd a"
  1435   (is "?lhs \<longleftrightarrow> ?rhs")
  1436 proof
  1437   assume ?rhs
  1438   then show ?lhs by (auto intro!: associatedI)
  1439 next
  1440   assume ?lhs
  1441   then have "unit_factor a * normalize a = unit_factor a * normalize b"
  1442     by simp
  1443   then have *: "normalize b * unit_factor a = a"
  1444     by (simp add: ac_simps)
  1445   show ?rhs
  1446   proof (cases "a = 0 \<or> b = 0")
  1447     case True
  1448     with \<open>?lhs\<close> show ?thesis by auto
  1449   next
  1450     case False
  1451     then have "b dvd normalize b * unit_factor a" and "normalize b * unit_factor a dvd b"
  1452       by (simp_all add: mult_unit_dvd_iff dvd_mult_unit_iff)
  1453     with * show ?thesis by simp
  1454   qed
  1455 qed
  1456 
  1457 lemma associated_eqI:
  1458   assumes "a dvd b" and "b dvd a"
  1459   assumes "normalize a = a" and "normalize b = b"
  1460   shows "a = b"
  1461 proof -
  1462   from assms have "normalize a = normalize b"
  1463     unfolding associated_iff_dvd by simp
  1464   with \<open>normalize a = a\<close> have "a = normalize b"
  1465     by simp
  1466   with \<open>normalize b = b\<close> show "a = b"
  1467     by simp
  1468 qed
  1469 
  1470 lemma normalize_unit_factor_eqI:
  1471   assumes "normalize a = normalize b"
  1472     and "unit_factor a = unit_factor b"
  1473   shows "a = b"
  1474 proof -
  1475   from assms have "unit_factor a * normalize a = unit_factor b * normalize b"
  1476     by simp
  1477   then show ?thesis
  1478     by simp
  1479 qed
  1480 
  1481 end
  1482 
  1483 
  1484 text \<open>Syntactic division remainder operator\<close>
  1485 
  1486 class modulo = dvd + divide +
  1487   fixes modulo :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "mod" 70)
  1488 
  1489 text \<open>Arbitrary quotient and remainder partitions\<close>
  1490 
  1491 class semiring_modulo = comm_semiring_1_cancel + divide + modulo +
  1492   assumes div_mult_mod_eq: "a div b * b + a mod b = a"
  1493 begin
  1494 
  1495 lemma mod_div_decomp:
  1496   fixes a b
  1497   obtains q r where "q = a div b" and "r = a mod b"
  1498     and "a = q * b + r"
  1499 proof -
  1500   from div_mult_mod_eq have "a = a div b * b + a mod b" by simp
  1501   moreover have "a div b = a div b" ..
  1502   moreover have "a mod b = a mod b" ..
  1503   note that ultimately show thesis by blast
  1504 qed
  1505 
  1506 lemma mult_div_mod_eq: "b * (a div b) + a mod b = a"
  1507   using div_mult_mod_eq [of a b] by (simp add: ac_simps)
  1508 
  1509 lemma mod_div_mult_eq: "a mod b + a div b * b = a"
  1510   using div_mult_mod_eq [of a b] by (simp add: ac_simps)
  1511 
  1512 lemma mod_mult_div_eq: "a mod b + b * (a div b) = a"
  1513   using div_mult_mod_eq [of a b] by (simp add: ac_simps)
  1514 
  1515 lemma minus_div_mult_eq_mod: "a - a div b * b = a mod b"
  1516   by (rule add_implies_diff [symmetric]) (fact mod_div_mult_eq)
  1517 
  1518 lemma minus_mult_div_eq_mod: "a - b * (a div b) = a mod b"
  1519   by (rule add_implies_diff [symmetric]) (fact mod_mult_div_eq)
  1520 
  1521 lemma minus_mod_eq_div_mult: "a - a mod b = a div b * b"
  1522   by (rule add_implies_diff [symmetric]) (fact div_mult_mod_eq)
  1523 
  1524 lemma minus_mod_eq_mult_div: "a - a mod b = b * (a div b)"
  1525   by (rule add_implies_diff [symmetric]) (fact mult_div_mod_eq)
  1526 
  1527 end
  1528 
  1529 
  1530 class ordered_semiring = semiring + ordered_comm_monoid_add +
  1531   assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
  1532   assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"
  1533 begin
  1534 
  1535 lemma mult_mono: "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * d"
  1536   apply (erule (1) mult_right_mono [THEN order_trans])
  1537   apply (erule (1) mult_left_mono)
  1538   done
  1539 
  1540 lemma mult_mono': "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * d"
  1541   by (rule mult_mono) (fast intro: order_trans)+
  1542 
  1543 end
  1544 
  1545 class ordered_semiring_0 = semiring_0 + ordered_semiring
  1546 begin
  1547 
  1548 lemma mult_nonneg_nonneg [simp]: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b"
  1549   using mult_left_mono [of 0 b a] by simp
  1550 
  1551 lemma mult_nonneg_nonpos: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> a * b \<le> 0"
  1552   using mult_left_mono [of b 0 a] by simp
  1553 
  1554 lemma mult_nonpos_nonneg: "a \<le> 0 \<Longrightarrow> 0 \<le> b \<Longrightarrow> a * b \<le> 0"
  1555   using mult_right_mono [of a 0 b] by simp
  1556 
  1557 text \<open>Legacy -- use @{thm [source] mult_nonpos_nonneg}.\<close>
  1558 lemma mult_nonneg_nonpos2: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> b * a \<le> 0"
  1559   by (drule mult_right_mono [of b 0]) auto
  1560 
  1561 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"
  1562   by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)
  1563 
  1564 end
  1565 
  1566 class ordered_cancel_semiring = ordered_semiring + cancel_comm_monoid_add
  1567 begin
  1568 
  1569 subclass semiring_0_cancel ..
  1570 
  1571 subclass ordered_semiring_0 ..
  1572 
  1573 end
  1574 
  1575 class linordered_semiring = ordered_semiring + linordered_cancel_ab_semigroup_add
  1576 begin
  1577 
  1578 subclass ordered_cancel_semiring ..
  1579 
  1580 subclass ordered_cancel_comm_monoid_add ..
  1581 
  1582 subclass ordered_ab_semigroup_monoid_add_imp_le ..
  1583 
  1584 lemma mult_left_less_imp_less: "c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
  1585   by (force simp add: mult_left_mono not_le [symmetric])
  1586 
  1587 lemma mult_right_less_imp_less: "a * c < b * c \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
  1588   by (force simp add: mult_right_mono not_le [symmetric])
  1589 
  1590 end
  1591 
  1592 class linordered_semiring_1 = linordered_semiring + semiring_1
  1593 begin
  1594 
  1595 lemma convex_bound_le:
  1596   assumes "x \<le> a" "y \<le> a" "0 \<le> u" "0 \<le> v" "u + v = 1"
  1597   shows "u * x + v * y \<le> a"
  1598 proof-
  1599   from assms have "u * x + v * y \<le> u * a + v * a"
  1600     by (simp add: add_mono mult_left_mono)
  1601   with assms show ?thesis
  1602     unfolding distrib_right[symmetric] by simp
  1603 qed
  1604 
  1605 end
  1606 
  1607 class linordered_semiring_strict = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add +
  1608   assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
  1609   assumes mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c"
  1610 begin
  1611 
  1612 subclass semiring_0_cancel ..
  1613 
  1614 subclass linordered_semiring
  1615 proof
  1616   fix a b c :: 'a
  1617   assume *: "a \<le> b" "0 \<le> c"
  1618   then show "c * a \<le> c * b"
  1619     unfolding le_less
  1620     using mult_strict_left_mono by (cases "c = 0") auto
  1621   from * show "a * c \<le> b * c"
  1622     unfolding le_less
  1623     using mult_strict_right_mono by (cases "c = 0") auto
  1624 qed
  1625 
  1626 lemma mult_left_le_imp_le: "c * a \<le> c * b \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
  1627   by (auto simp add: mult_strict_left_mono _not_less [symmetric])
  1628 
  1629 lemma mult_right_le_imp_le: "a * c \<le> b * c \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
  1630   by (auto simp add: mult_strict_right_mono not_less [symmetric])
  1631 
  1632 lemma mult_pos_pos[simp]: "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a * b"
  1633   using mult_strict_left_mono [of 0 b a] by simp
  1634 
  1635 lemma mult_pos_neg: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> a * b < 0"
  1636   using mult_strict_left_mono [of b 0 a] by simp
  1637 
  1638 lemma mult_neg_pos: "a < 0 \<Longrightarrow> 0 < b \<Longrightarrow> a * b < 0"
  1639   using mult_strict_right_mono [of a 0 b] by simp
  1640 
  1641 text \<open>Legacy -- use @{thm [source] mult_neg_pos}.\<close>
  1642 lemma mult_pos_neg2: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> b * a < 0"
  1643   by (drule mult_strict_right_mono [of b 0]) auto
  1644 
  1645 lemma zero_less_mult_pos: "0 < a * b \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"
  1646   apply (cases "b \<le> 0")
  1647    apply (auto simp add: le_less not_less)
  1648   apply (drule_tac mult_pos_neg [of a b])
  1649    apply (auto dest: less_not_sym)
  1650   done
  1651 
  1652 lemma zero_less_mult_pos2: "0 < b * a \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"
  1653   apply (cases "b \<le> 0")
  1654    apply (auto simp add: le_less not_less)
  1655   apply (drule_tac mult_pos_neg2 [of a b])
  1656    apply (auto dest: less_not_sym)
  1657   done
  1658 
  1659 text \<open>Strict monotonicity in both arguments\<close>
  1660 lemma mult_strict_mono:
  1661   assumes "a < b" and "c < d" and "0 < b" and "0 \<le> c"
  1662   shows "a * c < b * d"
  1663   using assms
  1664   apply (cases "c = 0")
  1665    apply simp
  1666   apply (erule mult_strict_right_mono [THEN less_trans])
  1667    apply (auto simp add: le_less)
  1668   apply (erule (1) mult_strict_left_mono)
  1669   done
  1670 
  1671 text \<open>This weaker variant has more natural premises\<close>
  1672 lemma mult_strict_mono':
  1673   assumes "a < b" and "c < d" and "0 \<le> a" and "0 \<le> c"
  1674   shows "a * c < b * d"
  1675   by (rule mult_strict_mono) (insert assms, auto)
  1676 
  1677 lemma mult_less_le_imp_less:
  1678   assumes "a < b" and "c \<le> d" and "0 \<le> a" and "0 < c"
  1679   shows "a * c < b * d"
  1680   using assms
  1681   apply (subgoal_tac "a * c < b * c")
  1682    apply (erule less_le_trans)
  1683    apply (erule mult_left_mono)
  1684    apply simp
  1685   apply (erule (1) mult_strict_right_mono)
  1686   done
  1687 
  1688 lemma mult_le_less_imp_less:
  1689   assumes "a \<le> b" and "c < d" and "0 < a" and "0 \<le> c"
  1690   shows "a * c < b * d"
  1691   using assms
  1692   apply (subgoal_tac "a * c \<le> b * c")
  1693    apply (erule le_less_trans)
  1694    apply (erule mult_strict_left_mono)
  1695    apply simp
  1696   apply (erule (1) mult_right_mono)
  1697   done
  1698 
  1699 end
  1700 
  1701 class linordered_semiring_1_strict = linordered_semiring_strict + semiring_1
  1702 begin
  1703 
  1704 subclass linordered_semiring_1 ..
  1705 
  1706 lemma convex_bound_lt:
  1707   assumes "x < a" "y < a" "0 \<le> u" "0 \<le> v" "u + v = 1"
  1708   shows "u * x + v * y < a"
  1709 proof -
  1710   from assms have "u * x + v * y < u * a + v * a"
  1711     by (cases "u = 0") (auto intro!: add_less_le_mono mult_strict_left_mono mult_left_mono)
  1712   with assms show ?thesis
  1713     unfolding distrib_right[symmetric] by simp
  1714 qed
  1715 
  1716 end
  1717 
  1718 class ordered_comm_semiring = comm_semiring_0 + ordered_ab_semigroup_add +
  1719   assumes comm_mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
  1720 begin
  1721 
  1722 subclass ordered_semiring
  1723 proof
  1724   fix a b c :: 'a
  1725   assume "a \<le> b" "0 \<le> c"
  1726   then show "c * a \<le> c * b" by (rule comm_mult_left_mono)
  1727   then show "a * c \<le> b * c" by (simp only: mult.commute)
  1728 qed
  1729 
  1730 end
  1731 
  1732 class ordered_cancel_comm_semiring = ordered_comm_semiring + cancel_comm_monoid_add
  1733 begin
  1734 
  1735 subclass comm_semiring_0_cancel ..
  1736 subclass ordered_comm_semiring ..
  1737 subclass ordered_cancel_semiring ..
  1738 
  1739 end
  1740 
  1741 class linordered_comm_semiring_strict = comm_semiring_0 + linordered_cancel_ab_semigroup_add +
  1742   assumes comm_mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
  1743 begin
  1744 
  1745 subclass linordered_semiring_strict
  1746 proof
  1747   fix a b c :: 'a
  1748   assume "a < b" "0 < c"
  1749   then show "c * a < c * b"
  1750     by (rule comm_mult_strict_left_mono)
  1751   then show "a * c < b * c"
  1752     by (simp only: mult.commute)
  1753 qed
  1754 
  1755 subclass ordered_cancel_comm_semiring
  1756 proof
  1757   fix a b c :: 'a
  1758   assume "a \<le> b" "0 \<le> c"
  1759   then show "c * a \<le> c * b"
  1760     unfolding le_less
  1761     using mult_strict_left_mono by (cases "c = 0") auto
  1762 qed
  1763 
  1764 end
  1765 
  1766 class ordered_ring = ring + ordered_cancel_semiring
  1767 begin
  1768 
  1769 subclass ordered_ab_group_add ..
  1770 
  1771 lemma less_add_iff1: "a * e + c < b * e + d \<longleftrightarrow> (a - b) * e + c < d"
  1772   by (simp add: algebra_simps)
  1773 
  1774 lemma less_add_iff2: "a * e + c < b * e + d \<longleftrightarrow> c < (b - a) * e + d"
  1775   by (simp add: algebra_simps)
  1776 
  1777 lemma le_add_iff1: "a * e + c \<le> b * e + d \<longleftrightarrow> (a - b) * e + c \<le> d"
  1778   by (simp add: algebra_simps)
  1779 
  1780 lemma le_add_iff2: "a * e + c \<le> b * e + d \<longleftrightarrow> c \<le> (b - a) * e + d"
  1781   by (simp add: algebra_simps)
  1782 
  1783 lemma mult_left_mono_neg: "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> c * a \<le> c * b"
  1784   apply (drule mult_left_mono [of _ _ "- c"])
  1785   apply simp_all
  1786   done
  1787 
  1788 lemma mult_right_mono_neg: "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> a * c \<le> b * c"
  1789   apply (drule mult_right_mono [of _ _ "- c"])
  1790   apply simp_all
  1791   done
  1792 
  1793 lemma mult_nonpos_nonpos: "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> 0 \<le> a * b"
  1794   using mult_right_mono_neg [of a 0 b] by simp
  1795 
  1796 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"
  1797   by (auto simp add: mult_nonpos_nonpos)
  1798 
  1799 end
  1800 
  1801 class abs_if = minus + uminus + ord + zero + abs +
  1802   assumes abs_if: "\<bar>a\<bar> = (if a < 0 then - a else a)"
  1803 
  1804 class linordered_ring = ring + linordered_semiring + linordered_ab_group_add + abs_if
  1805 begin
  1806 
  1807 subclass ordered_ring ..
  1808 
  1809 subclass ordered_ab_group_add_abs
  1810 proof
  1811   fix a b
  1812   show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
  1813     by (auto simp add: abs_if not_le not_less algebra_simps
  1814         simp del: add.commute dest: add_neg_neg add_nonneg_nonneg)
  1815 qed (auto simp: abs_if)
  1816 
  1817 lemma zero_le_square [simp]: "0 \<le> a * a"
  1818   using linear [of 0 a] by (auto simp add: mult_nonpos_nonpos)
  1819 
  1820 lemma not_square_less_zero [simp]: "\<not> (a * a < 0)"
  1821   by (simp add: not_less)
  1822 
  1823 proposition abs_eq_iff: "\<bar>x\<bar> = \<bar>y\<bar> \<longleftrightarrow> x = y \<or> x = -y"
  1824   by (auto simp add: abs_if split: if_split_asm)
  1825 
  1826 lemma sum_squares_ge_zero: "0 \<le> x * x + y * y"
  1827   by (intro add_nonneg_nonneg zero_le_square)
  1828 
  1829 lemma not_sum_squares_lt_zero: "\<not> x * x + y * y < 0"
  1830   by (simp add: not_less sum_squares_ge_zero)
  1831 
  1832 end
  1833 
  1834 class linordered_ring_strict = ring + linordered_semiring_strict
  1835   + ordered_ab_group_add + abs_if
  1836 begin
  1837 
  1838 subclass linordered_ring ..
  1839 
  1840 lemma mult_strict_left_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> c * a < c * b"
  1841   using mult_strict_left_mono [of b a "- c"] by simp
  1842 
  1843 lemma mult_strict_right_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> a * c < b * c"
  1844   using mult_strict_right_mono [of b a "- c"] by simp
  1845 
  1846 lemma mult_neg_neg: "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> 0 < a * b"
  1847   using mult_strict_right_mono_neg [of a 0 b] by simp
  1848 
  1849 subclass ring_no_zero_divisors
  1850 proof
  1851   fix a b
  1852   assume "a \<noteq> 0"
  1853   then have a: "a < 0 \<or> 0 < a" by (simp add: neq_iff)
  1854   assume "b \<noteq> 0"
  1855   then have b: "b < 0 \<or> 0 < b" by (simp add: neq_iff)
  1856   have "a * b < 0 \<or> 0 < a * b"
  1857   proof (cases "a < 0")
  1858     case True
  1859     show ?thesis
  1860     proof (cases "b < 0")
  1861       case True
  1862       with \<open>a < 0\<close> show ?thesis by (auto dest: mult_neg_neg)
  1863     next
  1864       case False
  1865       with b have "0 < b" by auto
  1866       with \<open>a < 0\<close> show ?thesis by (auto dest: mult_strict_right_mono)
  1867     qed
  1868   next
  1869     case False
  1870     with a have "0 < a" by auto
  1871     show ?thesis
  1872     proof (cases "b < 0")
  1873       case True
  1874       with \<open>0 < a\<close> show ?thesis
  1875         by (auto dest: mult_strict_right_mono_neg)
  1876     next
  1877       case False
  1878       with b have "0 < b" by auto
  1879       with \<open>0 < a\<close> show ?thesis by auto
  1880     qed
  1881   qed
  1882   then show "a * b \<noteq> 0"
  1883     by (simp add: neq_iff)
  1884 qed
  1885 
  1886 lemma zero_less_mult_iff: "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0"
  1887   by (cases a 0 b 0 rule: linorder_cases[case_product linorder_cases])
  1888      (auto simp add: mult_neg_neg not_less le_less dest: zero_less_mult_pos zero_less_mult_pos2)
  1889 
  1890 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"
  1891   by (auto simp add: eq_commute [of 0] le_less not_less zero_less_mult_iff)
  1892 
  1893 lemma mult_less_0_iff: "a * b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b"
  1894   using zero_less_mult_iff [of "- a" b] by auto
  1895 
  1896 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"
  1897   using zero_le_mult_iff [of "- a" b] by auto
  1898 
  1899 text \<open>
  1900   Cancellation laws for @{term "c * a < c * b"} and @{term "a * c < b * c"},
  1901   also with the relations \<open>\<le>\<close> and equality.
  1902 \<close>
  1903 
  1904 text \<open>
  1905   These ``disjunction'' versions produce two cases when the comparison is
  1906   an assumption, but effectively four when the comparison is a goal.
  1907 \<close>
  1908 
  1909 lemma mult_less_cancel_right_disj: "a * c < b * c \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"
  1910   apply (cases "c = 0")
  1911    apply (auto simp add: neq_iff mult_strict_right_mono mult_strict_right_mono_neg)
  1912      apply (auto simp add: not_less not_le [symmetric, of "a*c"] not_le [symmetric, of a])
  1913      apply (erule_tac [!] notE)
  1914      apply (auto simp add: less_imp_le mult_right_mono mult_right_mono_neg)
  1915   done
  1916 
  1917 lemma mult_less_cancel_left_disj: "c * a < c * b \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"
  1918   apply (cases "c = 0")
  1919    apply (auto simp add: neq_iff mult_strict_left_mono mult_strict_left_mono_neg)
  1920      apply (auto simp add: not_less not_le [symmetric, of "c * a"] not_le [symmetric, of a])
  1921      apply (erule_tac [!] notE)
  1922      apply (auto simp add: less_imp_le mult_left_mono mult_left_mono_neg)
  1923   done
  1924 
  1925 text \<open>
  1926   The ``conjunction of implication'' lemmas produce two cases when the
  1927   comparison is a goal, but give four when the comparison is an assumption.
  1928 \<close>
  1929 
  1930 lemma mult_less_cancel_right: "a * c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)"
  1931   using mult_less_cancel_right_disj [of a c b] by auto
  1932 
  1933 lemma mult_less_cancel_left: "c * a < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)"
  1934   using mult_less_cancel_left_disj [of c a b] by auto
  1935 
  1936 lemma mult_le_cancel_right: "a * c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
  1937   by (simp add: not_less [symmetric] mult_less_cancel_right_disj)
  1938 
  1939 lemma mult_le_cancel_left: "c * a \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
  1940   by (simp add: not_less [symmetric] mult_less_cancel_left_disj)
  1941 
  1942 lemma mult_le_cancel_left_pos: "0 < c \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> a \<le> b"
  1943   by (auto simp: mult_le_cancel_left)
  1944 
  1945 lemma mult_le_cancel_left_neg: "c < 0 \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> b \<le> a"
  1946   by (auto simp: mult_le_cancel_left)
  1947 
  1948 lemma mult_less_cancel_left_pos: "0 < c \<Longrightarrow> c * a < c * b \<longleftrightarrow> a < b"
  1949   by (auto simp: mult_less_cancel_left)
  1950 
  1951 lemma mult_less_cancel_left_neg: "c < 0 \<Longrightarrow> c * a < c * b \<longleftrightarrow> b < a"
  1952   by (auto simp: mult_less_cancel_left)
  1953 
  1954 end
  1955 
  1956 lemmas mult_sign_intros =
  1957   mult_nonneg_nonneg mult_nonneg_nonpos
  1958   mult_nonpos_nonneg mult_nonpos_nonpos
  1959   mult_pos_pos mult_pos_neg
  1960   mult_neg_pos mult_neg_neg
  1961 
  1962 class ordered_comm_ring = comm_ring + ordered_comm_semiring
  1963 begin
  1964 
  1965 subclass ordered_ring ..
  1966 subclass ordered_cancel_comm_semiring ..
  1967 
  1968 end
  1969 
  1970 class zero_less_one = order + zero + one +
  1971   assumes zero_less_one [simp]: "0 < 1"
  1972 
  1973 class linordered_nonzero_semiring = ordered_comm_semiring + monoid_mult + linorder + zero_less_one
  1974 begin
  1975 
  1976 subclass zero_neq_one
  1977   by standard (insert zero_less_one, blast)
  1978 
  1979 subclass comm_semiring_1
  1980   by standard (rule mult_1_left)
  1981 
  1982 lemma zero_le_one [simp]: "0 \<le> 1"
  1983   by (rule zero_less_one [THEN less_imp_le])
  1984 
  1985 lemma not_one_le_zero [simp]: "\<not> 1 \<le> 0"
  1986   by (simp add: not_le)
  1987 
  1988 lemma not_one_less_zero [simp]: "\<not> 1 < 0"
  1989   by (simp add: not_less)
  1990 
  1991 lemma mult_left_le: "c \<le> 1 \<Longrightarrow> 0 \<le> a \<Longrightarrow> a * c \<le> a"
  1992   using mult_left_mono[of c 1 a] by simp
  1993 
  1994 lemma mult_le_one: "a \<le> 1 \<Longrightarrow> 0 \<le> b \<Longrightarrow> b \<le> 1 \<Longrightarrow> a * b \<le> 1"
  1995   using mult_mono[of a 1 b 1] by simp
  1996 
  1997 lemma zero_less_two: "0 < 1 + 1"
  1998   using add_pos_pos[OF zero_less_one zero_less_one] .
  1999 
  2000 end
  2001 
  2002 class linordered_semidom = semidom + linordered_comm_semiring_strict + zero_less_one +
  2003   assumes le_add_diff_inverse2 [simp]: "b \<le> a \<Longrightarrow> a - b + b = a"
  2004 begin
  2005 
  2006 subclass linordered_nonzero_semiring ..
  2007 
  2008 text \<open>Addition is the inverse of subtraction.\<close>
  2009 
  2010 lemma le_add_diff_inverse [simp]: "b \<le> a \<Longrightarrow> b + (a - b) = a"
  2011   by (frule le_add_diff_inverse2) (simp add: add.commute)
  2012 
  2013 lemma add_diff_inverse: "\<not> a < b \<Longrightarrow> b + (a - b) = a"
  2014   by simp
  2015 
  2016 lemma add_le_imp_le_diff: "i + k \<le> n \<Longrightarrow> i \<le> n - k"
  2017   apply (subst add_le_cancel_right [where c=k, symmetric])
  2018   apply (frule le_add_diff_inverse2)
  2019   apply (simp only: add.assoc [symmetric])
  2020   using add_implies_diff
  2021   apply fastforce
  2022   done
  2023 
  2024 lemma add_le_add_imp_diff_le:
  2025   assumes 1: "i + k \<le> n"
  2026     and 2: "n \<le> j + k"
  2027   shows "i + k \<le> n \<Longrightarrow> n \<le> j + k \<Longrightarrow> n - k \<le> j"
  2028 proof -
  2029   have "n - (i + k) + (i + k) = n"
  2030     using 1 by simp
  2031   moreover have "n - k = n - k - i + i"
  2032     using 1 by (simp add: add_le_imp_le_diff)
  2033   ultimately show ?thesis
  2034     using 2
  2035     apply (simp add: add.assoc [symmetric])
  2036     apply (rule add_le_imp_le_diff [of _ k "j + k", simplified add_diff_cancel_right'])
  2037     apply (simp add: add.commute diff_diff_add)
  2038     done
  2039 qed
  2040 
  2041 lemma less_1_mult: "1 < m \<Longrightarrow> 1 < n \<Longrightarrow> 1 < m * n"
  2042   using mult_strict_mono [of 1 m 1 n] by (simp add: less_trans [OF zero_less_one])
  2043 
  2044 end
  2045 
  2046 class linordered_idom =
  2047   comm_ring_1 + linordered_comm_semiring_strict + ordered_ab_group_add + abs_if + sgn +
  2048   assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
  2049 begin
  2050 
  2051 subclass linordered_semiring_1_strict ..
  2052 subclass linordered_ring_strict ..
  2053 subclass ordered_comm_ring ..
  2054 subclass idom ..
  2055 
  2056 subclass linordered_semidom
  2057 proof
  2058   have "0 \<le> 1 * 1" by (rule zero_le_square)
  2059   then show "0 < 1" by (simp add: le_less)
  2060   show "b \<le> a \<Longrightarrow> a - b + b = a" for a b by simp
  2061 qed
  2062 
  2063 subclass idom_abs_sgn
  2064   by standard
  2065     (auto simp add: sgn_if abs_if zero_less_mult_iff)
  2066 
  2067 lemma linorder_neqE_linordered_idom:
  2068   assumes "x \<noteq> y"
  2069   obtains "x < y" | "y < x"
  2070   using assms by (rule neqE)
  2071 
  2072 text \<open>These cancellation simp rules also produce two cases when the comparison is a goal.\<close>
  2073 
  2074 lemma mult_le_cancel_right1: "c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)"
  2075   using mult_le_cancel_right [of 1 c b] by simp
  2076 
  2077 lemma mult_le_cancel_right2: "a * c \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)"
  2078   using mult_le_cancel_right [of a c 1] by simp
  2079 
  2080 lemma mult_le_cancel_left1: "c \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)"
  2081   using mult_le_cancel_left [of c 1 b] by simp
  2082 
  2083 lemma mult_le_cancel_left2: "c * a \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)"
  2084   using mult_le_cancel_left [of c a 1] by simp
  2085 
  2086 lemma mult_less_cancel_right1: "c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)"
  2087   using mult_less_cancel_right [of 1 c b] by simp
  2088 
  2089 lemma mult_less_cancel_right2: "a * c < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"
  2090   using mult_less_cancel_right [of a c 1] by simp
  2091 
  2092 lemma mult_less_cancel_left1: "c < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)"
  2093   using mult_less_cancel_left [of c 1 b] by simp
  2094 
  2095 lemma mult_less_cancel_left2: "c * a < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"
  2096   using mult_less_cancel_left [of c a 1] by simp
  2097 
  2098 lemma sgn_0_0: "sgn a = 0 \<longleftrightarrow> a = 0"
  2099   by (fact sgn_eq_0_iff)
  2100 
  2101 lemma sgn_1_pos: "sgn a = 1 \<longleftrightarrow> a > 0"
  2102   unfolding sgn_if by simp
  2103 
  2104 lemma sgn_1_neg: "sgn a = - 1 \<longleftrightarrow> a < 0"
  2105   unfolding sgn_if by auto
  2106 
  2107 lemma sgn_pos [simp]: "0 < a \<Longrightarrow> sgn a = 1"
  2108   by (simp only: sgn_1_pos)
  2109 
  2110 lemma sgn_neg [simp]: "a < 0 \<Longrightarrow> sgn a = - 1"
  2111   by (simp only: sgn_1_neg)
  2112 
  2113 lemma abs_sgn: "\<bar>k\<bar> = k * sgn k"
  2114   unfolding sgn_if abs_if by auto
  2115 
  2116 lemma sgn_greater [simp]: "0 < sgn a \<longleftrightarrow> 0 < a"
  2117   unfolding sgn_if by auto
  2118 
  2119 lemma sgn_less [simp]: "sgn a < 0 \<longleftrightarrow> a < 0"
  2120   unfolding sgn_if by auto
  2121 
  2122 lemma abs_sgn_eq_1 [simp]:
  2123   "a \<noteq> 0 \<Longrightarrow> \<bar>sgn a\<bar> = 1"
  2124   by simp
  2125 
  2126 lemma abs_sgn_eq: "\<bar>sgn a\<bar> = (if a = 0 then 0 else 1)"
  2127   by (simp add: sgn_if)
  2128 
  2129 lemma abs_dvd_iff [simp]: "\<bar>m\<bar> dvd k \<longleftrightarrow> m dvd k"
  2130   by (simp add: abs_if)
  2131 
  2132 lemma dvd_abs_iff [simp]: "m dvd \<bar>k\<bar> \<longleftrightarrow> m dvd k"
  2133   by (simp add: abs_if)
  2134 
  2135 lemma dvd_if_abs_eq: "\<bar>l\<bar> = \<bar>k\<bar> \<Longrightarrow> l dvd k"
  2136   by (subst abs_dvd_iff [symmetric]) simp
  2137 
  2138 text \<open>
  2139   The following lemmas can be proven in more general structures, but
  2140   are dangerous as simp rules in absence of @{thm neg_equal_zero},
  2141   @{thm neg_less_pos}, @{thm neg_less_eq_nonneg}.
  2142 \<close>
  2143 
  2144 lemma equation_minus_iff_1 [simp, no_atp]: "1 = - a \<longleftrightarrow> a = - 1"
  2145   by (fact equation_minus_iff)
  2146 
  2147 lemma minus_equation_iff_1 [simp, no_atp]: "- a = 1 \<longleftrightarrow> a = - 1"
  2148   by (subst minus_equation_iff, auto)
  2149 
  2150 lemma le_minus_iff_1 [simp, no_atp]: "1 \<le> - b \<longleftrightarrow> b \<le> - 1"
  2151   by (fact le_minus_iff)
  2152 
  2153 lemma minus_le_iff_1 [simp, no_atp]: "- a \<le> 1 \<longleftrightarrow> - 1 \<le> a"
  2154   by (fact minus_le_iff)
  2155 
  2156 lemma less_minus_iff_1 [simp, no_atp]: "1 < - b \<longleftrightarrow> b < - 1"
  2157   by (fact less_minus_iff)
  2158 
  2159 lemma minus_less_iff_1 [simp, no_atp]: "- a < 1 \<longleftrightarrow> - 1 < a"
  2160   by (fact minus_less_iff)
  2161 
  2162 end
  2163 
  2164 text \<open>Simprules for comparisons where common factors can be cancelled.\<close>
  2165 
  2166 lemmas mult_compare_simps =
  2167   mult_le_cancel_right mult_le_cancel_left
  2168   mult_le_cancel_right1 mult_le_cancel_right2
  2169   mult_le_cancel_left1 mult_le_cancel_left2
  2170   mult_less_cancel_right mult_less_cancel_left
  2171   mult_less_cancel_right1 mult_less_cancel_right2
  2172   mult_less_cancel_left1 mult_less_cancel_left2
  2173   mult_cancel_right mult_cancel_left
  2174   mult_cancel_right1 mult_cancel_right2
  2175   mult_cancel_left1 mult_cancel_left2
  2176 
  2177 
  2178 text \<open>Reasoning about inequalities with division\<close>
  2179 
  2180 context linordered_semidom
  2181 begin
  2182 
  2183 lemma less_add_one: "a < a + 1"
  2184 proof -
  2185   have "a + 0 < a + 1"
  2186     by (blast intro: zero_less_one add_strict_left_mono)
  2187   then show ?thesis by simp
  2188 qed
  2189 
  2190 end
  2191 
  2192 context linordered_idom
  2193 begin
  2194 
  2195 lemma mult_right_le_one_le: "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> x * y \<le> x"
  2196   by (rule mult_left_le)
  2197 
  2198 lemma mult_left_le_one_le: "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> y * x \<le> x"
  2199   by (auto simp add: mult_le_cancel_right2)
  2200 
  2201 end
  2202 
  2203 text \<open>Absolute Value\<close>
  2204 
  2205 context linordered_idom
  2206 begin
  2207 
  2208 lemma mult_sgn_abs: "sgn x * \<bar>x\<bar> = x"
  2209   by (fact sgn_mult_abs)
  2210 
  2211 lemma abs_one: "\<bar>1\<bar> = 1"
  2212   by (fact abs_1)
  2213 
  2214 end
  2215 
  2216 class ordered_ring_abs = ordered_ring + ordered_ab_group_add_abs +
  2217   assumes abs_eq_mult:
  2218     "(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>"
  2219 
  2220 context linordered_idom
  2221 begin
  2222 
  2223 subclass ordered_ring_abs
  2224   by standard (auto simp: abs_if not_less mult_less_0_iff)
  2225 
  2226 lemma abs_mult_self [simp]: "\<bar>a\<bar> * \<bar>a\<bar> = a * a"
  2227   by (simp add: abs_if)
  2228 
  2229 lemma abs_mult_less:
  2230   assumes ac: "\<bar>a\<bar> < c"
  2231     and bd: "\<bar>b\<bar> < d"
  2232   shows "\<bar>a\<bar> * \<bar>b\<bar> < c * d"
  2233 proof -
  2234   from ac have "0 < c"
  2235     by (blast intro: le_less_trans abs_ge_zero)
  2236   with bd show ?thesis by (simp add: ac mult_strict_mono)
  2237 qed
  2238 
  2239 lemma abs_less_iff: "\<bar>a\<bar> < b \<longleftrightarrow> a < b \<and> - a < b"
  2240   by (simp add: less_le abs_le_iff) (auto simp add: abs_if)
  2241 
  2242 lemma abs_mult_pos: "0 \<le> x \<Longrightarrow> \<bar>y\<bar> * x = \<bar>y * x\<bar>"
  2243   by (simp add: abs_mult)
  2244 
  2245 lemma abs_diff_less_iff: "\<bar>x - a\<bar> < r \<longleftrightarrow> a - r < x \<and> x < a + r"
  2246   by (auto simp add: diff_less_eq ac_simps abs_less_iff)
  2247 
  2248 lemma abs_diff_le_iff: "\<bar>x - a\<bar> \<le> r \<longleftrightarrow> a - r \<le> x \<and> x \<le> a + r"
  2249   by (auto simp add: diff_le_eq ac_simps abs_le_iff)
  2250 
  2251 lemma abs_add_one_gt_zero: "0 < 1 + \<bar>x\<bar>"
  2252   by (auto simp: abs_if not_less intro: zero_less_one add_strict_increasing less_trans)
  2253 
  2254 end
  2255 
  2256 subsection \<open>Dioids\<close>
  2257 
  2258 text \<open>
  2259   Dioids are the alternative extensions of semirings, a semiring can
  2260   either be a ring or a dioid but never both.
  2261 \<close>
  2262 
  2263 class dioid = semiring_1 + canonically_ordered_monoid_add
  2264 begin
  2265 
  2266 subclass ordered_semiring
  2267   by standard (auto simp: le_iff_add distrib_left distrib_right)
  2268 
  2269 end
  2270 
  2271 
  2272 hide_fact (open) comm_mult_left_mono comm_mult_strict_left_mono distrib
  2273 
  2274 code_identifier
  2275   code_module Rings \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
  2276 
  2277 end