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