src/HOL/Rings.thy
author wenzelm
Mon Apr 25 16:09:26 2016 +0200 (2016-04-25)
changeset 63040 eb4ddd18d635
parent 62626 de25474ce728
child 63325 1086d56cde86
permissions -rw-r--r--
eliminated old 'def';
tuned comments;
     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   define b where "b = 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 lemma less_eq_add_cancel_left_greater_eq_zero [simp]:
  1353   "a \<le> a + b \<longleftrightarrow> 0 \<le> b"
  1354   using add_le_cancel_left [of a 0 b] by simp
  1355 
  1356 lemma less_eq_add_cancel_left_less_eq_zero [simp]:
  1357   "a + b \<le> a \<longleftrightarrow> b \<le> 0"
  1358   using add_le_cancel_left [of a b 0] by simp
  1359 
  1360 lemma less_eq_add_cancel_right_greater_eq_zero [simp]:
  1361   "a \<le> b + a \<longleftrightarrow> 0 \<le> b"
  1362   using add_le_cancel_right [of 0 a b] by simp
  1363 
  1364 lemma less_eq_add_cancel_right_less_eq_zero [simp]:
  1365   "b + a \<le> a \<longleftrightarrow> b \<le> 0"
  1366   using add_le_cancel_right [of b a 0] by simp
  1367 
  1368 lemma less_add_cancel_left_greater_zero [simp]:
  1369   "a < a + b \<longleftrightarrow> 0 < b"
  1370   using add_less_cancel_left [of a 0 b] by simp
  1371 
  1372 lemma less_add_cancel_left_less_zero [simp]:
  1373   "a + b < a \<longleftrightarrow> b < 0"
  1374   using add_less_cancel_left [of a b 0] by simp
  1375 
  1376 lemma less_add_cancel_right_greater_zero [simp]:
  1377   "a < b + a \<longleftrightarrow> 0 < b"
  1378   using add_less_cancel_right [of 0 a b] by simp
  1379 
  1380 lemma less_add_cancel_right_less_zero [simp]:
  1381   "b + a < a \<longleftrightarrow> b < 0"
  1382   using add_less_cancel_right [of b a 0] by simp
  1383 
  1384 end
  1385 
  1386 class linordered_semiring_1 = linordered_semiring + semiring_1
  1387 begin
  1388 
  1389 lemma convex_bound_le:
  1390   assumes "x \<le> a" "y \<le> a" "0 \<le> u" "0 \<le> v" "u + v = 1"
  1391   shows "u * x + v * y \<le> a"
  1392 proof-
  1393   from assms have "u * x + v * y \<le> u * a + v * a"
  1394     by (simp add: add_mono mult_left_mono)
  1395   thus ?thesis using assms unfolding distrib_right[symmetric] by simp
  1396 qed
  1397 
  1398 end
  1399 
  1400 class linordered_semiring_strict = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add +
  1401   assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
  1402   assumes mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c"
  1403 begin
  1404 
  1405 subclass semiring_0_cancel ..
  1406 
  1407 subclass linordered_semiring
  1408 proof
  1409   fix a b c :: 'a
  1410   assume A: "a \<le> b" "0 \<le> c"
  1411   from A show "c * a \<le> c * b"
  1412     unfolding le_less
  1413     using mult_strict_left_mono by (cases "c = 0") auto
  1414   from A show "a * c \<le> b * c"
  1415     unfolding le_less
  1416     using mult_strict_right_mono by (cases "c = 0") auto
  1417 qed
  1418 
  1419 lemma mult_left_le_imp_le:
  1420   "c * a \<le> c * b \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
  1421 by (force simp add: mult_strict_left_mono _not_less [symmetric])
  1422 
  1423 lemma mult_right_le_imp_le:
  1424   "a * c \<le> b * c \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
  1425 by (force simp add: mult_strict_right_mono not_less [symmetric])
  1426 
  1427 lemma mult_pos_pos[simp]: "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a * b"
  1428 using mult_strict_left_mono [of 0 b a] by simp
  1429 
  1430 lemma mult_pos_neg: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> a * b < 0"
  1431 using mult_strict_left_mono [of b 0 a] by simp
  1432 
  1433 lemma mult_neg_pos: "a < 0 \<Longrightarrow> 0 < b \<Longrightarrow> a * b < 0"
  1434 using mult_strict_right_mono [of a 0 b] by simp
  1435 
  1436 text \<open>Legacy - use \<open>mult_neg_pos\<close>\<close>
  1437 lemma mult_pos_neg2: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> b * a < 0"
  1438 by (drule mult_strict_right_mono [of b 0], auto)
  1439 
  1440 lemma zero_less_mult_pos:
  1441   "0 < a * b \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"
  1442 apply (cases "b\<le>0")
  1443  apply (auto simp add: le_less not_less)
  1444 apply (drule_tac mult_pos_neg [of a b])
  1445  apply (auto dest: less_not_sym)
  1446 done
  1447 
  1448 lemma zero_less_mult_pos2:
  1449   "0 < b * a \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"
  1450 apply (cases "b\<le>0")
  1451  apply (auto simp add: le_less not_less)
  1452 apply (drule_tac mult_pos_neg2 [of a b])
  1453  apply (auto dest: less_not_sym)
  1454 done
  1455 
  1456 text\<open>Strict monotonicity in both arguments\<close>
  1457 lemma mult_strict_mono:
  1458   assumes "a < b" and "c < d" and "0 < b" and "0 \<le> c"
  1459   shows "a * c < b * d"
  1460   using assms apply (cases "c=0")
  1461   apply (simp)
  1462   apply (erule mult_strict_right_mono [THEN less_trans])
  1463   apply (force simp add: le_less)
  1464   apply (erule mult_strict_left_mono, assumption)
  1465   done
  1466 
  1467 text\<open>This weaker variant has more natural premises\<close>
  1468 lemma mult_strict_mono':
  1469   assumes "a < b" and "c < d" and "0 \<le> a" and "0 \<le> c"
  1470   shows "a * c < b * d"
  1471 by (rule mult_strict_mono) (insert assms, auto)
  1472 
  1473 lemma mult_less_le_imp_less:
  1474   assumes "a < b" and "c \<le> d" and "0 \<le> a" and "0 < c"
  1475   shows "a * c < b * d"
  1476   using assms apply (subgoal_tac "a * c < b * c")
  1477   apply (erule less_le_trans)
  1478   apply (erule mult_left_mono)
  1479   apply simp
  1480   apply (erule mult_strict_right_mono)
  1481   apply assumption
  1482   done
  1483 
  1484 lemma mult_le_less_imp_less:
  1485   assumes "a \<le> b" and "c < d" and "0 < a" and "0 \<le> c"
  1486   shows "a * c < b * d"
  1487   using assms apply (subgoal_tac "a * c \<le> b * c")
  1488   apply (erule le_less_trans)
  1489   apply (erule mult_strict_left_mono)
  1490   apply simp
  1491   apply (erule mult_right_mono)
  1492   apply simp
  1493   done
  1494 
  1495 end
  1496 
  1497 class linordered_semiring_1_strict = linordered_semiring_strict + semiring_1
  1498 begin
  1499 
  1500 subclass linordered_semiring_1 ..
  1501 
  1502 lemma convex_bound_lt:
  1503   assumes "x < a" "y < a" "0 \<le> u" "0 \<le> v" "u + v = 1"
  1504   shows "u * x + v * y < a"
  1505 proof -
  1506   from assms have "u * x + v * y < u * a + v * a"
  1507     by (cases "u = 0")
  1508        (auto intro!: add_less_le_mono mult_strict_left_mono mult_left_mono)
  1509   thus ?thesis using assms unfolding distrib_right[symmetric] by simp
  1510 qed
  1511 
  1512 end
  1513 
  1514 class ordered_comm_semiring = comm_semiring_0 + ordered_ab_semigroup_add +
  1515   assumes comm_mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
  1516 begin
  1517 
  1518 subclass ordered_semiring
  1519 proof
  1520   fix a b c :: 'a
  1521   assume "a \<le> b" "0 \<le> c"
  1522   thus "c * a \<le> c * b" by (rule comm_mult_left_mono)
  1523   thus "a * c \<le> b * c" by (simp only: mult.commute)
  1524 qed
  1525 
  1526 end
  1527 
  1528 class ordered_cancel_comm_semiring = ordered_comm_semiring + cancel_comm_monoid_add
  1529 begin
  1530 
  1531 subclass comm_semiring_0_cancel ..
  1532 subclass ordered_comm_semiring ..
  1533 subclass ordered_cancel_semiring ..
  1534 
  1535 end
  1536 
  1537 class linordered_comm_semiring_strict = comm_semiring_0 + linordered_cancel_ab_semigroup_add +
  1538   assumes comm_mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
  1539 begin
  1540 
  1541 subclass linordered_semiring_strict
  1542 proof
  1543   fix a b c :: 'a
  1544   assume "a < b" "0 < c"
  1545   thus "c * a < c * b" by (rule comm_mult_strict_left_mono)
  1546   thus "a * c < b * c" by (simp only: mult.commute)
  1547 qed
  1548 
  1549 subclass ordered_cancel_comm_semiring
  1550 proof
  1551   fix a b c :: 'a
  1552   assume "a \<le> b" "0 \<le> c"
  1553   thus "c * a \<le> c * b"
  1554     unfolding le_less
  1555     using mult_strict_left_mono by (cases "c = 0") auto
  1556 qed
  1557 
  1558 end
  1559 
  1560 class ordered_ring = ring + ordered_cancel_semiring
  1561 begin
  1562 
  1563 subclass ordered_ab_group_add ..
  1564 
  1565 lemma less_add_iff1:
  1566   "a * e + c < b * e + d \<longleftrightarrow> (a - b) * e + c < d"
  1567 by (simp add: algebra_simps)
  1568 
  1569 lemma less_add_iff2:
  1570   "a * e + c < b * e + d \<longleftrightarrow> c < (b - a) * e + d"
  1571 by (simp add: algebra_simps)
  1572 
  1573 lemma le_add_iff1:
  1574   "a * e + c \<le> b * e + d \<longleftrightarrow> (a - b) * e + c \<le> d"
  1575 by (simp add: algebra_simps)
  1576 
  1577 lemma le_add_iff2:
  1578   "a * e + c \<le> b * e + d \<longleftrightarrow> c \<le> (b - a) * e + d"
  1579 by (simp add: algebra_simps)
  1580 
  1581 lemma mult_left_mono_neg:
  1582   "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> c * a \<le> c * b"
  1583   apply (drule mult_left_mono [of _ _ "- c"])
  1584   apply simp_all
  1585   done
  1586 
  1587 lemma mult_right_mono_neg:
  1588   "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> a * c \<le> b * c"
  1589   apply (drule mult_right_mono [of _ _ "- c"])
  1590   apply simp_all
  1591   done
  1592 
  1593 lemma mult_nonpos_nonpos: "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> 0 \<le> a * b"
  1594 using mult_right_mono_neg [of a 0 b] by simp
  1595 
  1596 lemma split_mult_pos_le:
  1597   "(0 \<le> a \<and> 0 \<le> b) \<or> (a \<le> 0 \<and> b \<le> 0) \<Longrightarrow> 0 \<le> a * b"
  1598 by (auto simp add: mult_nonpos_nonpos)
  1599 
  1600 end
  1601 
  1602 class linordered_ring = ring + linordered_semiring + linordered_ab_group_add + abs_if
  1603 begin
  1604 
  1605 subclass ordered_ring ..
  1606 
  1607 subclass ordered_ab_group_add_abs
  1608 proof
  1609   fix a b
  1610   show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
  1611     by (auto simp add: abs_if not_le not_less algebra_simps simp del: add.commute dest: add_neg_neg add_nonneg_nonneg)
  1612 qed (auto simp add: abs_if)
  1613 
  1614 lemma zero_le_square [simp]: "0 \<le> a * a"
  1615   using linear [of 0 a]
  1616   by (auto simp add: mult_nonpos_nonpos)
  1617 
  1618 lemma not_square_less_zero [simp]: "\<not> (a * a < 0)"
  1619   by (simp add: not_less)
  1620 
  1621 proposition abs_eq_iff: "\<bar>x\<bar> = \<bar>y\<bar> \<longleftrightarrow> x = y \<or> x = -y"
  1622   by (auto simp add: abs_if split: if_split_asm)
  1623 
  1624 lemma sum_squares_ge_zero:
  1625   "0 \<le> x * x + y * y"
  1626   by (intro add_nonneg_nonneg zero_le_square)
  1627 
  1628 lemma not_sum_squares_lt_zero:
  1629   "\<not> x * x + y * y < 0"
  1630   by (simp add: not_less sum_squares_ge_zero)
  1631 
  1632 end
  1633 
  1634 class linordered_ring_strict = ring + linordered_semiring_strict
  1635   + ordered_ab_group_add + abs_if
  1636 begin
  1637 
  1638 subclass linordered_ring ..
  1639 
  1640 lemma mult_strict_left_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> c * a < c * b"
  1641 using mult_strict_left_mono [of b a "- c"] by simp
  1642 
  1643 lemma mult_strict_right_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> a * c < b * c"
  1644 using mult_strict_right_mono [of b a "- c"] by simp
  1645 
  1646 lemma mult_neg_neg: "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> 0 < a * b"
  1647 using mult_strict_right_mono_neg [of a 0 b] by simp
  1648 
  1649 subclass ring_no_zero_divisors
  1650 proof
  1651   fix a b
  1652   assume "a \<noteq> 0" then have A: "a < 0 \<or> 0 < a" by (simp add: neq_iff)
  1653   assume "b \<noteq> 0" then have B: "b < 0 \<or> 0 < b" by (simp add: neq_iff)
  1654   have "a * b < 0 \<or> 0 < a * b"
  1655   proof (cases "a < 0")
  1656     case True note A' = this
  1657     show ?thesis proof (cases "b < 0")
  1658       case True with A'
  1659       show ?thesis by (auto dest: mult_neg_neg)
  1660     next
  1661       case False with B have "0 < b" by auto
  1662       with A' show ?thesis by (auto dest: mult_strict_right_mono)
  1663     qed
  1664   next
  1665     case False with A have A': "0 < a" by auto
  1666     show ?thesis proof (cases "b < 0")
  1667       case True with A'
  1668       show ?thesis by (auto dest: mult_strict_right_mono_neg)
  1669     next
  1670       case False with B have "0 < b" by auto
  1671       with A' show ?thesis by auto
  1672     qed
  1673   qed
  1674   then show "a * b \<noteq> 0" by (simp add: neq_iff)
  1675 qed
  1676 
  1677 lemma zero_less_mult_iff: "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0"
  1678   by (cases a 0 b 0 rule: linorder_cases[case_product linorder_cases])
  1679      (auto simp add: mult_neg_neg not_less le_less dest: zero_less_mult_pos zero_less_mult_pos2)
  1680 
  1681 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"
  1682   by (auto simp add: eq_commute [of 0] le_less not_less zero_less_mult_iff)
  1683 
  1684 lemma mult_less_0_iff:
  1685   "a * b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b"
  1686   apply (insert zero_less_mult_iff [of "-a" b])
  1687   apply force
  1688   done
  1689 
  1690 lemma mult_le_0_iff:
  1691   "a * b \<le> 0 \<longleftrightarrow> 0 \<le> a \<and> b \<le> 0 \<or> a \<le> 0 \<and> 0 \<le> b"
  1692   apply (insert zero_le_mult_iff [of "-a" b])
  1693   apply force
  1694   done
  1695 
  1696 text\<open>Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"},
  1697    also with the relations \<open>\<le>\<close> and equality.\<close>
  1698 
  1699 text\<open>These ``disjunction'' versions produce two cases when the comparison is
  1700  an assumption, but effectively four when the comparison is a goal.\<close>
  1701 
  1702 lemma mult_less_cancel_right_disj:
  1703   "a * c < b * c \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"
  1704   apply (cases "c = 0")
  1705   apply (auto simp add: neq_iff mult_strict_right_mono
  1706                       mult_strict_right_mono_neg)
  1707   apply (auto simp add: not_less
  1708                       not_le [symmetric, of "a*c"]
  1709                       not_le [symmetric, of a])
  1710   apply (erule_tac [!] notE)
  1711   apply (auto simp add: less_imp_le mult_right_mono
  1712                       mult_right_mono_neg)
  1713   done
  1714 
  1715 lemma mult_less_cancel_left_disj:
  1716   "c * a < c * b \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"
  1717   apply (cases "c = 0")
  1718   apply (auto simp add: neq_iff mult_strict_left_mono
  1719                       mult_strict_left_mono_neg)
  1720   apply (auto simp add: not_less
  1721                       not_le [symmetric, of "c*a"]
  1722                       not_le [symmetric, of a])
  1723   apply (erule_tac [!] notE)
  1724   apply (auto simp add: less_imp_le mult_left_mono
  1725                       mult_left_mono_neg)
  1726   done
  1727 
  1728 text\<open>The ``conjunction of implication'' lemmas produce two cases when the
  1729 comparison is a goal, but give four when the comparison is an assumption.\<close>
  1730 
  1731 lemma mult_less_cancel_right:
  1732   "a * c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)"
  1733   using mult_less_cancel_right_disj [of a c b] by auto
  1734 
  1735 lemma mult_less_cancel_left:
  1736   "c * a < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)"
  1737   using mult_less_cancel_left_disj [of c a b] by auto
  1738 
  1739 lemma mult_le_cancel_right:
  1740    "a * c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
  1741 by (simp add: not_less [symmetric] mult_less_cancel_right_disj)
  1742 
  1743 lemma mult_le_cancel_left:
  1744   "c * a \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
  1745 by (simp add: not_less [symmetric] mult_less_cancel_left_disj)
  1746 
  1747 lemma mult_le_cancel_left_pos:
  1748   "0 < c \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> a \<le> b"
  1749 by (auto simp: mult_le_cancel_left)
  1750 
  1751 lemma mult_le_cancel_left_neg:
  1752   "c < 0 \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> b \<le> a"
  1753 by (auto simp: mult_le_cancel_left)
  1754 
  1755 lemma mult_less_cancel_left_pos:
  1756   "0 < c \<Longrightarrow> c * a < c * b \<longleftrightarrow> a < b"
  1757 by (auto simp: mult_less_cancel_left)
  1758 
  1759 lemma mult_less_cancel_left_neg:
  1760   "c < 0 \<Longrightarrow> c * a < c * b \<longleftrightarrow> b < a"
  1761 by (auto simp: mult_less_cancel_left)
  1762 
  1763 end
  1764 
  1765 lemmas mult_sign_intros =
  1766   mult_nonneg_nonneg mult_nonneg_nonpos
  1767   mult_nonpos_nonneg mult_nonpos_nonpos
  1768   mult_pos_pos mult_pos_neg
  1769   mult_neg_pos mult_neg_neg
  1770 
  1771 class ordered_comm_ring = comm_ring + ordered_comm_semiring
  1772 begin
  1773 
  1774 subclass ordered_ring ..
  1775 subclass ordered_cancel_comm_semiring ..
  1776 
  1777 end
  1778 
  1779 class zero_less_one = order + zero + one +
  1780   assumes zero_less_one [simp]: "0 < 1"
  1781 
  1782 class linordered_nonzero_semiring = ordered_comm_semiring + monoid_mult + linorder + zero_less_one
  1783 begin
  1784 
  1785 subclass zero_neq_one
  1786   proof qed (insert zero_less_one, blast)
  1787 
  1788 subclass comm_semiring_1
  1789   proof qed (rule mult_1_left)
  1790 
  1791 lemma zero_le_one [simp]: "0 \<le> 1"
  1792 by (rule zero_less_one [THEN less_imp_le])
  1793 
  1794 lemma not_one_le_zero [simp]: "\<not> 1 \<le> 0"
  1795 by (simp add: not_le)
  1796 
  1797 lemma not_one_less_zero [simp]: "\<not> 1 < 0"
  1798 by (simp add: not_less)
  1799 
  1800 lemma mult_left_le: "c \<le> 1 \<Longrightarrow> 0 \<le> a \<Longrightarrow> a * c \<le> a"
  1801   using mult_left_mono[of c 1 a] by simp
  1802 
  1803 lemma mult_le_one: "a \<le> 1 \<Longrightarrow> 0 \<le> b \<Longrightarrow> b \<le> 1 \<Longrightarrow> a * b \<le> 1"
  1804   using mult_mono[of a 1 b 1] by simp
  1805 
  1806 lemma zero_less_two: "0 < 1 + 1"
  1807   using add_pos_pos[OF zero_less_one zero_less_one] .
  1808 
  1809 end
  1810 
  1811 class linordered_semidom = semidom + linordered_comm_semiring_strict + zero_less_one +
  1812   assumes le_add_diff_inverse2 [simp]: "b \<le> a \<Longrightarrow> a - b + b = a"
  1813 begin
  1814 
  1815 subclass linordered_nonzero_semiring
  1816   proof qed
  1817 
  1818 text \<open>Addition is the inverse of subtraction.\<close>
  1819 
  1820 lemma le_add_diff_inverse [simp]: "b \<le> a \<Longrightarrow> b + (a - b) = a"
  1821   by (frule le_add_diff_inverse2) (simp add: add.commute)
  1822 
  1823 lemma add_diff_inverse: "\<not> a < b \<Longrightarrow> b + (a - b) = a"
  1824   by simp
  1825 
  1826 lemma add_le_imp_le_diff:
  1827   shows "i + k \<le> n \<Longrightarrow> i \<le> n - k"
  1828   apply (subst add_le_cancel_right [where c=k, symmetric])
  1829   apply (frule le_add_diff_inverse2)
  1830   apply (simp only: add.assoc [symmetric])
  1831   using add_implies_diff by fastforce
  1832 
  1833 lemma add_le_add_imp_diff_le:
  1834   assumes a1: "i + k \<le> n"
  1835       and a2: "n \<le> j + k"
  1836   shows "\<lbrakk>i + k \<le> n; n \<le> j + k\<rbrakk> \<Longrightarrow> n - k \<le> j"
  1837 proof -
  1838   have "n - (i + k) + (i + k) = n"
  1839     using a1 by simp
  1840   moreover have "n - k = n - k - i + i"
  1841     using a1 by (simp add: add_le_imp_le_diff)
  1842   ultimately show ?thesis
  1843     using a2
  1844     apply (simp add: add.assoc [symmetric])
  1845     apply (rule add_le_imp_le_diff [of _ k "j+k", simplified add_diff_cancel_right'])
  1846     by (simp add: add.commute diff_diff_add)
  1847 qed
  1848 
  1849 lemma less_1_mult:
  1850   "1 < m \<Longrightarrow> 1 < n \<Longrightarrow> 1 < m * n"
  1851   using mult_strict_mono [of 1 m 1 n] by (simp add: less_trans [OF zero_less_one])
  1852 
  1853 end
  1854 
  1855 class linordered_idom =
  1856   comm_ring_1 + linordered_comm_semiring_strict + ordered_ab_group_add + abs_if + sgn_if
  1857 begin
  1858 
  1859 subclass linordered_semiring_1_strict ..
  1860 subclass linordered_ring_strict ..
  1861 subclass ordered_comm_ring ..
  1862 subclass idom ..
  1863 
  1864 subclass linordered_semidom
  1865 proof
  1866   have "0 \<le> 1 * 1" by (rule zero_le_square)
  1867   thus "0 < 1" by (simp add: le_less)
  1868   show "\<And>b a. b \<le> a \<Longrightarrow> a - b + b = a"
  1869     by simp
  1870 qed
  1871 
  1872 lemma linorder_neqE_linordered_idom:
  1873   assumes "x \<noteq> y" obtains "x < y" | "y < x"
  1874   using assms by (rule neqE)
  1875 
  1876 text \<open>These cancellation simprules also produce two cases when the comparison is a goal.\<close>
  1877 
  1878 lemma mult_le_cancel_right1:
  1879   "c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)"
  1880 by (insert mult_le_cancel_right [of 1 c b], simp)
  1881 
  1882 lemma mult_le_cancel_right2:
  1883   "a * c \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)"
  1884 by (insert mult_le_cancel_right [of a c 1], simp)
  1885 
  1886 lemma mult_le_cancel_left1:
  1887   "c \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)"
  1888 by (insert mult_le_cancel_left [of c 1 b], simp)
  1889 
  1890 lemma mult_le_cancel_left2:
  1891   "c * a \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)"
  1892 by (insert mult_le_cancel_left [of c a 1], simp)
  1893 
  1894 lemma mult_less_cancel_right1:
  1895   "c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)"
  1896 by (insert mult_less_cancel_right [of 1 c b], simp)
  1897 
  1898 lemma mult_less_cancel_right2:
  1899   "a * c < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"
  1900 by (insert mult_less_cancel_right [of a c 1], simp)
  1901 
  1902 lemma mult_less_cancel_left1:
  1903   "c < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)"
  1904 by (insert mult_less_cancel_left [of c 1 b], simp)
  1905 
  1906 lemma mult_less_cancel_left2:
  1907   "c * a < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"
  1908 by (insert mult_less_cancel_left [of c a 1], simp)
  1909 
  1910 lemma sgn_sgn [simp]:
  1911   "sgn (sgn a) = sgn a"
  1912 unfolding sgn_if by simp
  1913 
  1914 lemma sgn_0_0:
  1915   "sgn a = 0 \<longleftrightarrow> a = 0"
  1916 unfolding sgn_if by simp
  1917 
  1918 lemma sgn_1_pos:
  1919   "sgn a = 1 \<longleftrightarrow> a > 0"
  1920 unfolding sgn_if by simp
  1921 
  1922 lemma sgn_1_neg:
  1923   "sgn a = - 1 \<longleftrightarrow> a < 0"
  1924 unfolding sgn_if by auto
  1925 
  1926 lemma sgn_pos [simp]:
  1927   "0 < a \<Longrightarrow> sgn a = 1"
  1928 unfolding sgn_1_pos .
  1929 
  1930 lemma sgn_neg [simp]:
  1931   "a < 0 \<Longrightarrow> sgn a = - 1"
  1932 unfolding sgn_1_neg .
  1933 
  1934 lemma sgn_times:
  1935   "sgn (a * b) = sgn a * sgn b"
  1936 by (auto simp add: sgn_if zero_less_mult_iff)
  1937 
  1938 lemma abs_sgn: "\<bar>k\<bar> = k * sgn k"
  1939 unfolding sgn_if abs_if by auto
  1940 
  1941 lemma sgn_greater [simp]:
  1942   "0 < sgn a \<longleftrightarrow> 0 < a"
  1943   unfolding sgn_if by auto
  1944 
  1945 lemma sgn_less [simp]:
  1946   "sgn a < 0 \<longleftrightarrow> a < 0"
  1947   unfolding sgn_if by auto
  1948 
  1949 lemma abs_sgn_eq:
  1950   "\<bar>sgn a\<bar> = (if a = 0 then 0 else 1)"
  1951   by (simp add: sgn_if)
  1952 
  1953 lemma abs_dvd_iff [simp]: "\<bar>m\<bar> dvd k \<longleftrightarrow> m dvd k"
  1954   by (simp add: abs_if)
  1955 
  1956 lemma dvd_abs_iff [simp]: "m dvd \<bar>k\<bar> \<longleftrightarrow> m dvd k"
  1957   by (simp add: abs_if)
  1958 
  1959 lemma dvd_if_abs_eq:
  1960   "\<bar>l\<bar> = \<bar>k\<bar> \<Longrightarrow> l dvd k"
  1961 by(subst abs_dvd_iff[symmetric]) simp
  1962 
  1963 text \<open>The following lemmas can be proven in more general structures, but
  1964 are dangerous as simp rules in absence of @{thm neg_equal_zero},
  1965 @{thm neg_less_pos}, @{thm neg_less_eq_nonneg}.\<close>
  1966 
  1967 lemma equation_minus_iff_1 [simp, no_atp]:
  1968   "1 = - a \<longleftrightarrow> a = - 1"
  1969   by (fact equation_minus_iff)
  1970 
  1971 lemma minus_equation_iff_1 [simp, no_atp]:
  1972   "- a = 1 \<longleftrightarrow> a = - 1"
  1973   by (subst minus_equation_iff, auto)
  1974 
  1975 lemma le_minus_iff_1 [simp, no_atp]:
  1976   "1 \<le> - b \<longleftrightarrow> b \<le> - 1"
  1977   by (fact le_minus_iff)
  1978 
  1979 lemma minus_le_iff_1 [simp, no_atp]:
  1980   "- a \<le> 1 \<longleftrightarrow> - 1 \<le> a"
  1981   by (fact minus_le_iff)
  1982 
  1983 lemma less_minus_iff_1 [simp, no_atp]:
  1984   "1 < - b \<longleftrightarrow> b < - 1"
  1985   by (fact less_minus_iff)
  1986 
  1987 lemma minus_less_iff_1 [simp, no_atp]:
  1988   "- a < 1 \<longleftrightarrow> - 1 < a"
  1989   by (fact minus_less_iff)
  1990 
  1991 end
  1992 
  1993 text \<open>Simprules for comparisons where common factors can be cancelled.\<close>
  1994 
  1995 lemmas mult_compare_simps =
  1996     mult_le_cancel_right mult_le_cancel_left
  1997     mult_le_cancel_right1 mult_le_cancel_right2
  1998     mult_le_cancel_left1 mult_le_cancel_left2
  1999     mult_less_cancel_right mult_less_cancel_left
  2000     mult_less_cancel_right1 mult_less_cancel_right2
  2001     mult_less_cancel_left1 mult_less_cancel_left2
  2002     mult_cancel_right mult_cancel_left
  2003     mult_cancel_right1 mult_cancel_right2
  2004     mult_cancel_left1 mult_cancel_left2
  2005 
  2006 text \<open>Reasoning about inequalities with division\<close>
  2007 
  2008 context linordered_semidom
  2009 begin
  2010 
  2011 lemma less_add_one: "a < a + 1"
  2012 proof -
  2013   have "a + 0 < a + 1"
  2014     by (blast intro: zero_less_one add_strict_left_mono)
  2015   thus ?thesis by simp
  2016 qed
  2017 
  2018 end
  2019 
  2020 context linordered_idom
  2021 begin
  2022 
  2023 lemma mult_right_le_one_le:
  2024   "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> x * y \<le> x"
  2025   by (rule mult_left_le)
  2026 
  2027 lemma mult_left_le_one_le:
  2028   "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> y * x \<le> x"
  2029   by (auto simp add: mult_le_cancel_right2)
  2030 
  2031 end
  2032 
  2033 text \<open>Absolute Value\<close>
  2034 
  2035 context linordered_idom
  2036 begin
  2037 
  2038 lemma mult_sgn_abs:
  2039   "sgn x * \<bar>x\<bar> = x"
  2040   unfolding abs_if sgn_if by auto
  2041 
  2042 lemma abs_one [simp]:
  2043   "\<bar>1\<bar> = 1"
  2044   by (simp add: abs_if)
  2045 
  2046 end
  2047 
  2048 class ordered_ring_abs = ordered_ring + ordered_ab_group_add_abs +
  2049   assumes abs_eq_mult:
  2050     "(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>"
  2051 
  2052 context linordered_idom
  2053 begin
  2054 
  2055 subclass ordered_ring_abs proof
  2056 qed (auto simp add: abs_if not_less mult_less_0_iff)
  2057 
  2058 lemma abs_mult:
  2059   "\<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>"
  2060   by (rule abs_eq_mult) auto
  2061 
  2062 lemma abs_mult_self [simp]:
  2063   "\<bar>a\<bar> * \<bar>a\<bar> = a * a"
  2064   by (simp add: abs_if)
  2065 
  2066 lemma abs_mult_less:
  2067   "\<bar>a\<bar> < c \<Longrightarrow> \<bar>b\<bar> < d \<Longrightarrow> \<bar>a\<bar> * \<bar>b\<bar> < c * d"
  2068 proof -
  2069   assume ac: "\<bar>a\<bar> < c"
  2070   hence cpos: "0<c" by (blast intro: le_less_trans abs_ge_zero)
  2071   assume "\<bar>b\<bar> < d"
  2072   thus ?thesis by (simp add: ac cpos mult_strict_mono)
  2073 qed
  2074 
  2075 lemma abs_less_iff:
  2076   "\<bar>a\<bar> < b \<longleftrightarrow> a < b \<and> - a < b"
  2077   by (simp add: less_le abs_le_iff) (auto simp add: abs_if)
  2078 
  2079 lemma abs_mult_pos:
  2080   "0 \<le> x \<Longrightarrow> \<bar>y\<bar> * x = \<bar>y * x\<bar>"
  2081   by (simp add: abs_mult)
  2082 
  2083 lemma abs_diff_less_iff:
  2084   "\<bar>x - a\<bar> < r \<longleftrightarrow> a - r < x \<and> x < a + r"
  2085   by (auto simp add: diff_less_eq ac_simps abs_less_iff)
  2086 
  2087 lemma abs_diff_le_iff:
  2088    "\<bar>x - a\<bar> \<le> r \<longleftrightarrow> a - r \<le> x \<and> x \<le> a + r"
  2089   by (auto simp add: diff_le_eq ac_simps abs_le_iff)
  2090 
  2091 lemma abs_add_one_gt_zero: "0 < 1 + \<bar>x\<bar>"
  2092   by (force simp: abs_if not_less intro: zero_less_one add_strict_increasing less_trans)
  2093 
  2094 end
  2095 
  2096 subsection \<open>Dioids\<close>
  2097 
  2098 text \<open>Dioids are the alternative extensions of semirings, a semiring can either be a ring or a dioid
  2099 but never both.\<close>
  2100 
  2101 class dioid = semiring_1 + canonically_ordered_monoid_add
  2102 begin
  2103 
  2104 subclass ordered_semiring
  2105   proof qed (auto simp: le_iff_add distrib_left distrib_right)
  2106 
  2107 end
  2108 
  2109 
  2110 hide_fact (open) comm_mult_left_mono comm_mult_strict_left_mono distrib
  2111 
  2112 code_identifier
  2113   code_module Rings \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
  2114 
  2115 end