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