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