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