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