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