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