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