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