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