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