src/HOL/Rings.thy
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (19 months ago)
changeset 67003 49850a679c2c
parent 66937 a1a4a5e2933a
child 67051 e7e54a0b9197
permissions -rw-r--r--
more robust sorted_entries;
     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 begin
   122 
   123 lemma (in semiring_1) of_bool_conj:
   124   "of_bool (P \<and> Q) = of_bool P * of_bool Q"
   125   by auto
   126 
   127 end
   128 
   129 text \<open>Abstract divisibility\<close>
   130 
   131 class dvd = times
   132 begin
   133 
   134 definition dvd :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "dvd" 50)
   135   where "b dvd a \<longleftrightarrow> (\<exists>k. a = b * k)"
   136 
   137 lemma dvdI [intro?]: "a = b * k \<Longrightarrow> b dvd a"
   138   unfolding dvd_def ..
   139 
   140 lemma dvdE [elim?]: "b dvd a \<Longrightarrow> (\<And>k. a = b * k \<Longrightarrow> P) \<Longrightarrow> P"
   141   unfolding dvd_def by blast
   142 
   143 end
   144 
   145 context comm_monoid_mult
   146 begin
   147 
   148 subclass dvd .
   149 
   150 lemma dvd_refl [simp]: "a dvd a"
   151 proof
   152   show "a = a * 1" by simp
   153 qed
   154 
   155 lemma dvd_trans [trans]:
   156   assumes "a dvd b" and "b dvd c"
   157   shows "a dvd c"
   158 proof -
   159   from assms obtain v where "b = a * v"
   160     by (auto elim!: dvdE)
   161   moreover from assms obtain w where "c = b * w"
   162     by (auto elim!: dvdE)
   163   ultimately have "c = a * (v * w)"
   164     by (simp add: mult.assoc)
   165   then show ?thesis ..
   166 qed
   167 
   168 lemma subset_divisors_dvd: "{c. c dvd a} \<subseteq> {c. c dvd b} \<longleftrightarrow> a dvd b"
   169   by (auto simp add: subset_iff intro: dvd_trans)
   170 
   171 lemma strict_subset_divisors_dvd: "{c. c dvd a} \<subset> {c. c dvd b} \<longleftrightarrow> a dvd b \<and> \<not> b dvd a"
   172   by (auto simp add: subset_iff intro: dvd_trans)
   173 
   174 lemma one_dvd [simp]: "1 dvd a"
   175   by (auto intro!: dvdI)
   176 
   177 lemma dvd_mult [simp]: "a dvd c \<Longrightarrow> a dvd (b * c)"
   178   by (auto intro!: mult.left_commute dvdI elim!: dvdE)
   179 
   180 lemma dvd_mult2 [simp]: "a dvd b \<Longrightarrow> a dvd (b * c)"
   181   using dvd_mult [of a b c] by (simp add: ac_simps)
   182 
   183 lemma dvd_triv_right [simp]: "a dvd b * a"
   184   by (rule dvd_mult) (rule dvd_refl)
   185 
   186 lemma dvd_triv_left [simp]: "a dvd a * b"
   187   by (rule dvd_mult2) (rule dvd_refl)
   188 
   189 lemma mult_dvd_mono:
   190   assumes "a dvd b"
   191     and "c dvd d"
   192   shows "a * c dvd b * d"
   193 proof -
   194   from \<open>a dvd b\<close> obtain b' where "b = a * b'" ..
   195   moreover from \<open>c dvd d\<close> obtain d' where "d = c * d'" ..
   196   ultimately have "b * d = (a * c) * (b' * d')"
   197     by (simp add: ac_simps)
   198   then show ?thesis ..
   199 qed
   200 
   201 lemma dvd_mult_left: "a * b dvd c \<Longrightarrow> a dvd c"
   202   by (simp add: dvd_def mult.assoc) blast
   203 
   204 lemma dvd_mult_right: "a * b dvd c \<Longrightarrow> b dvd c"
   205   using dvd_mult_left [of b a c] by (simp add: ac_simps)
   206 
   207 end
   208 
   209 class comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult
   210 begin
   211 
   212 subclass semiring_1 ..
   213 
   214 lemma dvd_0_left_iff [simp]: "0 dvd a \<longleftrightarrow> a = 0"
   215   by (auto intro: dvd_refl elim!: dvdE)
   216 
   217 lemma dvd_0_right [iff]: "a dvd 0"
   218 proof
   219   show "0 = a * 0" by simp
   220 qed
   221 
   222 lemma dvd_0_left: "0 dvd a \<Longrightarrow> a = 0"
   223   by simp
   224 
   225 lemma dvd_add [simp]:
   226   assumes "a dvd b" and "a dvd c"
   227   shows "a dvd (b + c)"
   228 proof -
   229   from \<open>a dvd b\<close> obtain b' where "b = a * b'" ..
   230   moreover from \<open>a dvd c\<close> obtain c' where "c = a * c'" ..
   231   ultimately have "b + c = a * (b' + c')"
   232     by (simp add: distrib_left)
   233   then show ?thesis ..
   234 qed
   235 
   236 end
   237 
   238 class semiring_1_cancel = semiring + cancel_comm_monoid_add
   239   + zero_neq_one + monoid_mult
   240 begin
   241 
   242 subclass semiring_0_cancel ..
   243 
   244 subclass semiring_1 ..
   245 
   246 end
   247 
   248 class comm_semiring_1_cancel =
   249   comm_semiring + cancel_comm_monoid_add + zero_neq_one + comm_monoid_mult +
   250   assumes right_diff_distrib' [algebra_simps]: "a * (b - c) = a * b - a * c"
   251 begin
   252 
   253 subclass semiring_1_cancel ..
   254 subclass comm_semiring_0_cancel ..
   255 subclass comm_semiring_1 ..
   256 
   257 lemma left_diff_distrib' [algebra_simps]: "(b - c) * a = b * a - c * a"
   258   by (simp add: algebra_simps)
   259 
   260 lemma dvd_add_times_triv_left_iff [simp]: "a dvd c * a + b \<longleftrightarrow> a dvd b"
   261 proof -
   262   have "a dvd a * c + b \<longleftrightarrow> a dvd b" (is "?P \<longleftrightarrow> ?Q")
   263   proof
   264     assume ?Q
   265     then show ?P by simp
   266   next
   267     assume ?P
   268     then obtain d where "a * c + b = a * d" ..
   269     then have "a * c + b - a * c = a * d - a * c" by simp
   270     then have "b = a * d - a * c" by simp
   271     then have "b = a * (d - c)" by (simp add: algebra_simps)
   272     then show ?Q ..
   273   qed
   274   then show "a dvd c * a + b \<longleftrightarrow> a dvd b" by (simp add: ac_simps)
   275 qed
   276 
   277 lemma dvd_add_times_triv_right_iff [simp]: "a dvd b + c * a \<longleftrightarrow> a dvd b"
   278   using dvd_add_times_triv_left_iff [of a c b] by (simp add: ac_simps)
   279 
   280 lemma dvd_add_triv_left_iff [simp]: "a dvd a + b \<longleftrightarrow> a dvd b"
   281   using dvd_add_times_triv_left_iff [of a 1 b] by simp
   282 
   283 lemma dvd_add_triv_right_iff [simp]: "a dvd b + a \<longleftrightarrow> a dvd b"
   284   using dvd_add_times_triv_right_iff [of a b 1] by simp
   285 
   286 lemma dvd_add_right_iff:
   287   assumes "a dvd b"
   288   shows "a dvd b + c \<longleftrightarrow> a dvd c" (is "?P \<longleftrightarrow> ?Q")
   289 proof
   290   assume ?P
   291   then obtain d where "b + c = a * d" ..
   292   moreover from \<open>a dvd b\<close> obtain e where "b = a * e" ..
   293   ultimately have "a * e + c = a * d" by simp
   294   then have "a * e + c - a * e = a * d - a * e" by simp
   295   then have "c = a * d - a * e" by simp
   296   then have "c = a * (d - e)" by (simp add: algebra_simps)
   297   then show ?Q ..
   298 next
   299   assume ?Q
   300   with assms show ?P by simp
   301 qed
   302 
   303 lemma dvd_add_left_iff: "a dvd c \<Longrightarrow> a dvd b + c \<longleftrightarrow> a dvd b"
   304   using dvd_add_right_iff [of a c b] by (simp add: ac_simps)
   305 
   306 end
   307 
   308 class ring = semiring + ab_group_add
   309 begin
   310 
   311 subclass semiring_0_cancel ..
   312 
   313 text \<open>Distribution rules\<close>
   314 
   315 lemma minus_mult_left: "- (a * b) = - a * b"
   316   by (rule minus_unique) (simp add: distrib_right [symmetric])
   317 
   318 lemma minus_mult_right: "- (a * b) = a * - b"
   319   by (rule minus_unique) (simp add: distrib_left [symmetric])
   320 
   321 text \<open>Extract signs from products\<close>
   322 lemmas mult_minus_left [simp] = minus_mult_left [symmetric]
   323 lemmas mult_minus_right [simp] = minus_mult_right [symmetric]
   324 
   325 lemma minus_mult_minus [simp]: "- a * - b = a * b"
   326   by simp
   327 
   328 lemma minus_mult_commute: "- a * b = a * - b"
   329   by simp
   330 
   331 lemma right_diff_distrib [algebra_simps]: "a * (b - c) = a * b - a * c"
   332   using distrib_left [of a b "-c "] by simp
   333 
   334 lemma left_diff_distrib [algebra_simps]: "(a - b) * c = a * c - b * c"
   335   using distrib_right [of a "- b" c] by simp
   336 
   337 lemmas ring_distribs = distrib_left distrib_right left_diff_distrib right_diff_distrib
   338 
   339 lemma eq_add_iff1: "a * e + c = b * e + d \<longleftrightarrow> (a - b) * e + c = d"
   340   by (simp add: algebra_simps)
   341 
   342 lemma eq_add_iff2: "a * e + c = b * e + d \<longleftrightarrow> c = (b - a) * e + d"
   343   by (simp add: algebra_simps)
   344 
   345 end
   346 
   347 lemmas ring_distribs = distrib_left distrib_right left_diff_distrib right_diff_distrib
   348 
   349 class comm_ring = comm_semiring + ab_group_add
   350 begin
   351 
   352 subclass ring ..
   353 subclass comm_semiring_0_cancel ..
   354 
   355 lemma square_diff_square_factored: "x * x - y * y = (x + y) * (x - y)"
   356   by (simp add: algebra_simps)
   357 
   358 end
   359 
   360 class ring_1 = ring + zero_neq_one + monoid_mult
   361 begin
   362 
   363 subclass semiring_1_cancel ..
   364 
   365 lemma square_diff_one_factored: "x * x - 1 = (x + 1) * (x - 1)"
   366   by (simp add: algebra_simps)
   367 
   368 end
   369 
   370 class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult
   371 begin
   372 
   373 subclass ring_1 ..
   374 subclass comm_semiring_1_cancel
   375   by unfold_locales (simp add: algebra_simps)
   376 
   377 lemma dvd_minus_iff [simp]: "x dvd - y \<longleftrightarrow> x dvd y"
   378 proof
   379   assume "x dvd - y"
   380   then have "x dvd - 1 * - y" by (rule dvd_mult)
   381   then show "x dvd y" by simp
   382 next
   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 qed
   387 
   388 lemma minus_dvd_iff [simp]: "- x dvd y \<longleftrightarrow> x dvd y"
   389 proof
   390   assume "- x dvd y"
   391   then obtain k where "y = - x * k" ..
   392   then have "y = x * - k" by simp
   393   then show "x dvd y" ..
   394 next
   395   assume "x dvd y"
   396   then obtain k where "y = x * k" ..
   397   then have "y = - x * - k" by simp
   398   then show "- x dvd y" ..
   399 qed
   400 
   401 lemma dvd_diff [simp]: "x dvd y \<Longrightarrow> x dvd z \<Longrightarrow> x dvd (y - z)"
   402   using dvd_add [of x y "- z"] by simp
   403 
   404 end
   405 
   406 class semiring_no_zero_divisors = semiring_0 +
   407   assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
   408 begin
   409 
   410 lemma divisors_zero:
   411   assumes "a * b = 0"
   412   shows "a = 0 \<or> b = 0"
   413 proof (rule classical)
   414   assume "\<not> ?thesis"
   415   then have "a \<noteq> 0" and "b \<noteq> 0" by auto
   416   with no_zero_divisors have "a * b \<noteq> 0" by blast
   417   with assms show ?thesis by simp
   418 qed
   419 
   420 lemma mult_eq_0_iff [simp]: "a * b = 0 \<longleftrightarrow> a = 0 \<or> b = 0"
   421 proof (cases "a = 0 \<or> b = 0")
   422   case False
   423   then have "a \<noteq> 0" and "b \<noteq> 0" by auto
   424     then show ?thesis using no_zero_divisors by simp
   425 next
   426   case True
   427   then show ?thesis by auto
   428 qed
   429 
   430 end
   431 
   432 class semiring_1_no_zero_divisors = semiring_1 + semiring_no_zero_divisors
   433 
   434 class semiring_no_zero_divisors_cancel = semiring_no_zero_divisors +
   435   assumes mult_cancel_right [simp]: "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b"
   436     and mult_cancel_left [simp]: "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b"
   437 begin
   438 
   439 lemma mult_left_cancel: "c \<noteq> 0 \<Longrightarrow> c * a = c * b \<longleftrightarrow> a = b"
   440   by simp
   441 
   442 lemma mult_right_cancel: "c \<noteq> 0 \<Longrightarrow> a * c = b * c \<longleftrightarrow> a = b"
   443   by simp
   444 
   445 end
   446 
   447 class ring_no_zero_divisors = ring + semiring_no_zero_divisors
   448 begin
   449 
   450 subclass semiring_no_zero_divisors_cancel
   451 proof
   452   fix a b c
   453   have "a * c = b * c \<longleftrightarrow> (a - b) * c = 0"
   454     by (simp add: algebra_simps)
   455   also have "\<dots> \<longleftrightarrow> c = 0 \<or> a = b"
   456     by auto
   457   finally show "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b" .
   458   have "c * a = c * b \<longleftrightarrow> c * (a - b) = 0"
   459     by (simp add: algebra_simps)
   460   also have "\<dots> \<longleftrightarrow> c = 0 \<or> a = b"
   461     by auto
   462   finally show "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b" .
   463 qed
   464 
   465 end
   466 
   467 class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors
   468 begin
   469 
   470 subclass semiring_1_no_zero_divisors ..
   471 
   472 lemma square_eq_1_iff: "x * x = 1 \<longleftrightarrow> x = 1 \<or> x = - 1"
   473 proof -
   474   have "(x - 1) * (x + 1) = x * x - 1"
   475     by (simp add: algebra_simps)
   476   then have "x * x = 1 \<longleftrightarrow> (x - 1) * (x + 1) = 0"
   477     by simp
   478   then show ?thesis
   479     by (simp add: eq_neg_iff_add_eq_0)
   480 qed
   481 
   482 lemma mult_cancel_right1 [simp]: "c = b * c \<longleftrightarrow> c = 0 \<or> b = 1"
   483   using mult_cancel_right [of 1 c b] by auto
   484 
   485 lemma mult_cancel_right2 [simp]: "a * c = c \<longleftrightarrow> c = 0 \<or> a = 1"
   486   using mult_cancel_right [of a c 1] by simp
   487 
   488 lemma mult_cancel_left1 [simp]: "c = c * b \<longleftrightarrow> c = 0 \<or> b = 1"
   489   using mult_cancel_left [of c 1 b] by force
   490 
   491 lemma mult_cancel_left2 [simp]: "c * a = c \<longleftrightarrow> c = 0 \<or> a = 1"
   492   using mult_cancel_left [of c a 1] by simp
   493 
   494 end
   495 
   496 class semidom = comm_semiring_1_cancel + semiring_no_zero_divisors
   497 begin
   498 
   499 subclass semiring_1_no_zero_divisors ..
   500 
   501 end
   502 
   503 class idom = comm_ring_1 + semiring_no_zero_divisors
   504 begin
   505 
   506 subclass semidom ..
   507 
   508 subclass ring_1_no_zero_divisors ..
   509 
   510 lemma dvd_mult_cancel_right [simp]: "a * c dvd b * c \<longleftrightarrow> c = 0 \<or> a dvd b"
   511 proof -
   512   have "a * c dvd b * c \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)"
   513     unfolding dvd_def by (simp add: ac_simps)
   514   also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b"
   515     unfolding dvd_def by simp
   516   finally show ?thesis .
   517 qed
   518 
   519 lemma dvd_mult_cancel_left [simp]: "c * a dvd c * b \<longleftrightarrow> c = 0 \<or> a dvd b"
   520 proof -
   521   have "c * a dvd c * b \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)"
   522     unfolding dvd_def by (simp add: ac_simps)
   523   also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b"
   524     unfolding dvd_def by simp
   525   finally show ?thesis .
   526 qed
   527 
   528 lemma square_eq_iff: "a * a = b * b \<longleftrightarrow> a = b \<or> a = - b"
   529 proof
   530   assume "a * a = b * b"
   531   then have "(a - b) * (a + b) = 0"
   532     by (simp add: algebra_simps)
   533   then show "a = b \<or> a = - b"
   534     by (simp add: eq_neg_iff_add_eq_0)
   535 next
   536   assume "a = b \<or> a = - b"
   537   then show "a * a = b * b" by auto
   538 qed
   539 
   540 end
   541 
   542 class idom_abs_sgn = idom + abs + sgn +
   543   assumes sgn_mult_abs: "sgn a * \<bar>a\<bar> = a"
   544     and sgn_sgn [simp]: "sgn (sgn a) = sgn a"
   545     and abs_abs [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>"
   546     and abs_0 [simp]: "\<bar>0\<bar> = 0"
   547     and sgn_0 [simp]: "sgn 0 = 0"
   548     and sgn_1 [simp]: "sgn 1 = 1"
   549     and sgn_minus_1: "sgn (- 1) = - 1"
   550     and sgn_mult: "sgn (a * b) = sgn a * sgn b"
   551 begin
   552 
   553 lemma sgn_eq_0_iff:
   554   "sgn a = 0 \<longleftrightarrow> a = 0"
   555 proof -
   556   { assume "sgn a = 0"
   557     then have "sgn a * \<bar>a\<bar> = 0"
   558       by simp
   559     then have "a = 0"
   560       by (simp add: sgn_mult_abs)
   561   } then show ?thesis
   562     by auto
   563 qed
   564 
   565 lemma abs_eq_0_iff:
   566   "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0"
   567 proof -
   568   { assume "\<bar>a\<bar> = 0"
   569     then have "sgn a * \<bar>a\<bar> = 0"
   570       by simp
   571     then have "a = 0"
   572       by (simp add: sgn_mult_abs)
   573   } then show ?thesis
   574     by auto
   575 qed
   576 
   577 lemma abs_mult_sgn:
   578   "\<bar>a\<bar> * sgn a = a"
   579   using sgn_mult_abs [of a] by (simp add: ac_simps)
   580 
   581 lemma abs_1 [simp]:
   582   "\<bar>1\<bar> = 1"
   583   using sgn_mult_abs [of 1] by simp
   584 
   585 lemma sgn_abs [simp]:
   586   "\<bar>sgn a\<bar> = of_bool (a \<noteq> 0)"
   587   using sgn_mult_abs [of "sgn a"] mult_cancel_left [of "sgn a" "\<bar>sgn a\<bar>" 1]
   588   by (auto simp add: sgn_eq_0_iff)
   589 
   590 lemma abs_sgn [simp]:
   591   "sgn \<bar>a\<bar> = of_bool (a \<noteq> 0)"
   592   using sgn_mult_abs [of "\<bar>a\<bar>"] mult_cancel_right [of "sgn \<bar>a\<bar>" "\<bar>a\<bar>" 1]
   593   by (auto simp add: abs_eq_0_iff)
   594 
   595 lemma abs_mult:
   596   "\<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>"
   597 proof (cases "a = 0 \<or> b = 0")
   598   case True
   599   then show ?thesis
   600     by auto
   601 next
   602   case False
   603   then have *: "sgn (a * b) \<noteq> 0"
   604     by (simp add: sgn_eq_0_iff)
   605   from abs_mult_sgn [of "a * b"] abs_mult_sgn [of a] abs_mult_sgn [of b]
   606   have "\<bar>a * b\<bar> * sgn (a * b) = \<bar>a\<bar> * sgn a * \<bar>b\<bar> * sgn b"
   607     by (simp add: ac_simps)
   608   then have "\<bar>a * b\<bar> * sgn (a * b) = \<bar>a\<bar> * \<bar>b\<bar> * sgn (a * b)"
   609     by (simp add: sgn_mult ac_simps)
   610   with * show ?thesis
   611     by simp
   612 qed
   613 
   614 lemma sgn_minus [simp]:
   615   "sgn (- a) = - sgn a"
   616 proof -
   617   from sgn_minus_1 have "sgn (- 1 * a) = - 1 * sgn a"
   618     by (simp only: sgn_mult)
   619   then show ?thesis
   620     by simp
   621 qed
   622 
   623 lemma abs_minus [simp]:
   624   "\<bar>- a\<bar> = \<bar>a\<bar>"
   625 proof -
   626   have [simp]: "\<bar>- 1\<bar> = 1"
   627     using sgn_mult_abs [of "- 1"] by simp
   628   then have "\<bar>- 1 * a\<bar> = 1 * \<bar>a\<bar>"
   629     by (simp only: abs_mult)
   630   then show ?thesis
   631     by simp
   632 qed
   633 
   634 end
   635 
   636 text \<open>
   637   The theory of partially ordered rings is taken from the books:
   638     \<^item> \<^emph>\<open>Lattice Theory\<close> by Garret Birkhoff, American Mathematical Society, 1979
   639     \<^item> \<^emph>\<open>Partially Ordered Algebraic Systems\<close>, Pergamon Press, 1963
   640 
   641   Most of the used notions can also be looked up in
   642     \<^item> \<^url>\<open>http://www.mathworld.com\<close> by Eric Weisstein et. al.
   643     \<^item> \<^emph>\<open>Algebra I\<close> by van der Waerden, Springer
   644 \<close>
   645 
   646 text \<open>Syntactic division operator\<close>
   647 
   648 class divide =
   649   fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "div" 70)
   650 
   651 setup \<open>Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a \<Rightarrow> 'a \<Rightarrow> 'a"})\<close>
   652 
   653 context semiring
   654 begin
   655 
   656 lemma [field_simps]:
   657   shows distrib_left_NO_MATCH: "NO_MATCH (x div y) a \<Longrightarrow> a * (b + c) = a * b + a * c"
   658     and distrib_right_NO_MATCH: "NO_MATCH (x div y) c \<Longrightarrow> (a + b) * c = a * c + b * c"
   659   by (rule distrib_left distrib_right)+
   660 
   661 end
   662 
   663 context ring
   664 begin
   665 
   666 lemma [field_simps]:
   667   shows left_diff_distrib_NO_MATCH: "NO_MATCH (x div y) c \<Longrightarrow> (a - b) * c = a * c - b * c"
   668     and right_diff_distrib_NO_MATCH: "NO_MATCH (x div y) a \<Longrightarrow> a * (b - c) = a * b - a * c"
   669   by (rule left_diff_distrib right_diff_distrib)+
   670 
   671 end
   672 
   673 setup \<open>Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a::divide \<Rightarrow> 'a \<Rightarrow> 'a"})\<close>
   674 
   675 text \<open>Algebraic classes with division\<close>
   676   
   677 class semidom_divide = semidom + divide +
   678   assumes nonzero_mult_div_cancel_right [simp]: "b \<noteq> 0 \<Longrightarrow> (a * b) div b = a"
   679   assumes div_by_0 [simp]: "a div 0 = 0"
   680 begin
   681 
   682 lemma nonzero_mult_div_cancel_left [simp]: "a \<noteq> 0 \<Longrightarrow> (a * b) div a = b"
   683   using nonzero_mult_div_cancel_right [of a b] by (simp add: ac_simps)
   684 
   685 subclass semiring_no_zero_divisors_cancel
   686 proof
   687   show *: "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b" for a b c
   688   proof (cases "c = 0")
   689     case True
   690     then show ?thesis by simp
   691   next
   692     case False
   693     have "a = b" if "a * c = b * c"
   694     proof -
   695       from that have "a * c div c = b * c div c"
   696         by simp
   697       with False show ?thesis
   698         by simp
   699     qed
   700     then show ?thesis by auto
   701   qed
   702   show "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b" for a b c
   703     using * [of a c b] by (simp add: ac_simps)
   704 qed
   705 
   706 lemma div_self [simp]: "a \<noteq> 0 \<Longrightarrow> a div a = 1"
   707   using nonzero_mult_div_cancel_left [of a 1] by simp
   708 
   709 lemma div_0 [simp]: "0 div a = 0"
   710 proof (cases "a = 0")
   711   case True
   712   then show ?thesis by simp
   713 next
   714   case False
   715   then have "a * 0 div a = 0"
   716     by (rule nonzero_mult_div_cancel_left)
   717   then show ?thesis by simp
   718 qed
   719 
   720 lemma div_by_1 [simp]: "a div 1 = a"
   721   using nonzero_mult_div_cancel_left [of 1 a] by simp
   722 
   723 lemma dvd_div_eq_0_iff:
   724   assumes "b dvd a"
   725   shows "a div b = 0 \<longleftrightarrow> a = 0"
   726   using assms by (elim dvdE, cases "b = 0") simp_all  
   727 
   728 lemma dvd_div_eq_cancel:
   729   "a div c = b div c \<Longrightarrow> c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> a = b"
   730   by (elim dvdE, cases "c = 0") simp_all
   731 
   732 lemma dvd_div_eq_iff:
   733   "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> a div c = b div c \<longleftrightarrow> a = b"
   734   by (elim dvdE, cases "c = 0") simp_all
   735 
   736 end
   737 
   738 class idom_divide = idom + semidom_divide
   739 begin
   740 
   741 lemma dvd_neg_div:
   742   assumes "b dvd a"
   743   shows "- a div b = - (a div b)"
   744 proof (cases "b = 0")
   745   case True
   746   then show ?thesis by simp
   747 next
   748   case False
   749   from assms obtain c where "a = b * c" ..
   750   then have "- a div b = (b * - c) div b"
   751     by simp
   752   from False also have "\<dots> = - c"
   753     by (rule nonzero_mult_div_cancel_left)  
   754   with False \<open>a = b * c\<close> show ?thesis
   755     by simp
   756 qed
   757 
   758 lemma dvd_div_neg:
   759   assumes "b dvd a"
   760   shows "a div - b = - (a div b)"
   761 proof (cases "b = 0")
   762   case True
   763   then show ?thesis by simp
   764 next
   765   case False
   766   then have "- b \<noteq> 0"
   767     by simp
   768   from assms obtain c where "a = b * c" ..
   769   then have "a div - b = (- b * - c) div - b"
   770     by simp
   771   from \<open>- b \<noteq> 0\<close> also have "\<dots> = - c"
   772     by (rule nonzero_mult_div_cancel_left)  
   773   with False \<open>a = b * c\<close> show ?thesis
   774     by simp
   775 qed
   776 
   777 end
   778 
   779 class algebraic_semidom = semidom_divide
   780 begin
   781 
   782 text \<open>
   783   Class @{class algebraic_semidom} enriches a integral domain
   784   by notions from algebra, like units in a ring.
   785   It is a separate class to avoid spoiling fields with notions
   786   which are degenerated there.
   787 \<close>
   788 
   789 lemma dvd_times_left_cancel_iff [simp]:
   790   assumes "a \<noteq> 0"
   791   shows "a * b dvd a * c \<longleftrightarrow> b dvd c"
   792     (is "?lhs \<longleftrightarrow> ?rhs")
   793 proof
   794   assume ?lhs
   795   then obtain d where "a * c = a * b * d" ..
   796   with assms have "c = b * d" by (simp add: ac_simps)
   797   then show ?rhs ..
   798 next
   799   assume ?rhs
   800   then obtain d where "c = b * d" ..
   801   then have "a * c = a * b * d" by (simp add: ac_simps)
   802   then show ?lhs ..
   803 qed
   804 
   805 lemma dvd_times_right_cancel_iff [simp]:
   806   assumes "a \<noteq> 0"
   807   shows "b * a dvd c * a \<longleftrightarrow> b dvd c"
   808   using dvd_times_left_cancel_iff [of a b c] assms by (simp add: ac_simps)
   809 
   810 lemma div_dvd_iff_mult:
   811   assumes "b \<noteq> 0" and "b dvd a"
   812   shows "a div b dvd c \<longleftrightarrow> a dvd c * b"
   813 proof -
   814   from \<open>b dvd a\<close> obtain d where "a = b * d" ..
   815   with \<open>b \<noteq> 0\<close> show ?thesis by (simp add: ac_simps)
   816 qed
   817 
   818 lemma dvd_div_iff_mult:
   819   assumes "c \<noteq> 0" and "c dvd b"
   820   shows "a dvd b div c \<longleftrightarrow> a * c dvd b"
   821 proof -
   822   from \<open>c dvd b\<close> obtain d where "b = c * d" ..
   823   with \<open>c \<noteq> 0\<close> show ?thesis by (simp add: mult.commute [of a])
   824 qed
   825 
   826 lemma div_dvd_div [simp]:
   827   assumes "a dvd b" and "a dvd c"
   828   shows "b div a dvd c div a \<longleftrightarrow> b dvd c"
   829 proof (cases "a = 0")
   830   case True
   831   with assms show ?thesis by simp
   832 next
   833   case False
   834   moreover from assms obtain k l where "b = a * k" and "c = a * l"
   835     by (auto elim!: dvdE)
   836   ultimately show ?thesis by simp
   837 qed
   838 
   839 lemma div_add [simp]:
   840   assumes "c dvd a" and "c dvd b"
   841   shows "(a + b) div c = a div c + b div c"
   842 proof (cases "c = 0")
   843   case True
   844   then show ?thesis by simp
   845 next
   846   case False
   847   moreover from assms obtain k l where "a = c * k" and "b = c * l"
   848     by (auto elim!: dvdE)
   849   moreover have "c * k + c * l = c * (k + l)"
   850     by (simp add: algebra_simps)
   851   ultimately show ?thesis
   852     by simp
   853 qed
   854 
   855 lemma div_mult_div_if_dvd:
   856   assumes "b dvd a" and "d dvd c"
   857   shows "(a div b) * (c div d) = (a * c) div (b * d)"
   858 proof (cases "b = 0 \<or> c = 0")
   859   case True
   860   with assms show ?thesis by auto
   861 next
   862   case False
   863   moreover from assms obtain k l where "a = b * k" and "c = d * l"
   864     by (auto elim!: dvdE)
   865   moreover have "b * k * (d * l) div (b * d) = (b * d) * (k * l) div (b * d)"
   866     by (simp add: ac_simps)
   867   ultimately show ?thesis by simp
   868 qed
   869 
   870 lemma dvd_div_eq_mult:
   871   assumes "a \<noteq> 0" and "a dvd b"
   872   shows "b div a = c \<longleftrightarrow> b = c * a"
   873     (is "?lhs \<longleftrightarrow> ?rhs")
   874 proof
   875   assume ?rhs
   876   then show ?lhs by (simp add: assms)
   877 next
   878   assume ?lhs
   879   then have "b div a * a = c * a" by simp
   880   moreover from assms have "b div a * a = b"
   881     by (auto elim!: dvdE simp add: ac_simps)
   882   ultimately show ?rhs by simp
   883 qed
   884 
   885 lemma dvd_div_mult_self [simp]: "a dvd b \<Longrightarrow> b div a * a = b"
   886   by (cases "a = 0") (auto elim: dvdE simp add: ac_simps)
   887 
   888 lemma dvd_mult_div_cancel [simp]: "a dvd b \<Longrightarrow> a * (b div a) = b"
   889   using dvd_div_mult_self [of a b] by (simp add: ac_simps)
   890 
   891 lemma div_mult_swap:
   892   assumes "c dvd b"
   893   shows "a * (b div c) = (a * b) div c"
   894 proof (cases "c = 0")
   895   case True
   896   then show ?thesis by simp
   897 next
   898   case False
   899   from assms obtain d where "b = c * d" ..
   900   moreover from False have "a * divide (d * c) c = ((a * d) * c) div c"
   901     by simp
   902   ultimately show ?thesis by (simp add: ac_simps)
   903 qed
   904 
   905 lemma dvd_div_mult: "c dvd b \<Longrightarrow> b div c * a = (b * a) div c"
   906   using div_mult_swap [of c b a] by (simp add: ac_simps)
   907 
   908 lemma dvd_div_mult2_eq:
   909   assumes "b * c dvd a"
   910   shows "a div (b * c) = a div b div c"
   911 proof -
   912   from assms obtain k where "a = b * c * k" ..
   913   then show ?thesis
   914     by (cases "b = 0 \<or> c = 0") (auto, simp add: ac_simps)
   915 qed
   916 
   917 lemma dvd_div_div_eq_mult:
   918   assumes "a \<noteq> 0" "c \<noteq> 0" and "a dvd b" "c dvd d"
   919   shows "b div a = d div c \<longleftrightarrow> b * c = a * d"
   920     (is "?lhs \<longleftrightarrow> ?rhs")
   921 proof -
   922   from assms have "a * c \<noteq> 0" by simp
   923   then have "?lhs \<longleftrightarrow> b div a * (a * c) = d div c * (a * c)"
   924     by simp
   925   also have "\<dots> \<longleftrightarrow> (a * (b div a)) * c = (c * (d div c)) * a"
   926     by (simp add: ac_simps)
   927   also have "\<dots> \<longleftrightarrow> (a * b div a) * c = (c * d div c) * a"
   928     using assms by (simp add: div_mult_swap)
   929   also have "\<dots> \<longleftrightarrow> ?rhs"
   930     using assms by (simp add: ac_simps)
   931   finally show ?thesis .
   932 qed
   933 
   934 lemma dvd_mult_imp_div:
   935   assumes "a * c dvd b"
   936   shows "a dvd b div c"
   937 proof (cases "c = 0")
   938   case True then show ?thesis by simp
   939 next
   940   case False
   941   from \<open>a * c dvd b\<close> obtain d where "b = a * c * d" ..
   942   with False show ?thesis
   943     by (simp add: mult.commute [of a] mult.assoc)
   944 qed
   945 
   946 lemma div_div_eq_right:
   947   assumes "c dvd b" "b dvd a"
   948   shows   "a div (b div c) = a div b * c"
   949 proof (cases "c = 0 \<or> b = 0")
   950   case True
   951   then show ?thesis
   952     by auto
   953 next
   954   case False
   955   from assms obtain r s where "b = c * r" and "a = c * r * s"
   956     by (blast elim: dvdE)
   957   moreover with False have "r \<noteq> 0"
   958     by auto
   959   ultimately show ?thesis using False
   960     by simp (simp add: mult.commute [of _ r] mult.assoc mult.commute [of c])
   961 qed
   962 
   963 lemma div_div_div_same:
   964   assumes "d dvd b" "b dvd a"
   965   shows   "(a div d) div (b div d) = a div b"
   966 proof (cases "b = 0 \<or> d = 0")
   967   case True
   968   with assms show ?thesis
   969     by auto
   970 next
   971   case False
   972   from assms obtain r s
   973     where "a = d * r * s" and "b = d * r"
   974     by (blast elim: dvdE)
   975   with False show ?thesis
   976     by simp (simp add: ac_simps)
   977 qed
   978 
   979 
   980 text \<open>Units: invertible elements in a ring\<close>
   981 
   982 abbreviation is_unit :: "'a \<Rightarrow> bool"
   983   where "is_unit a \<equiv> a dvd 1"
   984 
   985 lemma not_is_unit_0 [simp]: "\<not> is_unit 0"
   986   by simp
   987 
   988 lemma unit_imp_dvd [dest]: "is_unit b \<Longrightarrow> b dvd a"
   989   by (rule dvd_trans [of _ 1]) simp_all
   990 
   991 lemma unit_dvdE:
   992   assumes "is_unit a"
   993   obtains c where "a \<noteq> 0" and "b = a * c"
   994 proof -
   995   from assms have "a dvd b" by auto
   996   then obtain c where "b = a * c" ..
   997   moreover from assms have "a \<noteq> 0" by auto
   998   ultimately show thesis using that by blast
   999 qed
  1000 
  1001 lemma dvd_unit_imp_unit: "a dvd b \<Longrightarrow> is_unit b \<Longrightarrow> is_unit a"
  1002   by (rule dvd_trans)
  1003 
  1004 lemma unit_div_1_unit [simp, intro]:
  1005   assumes "is_unit a"
  1006   shows "is_unit (1 div a)"
  1007 proof -
  1008   from assms have "1 = 1 div a * a" by simp
  1009   then show "is_unit (1 div a)" by (rule dvdI)
  1010 qed
  1011 
  1012 lemma is_unitE [elim?]:
  1013   assumes "is_unit a"
  1014   obtains b where "a \<noteq> 0" and "b \<noteq> 0"
  1015     and "is_unit b" and "1 div a = b" and "1 div b = a"
  1016     and "a * b = 1" and "c div a = c * b"
  1017 proof (rule that)
  1018   define b where "b = 1 div a"
  1019   then show "1 div a = b" by simp
  1020   from assms b_def show "is_unit b" by simp
  1021   with assms show "a \<noteq> 0" and "b \<noteq> 0" by auto
  1022   from assms b_def show "a * b = 1" by simp
  1023   then have "1 = a * b" ..
  1024   with b_def \<open>b \<noteq> 0\<close> show "1 div b = a" by simp
  1025   from assms have "a dvd c" ..
  1026   then obtain d where "c = a * d" ..
  1027   with \<open>a \<noteq> 0\<close> \<open>a * b = 1\<close> show "c div a = c * b"
  1028     by (simp add: mult.assoc mult.left_commute [of a])
  1029 qed
  1030 
  1031 lemma unit_prod [intro]: "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a * b)"
  1032   by (subst mult_1_left [of 1, symmetric]) (rule mult_dvd_mono)
  1033 
  1034 lemma is_unit_mult_iff: "is_unit (a * b) \<longleftrightarrow> is_unit a \<and> is_unit b"
  1035   by (auto dest: dvd_mult_left dvd_mult_right)
  1036 
  1037 lemma unit_div [intro]: "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a div b)"
  1038   by (erule is_unitE [of b a]) (simp add: ac_simps unit_prod)
  1039 
  1040 lemma mult_unit_dvd_iff:
  1041   assumes "is_unit b"
  1042   shows "a * b dvd c \<longleftrightarrow> a dvd c"
  1043 proof
  1044   assume "a * b dvd c"
  1045   with assms show "a dvd c"
  1046     by (simp add: dvd_mult_left)
  1047 next
  1048   assume "a dvd c"
  1049   then obtain k where "c = a * k" ..
  1050   with assms have "c = (a * b) * (1 div b * k)"
  1051     by (simp add: mult_ac)
  1052   then show "a * b dvd c" by (rule dvdI)
  1053 qed
  1054 
  1055 lemma mult_unit_dvd_iff': "is_unit a \<Longrightarrow> (a * b) dvd c \<longleftrightarrow> b dvd c"
  1056   using mult_unit_dvd_iff [of a b c] by (simp add: ac_simps)
  1057 
  1058 lemma dvd_mult_unit_iff:
  1059   assumes "is_unit b"
  1060   shows "a dvd c * b \<longleftrightarrow> a dvd c"
  1061 proof
  1062   assume "a dvd c * b"
  1063   with assms have "c * b dvd c * (b * (1 div b))"
  1064     by (subst mult_assoc [symmetric]) simp
  1065   also from assms have "b * (1 div b) = 1"
  1066     by (rule is_unitE) simp
  1067   finally have "c * b dvd c" by simp
  1068   with \<open>a dvd c * b\<close> show "a dvd c" by (rule dvd_trans)
  1069 next
  1070   assume "a dvd c"
  1071   then show "a dvd c * b" by simp
  1072 qed
  1073 
  1074 lemma dvd_mult_unit_iff': "is_unit b \<Longrightarrow> a dvd b * c \<longleftrightarrow> a dvd c"
  1075   using dvd_mult_unit_iff [of b a c] by (simp add: ac_simps)
  1076 
  1077 lemma div_unit_dvd_iff: "is_unit b \<Longrightarrow> a div b dvd c \<longleftrightarrow> a dvd c"
  1078   by (erule is_unitE [of _ a]) (auto simp add: mult_unit_dvd_iff)
  1079 
  1080 lemma dvd_div_unit_iff: "is_unit b \<Longrightarrow> a dvd c div b \<longleftrightarrow> a dvd c"
  1081   by (erule is_unitE [of _ c]) (simp add: dvd_mult_unit_iff)
  1082 
  1083 lemmas unit_dvd_iff = mult_unit_dvd_iff mult_unit_dvd_iff'
  1084   dvd_mult_unit_iff dvd_mult_unit_iff' 
  1085   div_unit_dvd_iff dvd_div_unit_iff (* FIXME consider named_theorems *)
  1086 
  1087 lemma unit_mult_div_div [simp]: "is_unit a \<Longrightarrow> b * (1 div a) = b div a"
  1088   by (erule is_unitE [of _ b]) simp
  1089 
  1090 lemma unit_div_mult_self [simp]: "is_unit a \<Longrightarrow> b div a * a = b"
  1091   by (rule dvd_div_mult_self) auto
  1092 
  1093 lemma unit_div_1_div_1 [simp]: "is_unit a \<Longrightarrow> 1 div (1 div a) = a"
  1094   by (erule is_unitE) simp
  1095 
  1096 lemma unit_div_mult_swap: "is_unit c \<Longrightarrow> a * (b div c) = (a * b) div c"
  1097   by (erule unit_dvdE [of _ b]) (simp add: mult.left_commute [of _ c])
  1098 
  1099 lemma unit_div_commute: "is_unit b \<Longrightarrow> (a div b) * c = (a * c) div b"
  1100   using unit_div_mult_swap [of b c a] by (simp add: ac_simps)
  1101 
  1102 lemma unit_eq_div1: "is_unit b \<Longrightarrow> a div b = c \<longleftrightarrow> a = c * b"
  1103   by (auto elim: is_unitE)
  1104 
  1105 lemma unit_eq_div2: "is_unit b \<Longrightarrow> a = c div b \<longleftrightarrow> a * b = c"
  1106   using unit_eq_div1 [of b c a] by auto
  1107 
  1108 lemma unit_mult_left_cancel: "is_unit a \<Longrightarrow> a * b = a * c \<longleftrightarrow> b = c"
  1109   using mult_cancel_left [of a b c] by auto
  1110 
  1111 lemma unit_mult_right_cancel: "is_unit a \<Longrightarrow> b * a = c * a \<longleftrightarrow> b = c"
  1112   using unit_mult_left_cancel [of a b c] by (auto simp add: ac_simps)
  1113 
  1114 lemma unit_div_cancel:
  1115   assumes "is_unit a"
  1116   shows "b div a = c div a \<longleftrightarrow> b = c"
  1117 proof -
  1118   from assms have "is_unit (1 div a)" by simp
  1119   then have "b * (1 div a) = c * (1 div a) \<longleftrightarrow> b = c"
  1120     by (rule unit_mult_right_cancel)
  1121   with assms show ?thesis by simp
  1122 qed
  1123 
  1124 lemma is_unit_div_mult2_eq:
  1125   assumes "is_unit b" and "is_unit c"
  1126   shows "a div (b * c) = a div b div c"
  1127 proof -
  1128   from assms have "is_unit (b * c)"
  1129     by (simp add: unit_prod)
  1130   then have "b * c dvd a"
  1131     by (rule unit_imp_dvd)
  1132   then show ?thesis
  1133     by (rule dvd_div_mult2_eq)
  1134 qed
  1135 
  1136 lemmas unit_simps = mult_unit_dvd_iff div_unit_dvd_iff dvd_mult_unit_iff
  1137   dvd_div_unit_iff unit_div_mult_swap unit_div_commute
  1138   unit_mult_left_cancel unit_mult_right_cancel unit_div_cancel
  1139   unit_eq_div1 unit_eq_div2
  1140 
  1141 lemma is_unit_div_mult_cancel_left:
  1142   assumes "a \<noteq> 0" and "is_unit b"
  1143   shows "a div (a * b) = 1 div b"
  1144 proof -
  1145   from assms have "a div (a * b) = a div a div b"
  1146     by (simp add: mult_unit_dvd_iff dvd_div_mult2_eq)
  1147   with assms show ?thesis by simp
  1148 qed
  1149 
  1150 lemma is_unit_div_mult_cancel_right:
  1151   assumes "a \<noteq> 0" and "is_unit b"
  1152   shows "a div (b * a) = 1 div b"
  1153   using assms is_unit_div_mult_cancel_left [of a b] by (simp add: ac_simps)
  1154 
  1155 lemma unit_div_eq_0_iff:
  1156   assumes "is_unit b"
  1157   shows "a div b = 0 \<longleftrightarrow> a = 0"
  1158   by (rule dvd_div_eq_0_iff) (insert assms, auto)  
  1159 
  1160 lemma div_mult_unit2:
  1161   "is_unit c \<Longrightarrow> b dvd a \<Longrightarrow> a div (b * c) = a div b div c"
  1162   by (rule dvd_div_mult2_eq) (simp_all add: mult_unit_dvd_iff)
  1163 
  1164 end
  1165 
  1166 class unit_factor =
  1167   fixes unit_factor :: "'a \<Rightarrow> 'a"
  1168 
  1169 class semidom_divide_unit_factor = semidom_divide + unit_factor +
  1170   assumes unit_factor_0 [simp]: "unit_factor 0 = 0"
  1171     and is_unit_unit_factor: "a dvd 1 \<Longrightarrow> unit_factor a = a"
  1172     and unit_factor_is_unit: "a \<noteq> 0 \<Longrightarrow> unit_factor a dvd 1"
  1173     and unit_factor_mult: "unit_factor (a * b) = unit_factor a * unit_factor b"
  1174   -- \<open>This fine-grained hierarchy will later on allow lean normalization of polynomials\<close>
  1175   
  1176 class normalization_semidom = algebraic_semidom + semidom_divide_unit_factor +
  1177   fixes normalize :: "'a \<Rightarrow> 'a"
  1178   assumes unit_factor_mult_normalize [simp]: "unit_factor a * normalize a = a"
  1179     and normalize_0 [simp]: "normalize 0 = 0"
  1180 begin
  1181 
  1182 text \<open>
  1183   Class @{class normalization_semidom} cultivates the idea that each integral
  1184   domain can be split into equivalence classes whose representants are
  1185   associated, i.e. divide each other. @{const normalize} specifies a canonical
  1186   representant for each equivalence class. The rationale behind this is that
  1187   it is easier to reason about equality than equivalences, hence we prefer to
  1188   think about equality of normalized values rather than associated elements.
  1189 \<close>
  1190 
  1191 declare unit_factor_is_unit [iff]
  1192   
  1193 lemma unit_factor_dvd [simp]: "a \<noteq> 0 \<Longrightarrow> unit_factor a dvd b"
  1194   by (rule unit_imp_dvd) simp
  1195 
  1196 lemma unit_factor_self [simp]: "unit_factor a dvd a"
  1197   by (cases "a = 0") simp_all
  1198 
  1199 lemma normalize_mult_unit_factor [simp]: "normalize a * unit_factor a = a"
  1200   using unit_factor_mult_normalize [of a] by (simp add: ac_simps)
  1201 
  1202 lemma normalize_eq_0_iff [simp]: "normalize a = 0 \<longleftrightarrow> a = 0"
  1203   (is "?lhs \<longleftrightarrow> ?rhs")
  1204 proof
  1205   assume ?lhs
  1206   moreover have "unit_factor a * normalize a = a" by simp
  1207   ultimately show ?rhs by simp
  1208 next
  1209   assume ?rhs
  1210   then show ?lhs by simp
  1211 qed
  1212 
  1213 lemma unit_factor_eq_0_iff [simp]: "unit_factor a = 0 \<longleftrightarrow> a = 0"
  1214   (is "?lhs \<longleftrightarrow> ?rhs")
  1215 proof
  1216   assume ?lhs
  1217   moreover have "unit_factor a * normalize a = a" by simp
  1218   ultimately show ?rhs by simp
  1219 next
  1220   assume ?rhs
  1221   then show ?lhs by simp
  1222 qed
  1223 
  1224 lemma div_unit_factor [simp]: "a div unit_factor a = normalize a"
  1225 proof (cases "a = 0")
  1226   case True
  1227   then show ?thesis by simp
  1228 next
  1229   case False
  1230   then have "unit_factor a \<noteq> 0"
  1231     by simp
  1232   with nonzero_mult_div_cancel_left
  1233   have "unit_factor a * normalize a div unit_factor a = normalize a"
  1234     by blast
  1235   then show ?thesis by simp
  1236 qed
  1237 
  1238 lemma normalize_div [simp]: "normalize a div a = 1 div unit_factor a"
  1239 proof (cases "a = 0")
  1240   case True
  1241   then show ?thesis by simp
  1242 next
  1243   case False
  1244   have "normalize a div a = normalize a div (unit_factor a * normalize a)"
  1245     by simp
  1246   also have "\<dots> = 1 div unit_factor a"
  1247     using False by (subst is_unit_div_mult_cancel_right) simp_all
  1248   finally show ?thesis .
  1249 qed
  1250 
  1251 lemma is_unit_normalize:
  1252   assumes "is_unit a"
  1253   shows "normalize a = 1"
  1254 proof -
  1255   from assms have "unit_factor a = a"
  1256     by (rule is_unit_unit_factor)
  1257   moreover from assms have "a \<noteq> 0"
  1258     by auto
  1259   moreover have "normalize a = a div unit_factor a"
  1260     by simp
  1261   ultimately show ?thesis
  1262     by simp
  1263 qed
  1264 
  1265 lemma unit_factor_1 [simp]: "unit_factor 1 = 1"
  1266   by (rule is_unit_unit_factor) simp
  1267 
  1268 lemma normalize_1 [simp]: "normalize 1 = 1"
  1269   by (rule is_unit_normalize) simp
  1270 
  1271 lemma normalize_1_iff: "normalize a = 1 \<longleftrightarrow> is_unit a"
  1272   (is "?lhs \<longleftrightarrow> ?rhs")
  1273 proof
  1274   assume ?rhs
  1275   then show ?lhs by (rule is_unit_normalize)
  1276 next
  1277   assume ?lhs
  1278   then have "unit_factor a * normalize a = unit_factor a * 1"
  1279     by simp
  1280   then have "unit_factor a = a"
  1281     by simp
  1282   moreover
  1283   from \<open>?lhs\<close> have "a \<noteq> 0" by auto
  1284   then have "is_unit (unit_factor a)" by simp
  1285   ultimately show ?rhs by simp
  1286 qed
  1287 
  1288 lemma div_normalize [simp]: "a div normalize a = unit_factor a"
  1289 proof (cases "a = 0")
  1290   case True
  1291   then show ?thesis by simp
  1292 next
  1293   case False
  1294   then have "normalize a \<noteq> 0" by simp
  1295   with nonzero_mult_div_cancel_right
  1296   have "unit_factor a * normalize a div normalize a = unit_factor a" by blast
  1297   then show ?thesis by simp
  1298 qed
  1299 
  1300 lemma mult_one_div_unit_factor [simp]: "a * (1 div unit_factor b) = a div unit_factor b"
  1301   by (cases "b = 0") simp_all
  1302 
  1303 lemma inv_unit_factor_eq_0_iff [simp]:
  1304   "1 div unit_factor a = 0 \<longleftrightarrow> a = 0"
  1305   (is "?lhs \<longleftrightarrow> ?rhs")
  1306 proof
  1307   assume ?lhs
  1308   then have "a * (1 div unit_factor a) = a * 0"
  1309     by simp
  1310   then show ?rhs
  1311     by simp
  1312 next
  1313   assume ?rhs
  1314   then show ?lhs by simp
  1315 qed
  1316 
  1317 lemma normalize_mult: "normalize (a * b) = normalize a * normalize b"
  1318 proof (cases "a = 0 \<or> b = 0")
  1319   case True
  1320   then show ?thesis by auto
  1321 next
  1322   case False
  1323   have "unit_factor (a * b) * normalize (a * b) = a * b"
  1324     by (rule unit_factor_mult_normalize)
  1325   then have "normalize (a * b) = a * b div unit_factor (a * b)"
  1326     by simp
  1327   also have "\<dots> = a * b div unit_factor (b * a)"
  1328     by (simp add: ac_simps)
  1329   also have "\<dots> = a * b div unit_factor b div unit_factor a"
  1330     using False by (simp add: unit_factor_mult is_unit_div_mult2_eq [symmetric])
  1331   also have "\<dots> = a * (b div unit_factor b) div unit_factor a"
  1332     using False by (subst unit_div_mult_swap) simp_all
  1333   also have "\<dots> = normalize a * normalize b"
  1334     using False
  1335     by (simp add: mult.commute [of a] mult.commute [of "normalize a"] unit_div_mult_swap [symmetric])
  1336   finally show ?thesis .
  1337 qed
  1338 
  1339 lemma unit_factor_idem [simp]: "unit_factor (unit_factor a) = unit_factor a"
  1340   by (cases "a = 0") (auto intro: is_unit_unit_factor)
  1341 
  1342 lemma normalize_unit_factor [simp]: "a \<noteq> 0 \<Longrightarrow> normalize (unit_factor a) = 1"
  1343   by (rule is_unit_normalize) simp
  1344 
  1345 lemma normalize_idem [simp]: "normalize (normalize a) = normalize a"
  1346 proof (cases "a = 0")
  1347   case True
  1348   then show ?thesis by simp
  1349 next
  1350   case False
  1351   have "normalize a = normalize (unit_factor a * normalize a)"
  1352     by simp
  1353   also have "\<dots> = normalize (unit_factor a) * normalize (normalize a)"
  1354     by (simp only: normalize_mult)
  1355   finally show ?thesis
  1356     using False by simp_all
  1357 qed
  1358 
  1359 lemma unit_factor_normalize [simp]:
  1360   assumes "a \<noteq> 0"
  1361   shows "unit_factor (normalize a) = 1"
  1362 proof -
  1363   from assms have *: "normalize a \<noteq> 0"
  1364     by simp
  1365   have "unit_factor (normalize a) * normalize (normalize a) = normalize a"
  1366     by (simp only: unit_factor_mult_normalize)
  1367   then have "unit_factor (normalize a) * normalize a = normalize a"
  1368     by simp
  1369   with * have "unit_factor (normalize a) * normalize a div normalize a = normalize a div normalize a"
  1370     by simp
  1371   with * show ?thesis
  1372     by simp
  1373 qed
  1374 
  1375 lemma dvd_unit_factor_div:
  1376   assumes "b dvd a"
  1377   shows "unit_factor (a div b) = unit_factor a div unit_factor b"
  1378 proof -
  1379   from assms have "a = a div b * b"
  1380     by simp
  1381   then have "unit_factor a = unit_factor (a div b * b)"
  1382     by simp
  1383   then show ?thesis
  1384     by (cases "b = 0") (simp_all add: unit_factor_mult)
  1385 qed
  1386 
  1387 lemma dvd_normalize_div:
  1388   assumes "b dvd a"
  1389   shows "normalize (a div b) = normalize a div normalize b"
  1390 proof -
  1391   from assms have "a = a div b * b"
  1392     by simp
  1393   then have "normalize a = normalize (a div b * b)"
  1394     by simp
  1395   then show ?thesis
  1396     by (cases "b = 0") (simp_all add: normalize_mult)
  1397 qed
  1398 
  1399 lemma normalize_dvd_iff [simp]: "normalize a dvd b \<longleftrightarrow> a dvd b"
  1400 proof -
  1401   have "normalize a dvd b \<longleftrightarrow> unit_factor a * normalize a dvd b"
  1402     using mult_unit_dvd_iff [of "unit_factor a" "normalize a" b]
  1403       by (cases "a = 0") simp_all
  1404   then show ?thesis by simp
  1405 qed
  1406 
  1407 lemma dvd_normalize_iff [simp]: "a dvd normalize b \<longleftrightarrow> a dvd b"
  1408 proof -
  1409   have "a dvd normalize  b \<longleftrightarrow> a dvd normalize b * unit_factor b"
  1410     using dvd_mult_unit_iff [of "unit_factor b" a "normalize b"]
  1411       by (cases "b = 0") simp_all
  1412   then show ?thesis by simp
  1413 qed
  1414 
  1415 lemma normalize_idem_imp_unit_factor_eq:
  1416   assumes "normalize a = a"
  1417   shows "unit_factor a = of_bool (a \<noteq> 0)"
  1418 proof (cases "a = 0")
  1419   case True
  1420   then show ?thesis
  1421     by simp
  1422 next
  1423   case False
  1424   then show ?thesis
  1425     using assms unit_factor_normalize [of a] by simp
  1426 qed
  1427 
  1428 lemma normalize_idem_imp_is_unit_iff:
  1429   assumes "normalize a = a"
  1430   shows "is_unit a \<longleftrightarrow> a = 1"
  1431   using assms by (cases "a = 0") (auto dest: is_unit_normalize)
  1432 
  1433 text \<open>
  1434   We avoid an explicit definition of associated elements but prefer explicit
  1435   normalisation instead. In theory we could define an abbreviation like @{prop
  1436   "associated a b \<longleftrightarrow> normalize a = normalize b"} but this is counterproductive
  1437   without suggestive infix syntax, which we do not want to sacrifice for this
  1438   purpose here.
  1439 \<close>
  1440 
  1441 lemma associatedI:
  1442   assumes "a dvd b" and "b dvd a"
  1443   shows "normalize a = normalize b"
  1444 proof (cases "a = 0 \<or> b = 0")
  1445   case True
  1446   with assms show ?thesis by auto
  1447 next
  1448   case False
  1449   from \<open>a dvd b\<close> obtain c where b: "b = a * c" ..
  1450   moreover from \<open>b dvd a\<close> obtain d where a: "a = b * d" ..
  1451   ultimately have "b * 1 = b * (c * d)"
  1452     by (simp add: ac_simps)
  1453   with False have "1 = c * d"
  1454     unfolding mult_cancel_left by simp
  1455   then have "is_unit c" and "is_unit d"
  1456     by auto
  1457   with a b show ?thesis
  1458     by (simp add: normalize_mult is_unit_normalize)
  1459 qed
  1460 
  1461 lemma associatedD1: "normalize a = normalize b \<Longrightarrow> a dvd b"
  1462   using dvd_normalize_iff [of _ b, symmetric] normalize_dvd_iff [of a _, symmetric]
  1463   by simp
  1464 
  1465 lemma associatedD2: "normalize a = normalize b \<Longrightarrow> b dvd a"
  1466   using dvd_normalize_iff [of _ a, symmetric] normalize_dvd_iff [of b _, symmetric]
  1467   by simp
  1468 
  1469 lemma associated_unit: "normalize a = normalize b \<Longrightarrow> is_unit a \<Longrightarrow> is_unit b"
  1470   using dvd_unit_imp_unit by (auto dest!: associatedD1 associatedD2)
  1471 
  1472 lemma associated_iff_dvd: "normalize a = normalize b \<longleftrightarrow> a dvd b \<and> b dvd a"
  1473   (is "?lhs \<longleftrightarrow> ?rhs")
  1474 proof
  1475   assume ?rhs
  1476   then show ?lhs by (auto intro!: associatedI)
  1477 next
  1478   assume ?lhs
  1479   then have "unit_factor a * normalize a = unit_factor a * normalize b"
  1480     by simp
  1481   then have *: "normalize b * unit_factor a = a"
  1482     by (simp add: ac_simps)
  1483   show ?rhs
  1484   proof (cases "a = 0 \<or> b = 0")
  1485     case True
  1486     with \<open>?lhs\<close> show ?thesis by auto
  1487   next
  1488     case False
  1489     then have "b dvd normalize b * unit_factor a" and "normalize b * unit_factor a dvd b"
  1490       by (simp_all add: mult_unit_dvd_iff dvd_mult_unit_iff)
  1491     with * show ?thesis by simp
  1492   qed
  1493 qed
  1494 
  1495 lemma associated_eqI:
  1496   assumes "a dvd b" and "b dvd a"
  1497   assumes "normalize a = a" and "normalize b = b"
  1498   shows "a = b"
  1499 proof -
  1500   from assms have "normalize a = normalize b"
  1501     unfolding associated_iff_dvd by simp
  1502   with \<open>normalize a = a\<close> have "a = normalize b"
  1503     by simp
  1504   with \<open>normalize b = b\<close> show "a = b"
  1505     by simp
  1506 qed
  1507 
  1508 lemma normalize_unit_factor_eqI:
  1509   assumes "normalize a = normalize b"
  1510     and "unit_factor a = unit_factor b"
  1511   shows "a = b"
  1512 proof -
  1513   from assms have "unit_factor a * normalize a = unit_factor b * normalize b"
  1514     by simp
  1515   then show ?thesis
  1516     by simp
  1517 qed
  1518 
  1519 end
  1520 
  1521 
  1522 text \<open>Syntactic division remainder operator\<close>
  1523 
  1524 class modulo = dvd + divide +
  1525   fixes modulo :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "mod" 70)
  1526 
  1527 text \<open>Arbitrary quotient and remainder partitions\<close>
  1528 
  1529 class semiring_modulo = comm_semiring_1_cancel + divide + modulo +
  1530   assumes div_mult_mod_eq: "a div b * b + a mod b = a"
  1531 begin
  1532 
  1533 lemma mod_div_decomp:
  1534   fixes a b
  1535   obtains q r where "q = a div b" and "r = a mod b"
  1536     and "a = q * b + r"
  1537 proof -
  1538   from div_mult_mod_eq have "a = a div b * b + a mod b" by simp
  1539   moreover have "a div b = a div b" ..
  1540   moreover have "a mod b = a mod b" ..
  1541   note that ultimately show thesis by blast
  1542 qed
  1543 
  1544 lemma mult_div_mod_eq: "b * (a div b) + a mod b = a"
  1545   using div_mult_mod_eq [of a b] by (simp add: ac_simps)
  1546 
  1547 lemma mod_div_mult_eq: "a mod b + a div b * b = a"
  1548   using div_mult_mod_eq [of a b] by (simp add: ac_simps)
  1549 
  1550 lemma mod_mult_div_eq: "a mod b + b * (a div b) = a"
  1551   using div_mult_mod_eq [of a b] by (simp add: ac_simps)
  1552 
  1553 lemma minus_div_mult_eq_mod: "a - a div b * b = a mod b"
  1554   by (rule add_implies_diff [symmetric]) (fact mod_div_mult_eq)
  1555 
  1556 lemma minus_mult_div_eq_mod: "a - b * (a div b) = a mod b"
  1557   by (rule add_implies_diff [symmetric]) (fact mod_mult_div_eq)
  1558 
  1559 lemma minus_mod_eq_div_mult: "a - a mod b = a div b * b"
  1560   by (rule add_implies_diff [symmetric]) (fact div_mult_mod_eq)
  1561 
  1562 lemma minus_mod_eq_mult_div: "a - a mod b = b * (a div b)"
  1563   by (rule add_implies_diff [symmetric]) (fact mult_div_mod_eq)
  1564 
  1565 end
  1566 
  1567 
  1568 text \<open>Quotient and remainder in integral domains\<close>
  1569 
  1570 class semidom_modulo = algebraic_semidom + semiring_modulo
  1571 begin
  1572 
  1573 lemma mod_0 [simp]: "0 mod a = 0"
  1574   using div_mult_mod_eq [of 0 a] by simp
  1575 
  1576 lemma mod_by_0 [simp]: "a mod 0 = a"
  1577   using div_mult_mod_eq [of a 0] by simp
  1578 
  1579 lemma mod_by_1 [simp]:
  1580   "a mod 1 = 0"
  1581 proof -
  1582   from div_mult_mod_eq [of a one] div_by_1 have "a + a mod 1 = a" by simp
  1583   then have "a + a mod 1 = a + 0" by simp
  1584   then show ?thesis by (rule add_left_imp_eq)
  1585 qed
  1586 
  1587 lemma mod_self [simp]:
  1588   "a mod a = 0"
  1589   using div_mult_mod_eq [of a a] by simp
  1590 
  1591 lemma dvd_imp_mod_0 [simp]:
  1592   assumes "a dvd b"
  1593   shows "b mod a = 0"
  1594   using assms minus_div_mult_eq_mod [of b a] by simp
  1595 
  1596 lemma mod_0_imp_dvd: 
  1597   assumes "a mod b = 0"
  1598   shows   "b dvd a"
  1599 proof -
  1600   have "b dvd ((a div b) * b)" by simp
  1601   also have "(a div b) * b = a"
  1602     using div_mult_mod_eq [of a b] by (simp add: assms)
  1603   finally show ?thesis .
  1604 qed
  1605 
  1606 lemma mod_eq_0_iff_dvd:
  1607   "a mod b = 0 \<longleftrightarrow> b dvd a"
  1608   by (auto intro: mod_0_imp_dvd)
  1609 
  1610 lemma dvd_eq_mod_eq_0 [nitpick_unfold, code]:
  1611   "a dvd b \<longleftrightarrow> b mod a = 0"
  1612   by (simp add: mod_eq_0_iff_dvd)
  1613 
  1614 lemma dvd_mod_iff: 
  1615   assumes "c dvd b"
  1616   shows "c dvd a mod b \<longleftrightarrow> c dvd a"
  1617 proof -
  1618   from assms have "(c dvd a mod b) \<longleftrightarrow> (c dvd ((a div b) * b + a mod b))" 
  1619     by (simp add: dvd_add_right_iff)
  1620   also have "(a div b) * b + a mod b = a"
  1621     using div_mult_mod_eq [of a b] by simp
  1622   finally show ?thesis .
  1623 qed
  1624 
  1625 lemma dvd_mod_imp_dvd:
  1626   assumes "c dvd a mod b" and "c dvd b"
  1627   shows "c dvd a"
  1628   using assms dvd_mod_iff [of c b a] by simp
  1629 
  1630 lemma dvd_minus_mod [simp]:
  1631   "b dvd a - a mod b"
  1632   by (simp add: minus_mod_eq_div_mult)
  1633 
  1634 lemma cancel_div_mod_rules:
  1635   "((a div b) * b + a mod b) + c = a + c"
  1636   "(b * (a div b) + a mod b) + c = a + c"
  1637   by (simp_all add: div_mult_mod_eq mult_div_mod_eq)
  1638 
  1639 end
  1640 
  1641 text \<open>Interlude: basic tool support for algebraic and arithmetic calculations\<close>
  1642 
  1643 named_theorems arith "arith facts -- only ground formulas"
  1644 ML_file "Tools/arith_data.ML"
  1645 
  1646 ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
  1647 
  1648 ML \<open>
  1649 structure Cancel_Div_Mod_Ring = Cancel_Div_Mod
  1650 (
  1651   val div_name = @{const_name divide};
  1652   val mod_name = @{const_name modulo};
  1653   val mk_binop = HOLogic.mk_binop;
  1654   val mk_sum = Arith_Data.mk_sum;
  1655   val dest_sum = Arith_Data.dest_sum;
  1656 
  1657   val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};
  1658 
  1659   val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
  1660     @{thms diff_conv_add_uminus add_0_left add_0_right ac_simps})
  1661 )
  1662 \<close>
  1663 
  1664 simproc_setup cancel_div_mod_int ("(a::'a::semidom_modulo) + b") =
  1665   \<open>K Cancel_Div_Mod_Ring.proc\<close>
  1666 
  1667 class idom_modulo = idom + semidom_modulo
  1668 begin
  1669 
  1670 subclass idom_divide ..
  1671 
  1672 lemma div_diff [simp]:
  1673   "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> (a - b) div c = a div c - b div c"
  1674   using div_add [of _  _ "- b"] by (simp add: dvd_neg_div)
  1675 
  1676 end
  1677 
  1678 
  1679 class ordered_semiring = semiring + ordered_comm_monoid_add +
  1680   assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
  1681   assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"
  1682 begin
  1683 
  1684 lemma mult_mono: "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * d"
  1685   apply (erule (1) mult_right_mono [THEN order_trans])
  1686   apply (erule (1) mult_left_mono)
  1687   done
  1688 
  1689 lemma mult_mono': "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * d"
  1690   by (rule mult_mono) (fast intro: order_trans)+
  1691 
  1692 end
  1693 
  1694 class ordered_semiring_0 = semiring_0 + ordered_semiring
  1695 begin
  1696 
  1697 lemma mult_nonneg_nonneg [simp]: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b"
  1698   using mult_left_mono [of 0 b a] by simp
  1699 
  1700 lemma mult_nonneg_nonpos: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> a * b \<le> 0"
  1701   using mult_left_mono [of b 0 a] by simp
  1702 
  1703 lemma mult_nonpos_nonneg: "a \<le> 0 \<Longrightarrow> 0 \<le> b \<Longrightarrow> a * b \<le> 0"
  1704   using mult_right_mono [of a 0 b] by simp
  1705 
  1706 text \<open>Legacy -- use @{thm [source] mult_nonpos_nonneg}.\<close>
  1707 lemma mult_nonneg_nonpos2: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> b * a \<le> 0"
  1708   by (drule mult_right_mono [of b 0]) auto
  1709 
  1710 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"
  1711   by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)
  1712 
  1713 end
  1714 
  1715 class ordered_cancel_semiring = ordered_semiring + cancel_comm_monoid_add
  1716 begin
  1717 
  1718 subclass semiring_0_cancel ..
  1719 
  1720 subclass ordered_semiring_0 ..
  1721 
  1722 end
  1723 
  1724 class linordered_semiring = ordered_semiring + linordered_cancel_ab_semigroup_add
  1725 begin
  1726 
  1727 subclass ordered_cancel_semiring ..
  1728 
  1729 subclass ordered_cancel_comm_monoid_add ..
  1730 
  1731 subclass ordered_ab_semigroup_monoid_add_imp_le ..
  1732 
  1733 lemma mult_left_less_imp_less: "c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
  1734   by (force simp add: mult_left_mono not_le [symmetric])
  1735 
  1736 lemma mult_right_less_imp_less: "a * c < b * c \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
  1737   by (force simp add: mult_right_mono not_le [symmetric])
  1738 
  1739 end
  1740 
  1741 class zero_less_one = order + zero + one +
  1742   assumes zero_less_one [simp]: "0 < 1"
  1743 
  1744 class linordered_semiring_1 = linordered_semiring + semiring_1 + zero_less_one
  1745 begin
  1746 
  1747 lemma convex_bound_le:
  1748   assumes "x \<le> a" "y \<le> a" "0 \<le> u" "0 \<le> v" "u + v = 1"
  1749   shows "u * x + v * y \<le> a"
  1750 proof-
  1751   from assms have "u * x + v * y \<le> u * a + v * a"
  1752     by (simp add: add_mono mult_left_mono)
  1753   with assms show ?thesis
  1754     unfolding distrib_right[symmetric] by simp
  1755 qed
  1756 
  1757 end
  1758 
  1759 class linordered_semiring_strict = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add +
  1760   assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
  1761   assumes mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c"
  1762 begin
  1763 
  1764 subclass semiring_0_cancel ..
  1765 
  1766 subclass linordered_semiring
  1767 proof
  1768   fix a b c :: 'a
  1769   assume *: "a \<le> b" "0 \<le> c"
  1770   then show "c * a \<le> c * b"
  1771     unfolding le_less
  1772     using mult_strict_left_mono by (cases "c = 0") auto
  1773   from * show "a * c \<le> b * c"
  1774     unfolding le_less
  1775     using mult_strict_right_mono by (cases "c = 0") auto
  1776 qed
  1777 
  1778 lemma mult_left_le_imp_le: "c * a \<le> c * b \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
  1779   by (auto simp add: mult_strict_left_mono _not_less [symmetric])
  1780 
  1781 lemma mult_right_le_imp_le: "a * c \<le> b * c \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
  1782   by (auto simp add: mult_strict_right_mono not_less [symmetric])
  1783 
  1784 lemma mult_pos_pos[simp]: "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a * b"
  1785   using mult_strict_left_mono [of 0 b a] by simp
  1786 
  1787 lemma mult_pos_neg: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> a * b < 0"
  1788   using mult_strict_left_mono [of b 0 a] by simp
  1789 
  1790 lemma mult_neg_pos: "a < 0 \<Longrightarrow> 0 < b \<Longrightarrow> a * b < 0"
  1791   using mult_strict_right_mono [of a 0 b] by simp
  1792 
  1793 text \<open>Legacy -- use @{thm [source] mult_neg_pos}.\<close>
  1794 lemma mult_pos_neg2: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> b * a < 0"
  1795   by (drule mult_strict_right_mono [of b 0]) auto
  1796 
  1797 lemma zero_less_mult_pos: "0 < a * b \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"
  1798   apply (cases "b \<le> 0")
  1799    apply (auto simp add: le_less not_less)
  1800   apply (drule_tac mult_pos_neg [of a b])
  1801    apply (auto dest: less_not_sym)
  1802   done
  1803 
  1804 lemma zero_less_mult_pos2: "0 < b * a \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"
  1805   apply (cases "b \<le> 0")
  1806    apply (auto simp add: le_less not_less)
  1807   apply (drule_tac mult_pos_neg2 [of a b])
  1808    apply (auto dest: less_not_sym)
  1809   done
  1810 
  1811 text \<open>Strict monotonicity in both arguments\<close>
  1812 lemma mult_strict_mono:
  1813   assumes "a < b" and "c < d" and "0 < b" and "0 \<le> c"
  1814   shows "a * c < b * d"
  1815   using assms
  1816   apply (cases "c = 0")
  1817    apply simp
  1818   apply (erule mult_strict_right_mono [THEN less_trans])
  1819    apply (auto simp add: le_less)
  1820   apply (erule (1) mult_strict_left_mono)
  1821   done
  1822 
  1823 text \<open>This weaker variant has more natural premises\<close>
  1824 lemma mult_strict_mono':
  1825   assumes "a < b" and "c < d" and "0 \<le> a" and "0 \<le> c"
  1826   shows "a * c < b * d"
  1827   by (rule mult_strict_mono) (insert assms, auto)
  1828 
  1829 lemma mult_less_le_imp_less:
  1830   assumes "a < b" and "c \<le> d" and "0 \<le> a" and "0 < c"
  1831   shows "a * c < b * d"
  1832   using assms
  1833   apply (subgoal_tac "a * c < b * c")
  1834    apply (erule less_le_trans)
  1835    apply (erule mult_left_mono)
  1836    apply simp
  1837   apply (erule (1) mult_strict_right_mono)
  1838   done
  1839 
  1840 lemma mult_le_less_imp_less:
  1841   assumes "a \<le> b" and "c < d" and "0 < a" and "0 \<le> c"
  1842   shows "a * c < b * d"
  1843   using assms
  1844   apply (subgoal_tac "a * c \<le> b * c")
  1845    apply (erule le_less_trans)
  1846    apply (erule mult_strict_left_mono)
  1847    apply simp
  1848   apply (erule (1) mult_right_mono)
  1849   done
  1850 
  1851 end
  1852 
  1853 class linordered_semiring_1_strict = linordered_semiring_strict + semiring_1 + zero_less_one
  1854 begin
  1855 
  1856 subclass linordered_semiring_1 ..
  1857 
  1858 lemma convex_bound_lt:
  1859   assumes "x < a" "y < a" "0 \<le> u" "0 \<le> v" "u + v = 1"
  1860   shows "u * x + v * y < a"
  1861 proof -
  1862   from assms have "u * x + v * y < u * a + v * a"
  1863     by (cases "u = 0") (auto intro!: add_less_le_mono mult_strict_left_mono mult_left_mono)
  1864   with assms show ?thesis
  1865     unfolding distrib_right[symmetric] by simp
  1866 qed
  1867 
  1868 end
  1869 
  1870 class ordered_comm_semiring = comm_semiring_0 + ordered_ab_semigroup_add +
  1871   assumes comm_mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
  1872 begin
  1873 
  1874 subclass ordered_semiring
  1875 proof
  1876   fix a b c :: 'a
  1877   assume "a \<le> b" "0 \<le> c"
  1878   then show "c * a \<le> c * b" by (rule comm_mult_left_mono)
  1879   then show "a * c \<le> b * c" by (simp only: mult.commute)
  1880 qed
  1881 
  1882 end
  1883 
  1884 class ordered_cancel_comm_semiring = ordered_comm_semiring + cancel_comm_monoid_add
  1885 begin
  1886 
  1887 subclass comm_semiring_0_cancel ..
  1888 subclass ordered_comm_semiring ..
  1889 subclass ordered_cancel_semiring ..
  1890 
  1891 end
  1892 
  1893 class linordered_comm_semiring_strict = comm_semiring_0 + linordered_cancel_ab_semigroup_add +
  1894   assumes comm_mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
  1895 begin
  1896 
  1897 subclass linordered_semiring_strict
  1898 proof
  1899   fix a b c :: 'a
  1900   assume "a < b" "0 < c"
  1901   then show "c * a < c * b"
  1902     by (rule comm_mult_strict_left_mono)
  1903   then show "a * c < b * c"
  1904     by (simp only: mult.commute)
  1905 qed
  1906 
  1907 subclass ordered_cancel_comm_semiring
  1908 proof
  1909   fix a b c :: 'a
  1910   assume "a \<le> b" "0 \<le> c"
  1911   then show "c * a \<le> c * b"
  1912     unfolding le_less
  1913     using mult_strict_left_mono by (cases "c = 0") auto
  1914 qed
  1915 
  1916 end
  1917 
  1918 class ordered_ring = ring + ordered_cancel_semiring
  1919 begin
  1920 
  1921 subclass ordered_ab_group_add ..
  1922 
  1923 lemma less_add_iff1: "a * e + c < b * e + d \<longleftrightarrow> (a - b) * e + c < d"
  1924   by (simp add: algebra_simps)
  1925 
  1926 lemma less_add_iff2: "a * e + c < b * e + d \<longleftrightarrow> c < (b - a) * e + d"
  1927   by (simp add: algebra_simps)
  1928 
  1929 lemma le_add_iff1: "a * e + c \<le> b * e + d \<longleftrightarrow> (a - b) * e + c \<le> d"
  1930   by (simp add: algebra_simps)
  1931 
  1932 lemma le_add_iff2: "a * e + c \<le> b * e + d \<longleftrightarrow> c \<le> (b - a) * e + d"
  1933   by (simp add: algebra_simps)
  1934 
  1935 lemma mult_left_mono_neg: "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> c * a \<le> c * b"
  1936   apply (drule mult_left_mono [of _ _ "- c"])
  1937   apply simp_all
  1938   done
  1939 
  1940 lemma mult_right_mono_neg: "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> a * c \<le> b * c"
  1941   apply (drule mult_right_mono [of _ _ "- c"])
  1942   apply simp_all
  1943   done
  1944 
  1945 lemma mult_nonpos_nonpos: "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> 0 \<le> a * b"
  1946   using mult_right_mono_neg [of a 0 b] by simp
  1947 
  1948 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"
  1949   by (auto simp add: mult_nonpos_nonpos)
  1950 
  1951 end
  1952 
  1953 class abs_if = minus + uminus + ord + zero + abs +
  1954   assumes abs_if: "\<bar>a\<bar> = (if a < 0 then - a else a)"
  1955 
  1956 class linordered_ring = ring + linordered_semiring + linordered_ab_group_add + abs_if
  1957 begin
  1958 
  1959 subclass ordered_ring ..
  1960 
  1961 subclass ordered_ab_group_add_abs
  1962 proof
  1963   fix a b
  1964   show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
  1965     by (auto simp add: abs_if not_le not_less algebra_simps
  1966         simp del: add.commute dest: add_neg_neg add_nonneg_nonneg)
  1967 qed (auto simp: abs_if)
  1968 
  1969 lemma zero_le_square [simp]: "0 \<le> a * a"
  1970   using linear [of 0 a] by (auto simp add: mult_nonpos_nonpos)
  1971 
  1972 lemma not_square_less_zero [simp]: "\<not> (a * a < 0)"
  1973   by (simp add: not_less)
  1974 
  1975 proposition abs_eq_iff: "\<bar>x\<bar> = \<bar>y\<bar> \<longleftrightarrow> x = y \<or> x = -y"
  1976   by (auto simp add: abs_if split: if_split_asm)
  1977 
  1978 lemma abs_eq_iff':
  1979   "\<bar>a\<bar> = b \<longleftrightarrow> b \<ge> 0 \<and> (a = b \<or> a = - b)"
  1980   by (cases "a \<ge> 0") auto
  1981 
  1982 lemma eq_abs_iff':
  1983   "a = \<bar>b\<bar> \<longleftrightarrow> a \<ge> 0 \<and> (b = a \<or> b = - a)"
  1984   using abs_eq_iff' [of b a] by auto
  1985 
  1986 lemma sum_squares_ge_zero: "0 \<le> x * x + y * y"
  1987   by (intro add_nonneg_nonneg zero_le_square)
  1988 
  1989 lemma not_sum_squares_lt_zero: "\<not> x * x + y * y < 0"
  1990   by (simp add: not_less sum_squares_ge_zero)
  1991 
  1992 end
  1993 
  1994 class linordered_ring_strict = ring + linordered_semiring_strict
  1995   + ordered_ab_group_add + abs_if
  1996 begin
  1997 
  1998 subclass linordered_ring ..
  1999 
  2000 lemma mult_strict_left_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> c * a < c * b"
  2001   using mult_strict_left_mono [of b a "- c"] by simp
  2002 
  2003 lemma mult_strict_right_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> a * c < b * c"
  2004   using mult_strict_right_mono [of b a "- c"] by simp
  2005 
  2006 lemma mult_neg_neg: "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> 0 < a * b"
  2007   using mult_strict_right_mono_neg [of a 0 b] by simp
  2008 
  2009 subclass ring_no_zero_divisors
  2010 proof
  2011   fix a b
  2012   assume "a \<noteq> 0"
  2013   then have a: "a < 0 \<or> 0 < a" by (simp add: neq_iff)
  2014   assume "b \<noteq> 0"
  2015   then have b: "b < 0 \<or> 0 < b" by (simp add: neq_iff)
  2016   have "a * b < 0 \<or> 0 < a * b"
  2017   proof (cases "a < 0")
  2018     case True
  2019     show ?thesis
  2020     proof (cases "b < 0")
  2021       case True
  2022       with \<open>a < 0\<close> show ?thesis by (auto dest: mult_neg_neg)
  2023     next
  2024       case False
  2025       with b have "0 < b" by auto
  2026       with \<open>a < 0\<close> show ?thesis by (auto dest: mult_strict_right_mono)
  2027     qed
  2028   next
  2029     case False
  2030     with a have "0 < a" by auto
  2031     show ?thesis
  2032     proof (cases "b < 0")
  2033       case True
  2034       with \<open>0 < a\<close> show ?thesis
  2035         by (auto dest: mult_strict_right_mono_neg)
  2036     next
  2037       case False
  2038       with b have "0 < b" by auto
  2039       with \<open>0 < a\<close> show ?thesis by auto
  2040     qed
  2041   qed
  2042   then show "a * b \<noteq> 0"
  2043     by (simp add: neq_iff)
  2044 qed
  2045 
  2046 lemma zero_less_mult_iff: "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0"
  2047   by (cases a 0 b 0 rule: linorder_cases[case_product linorder_cases])
  2048      (auto simp add: mult_neg_neg not_less le_less dest: zero_less_mult_pos zero_less_mult_pos2)
  2049 
  2050 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"
  2051   by (auto simp add: eq_commute [of 0] le_less not_less zero_less_mult_iff)
  2052 
  2053 lemma mult_less_0_iff: "a * b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b"
  2054   using zero_less_mult_iff [of "- a" b] by auto
  2055 
  2056 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"
  2057   using zero_le_mult_iff [of "- a" b] by auto
  2058 
  2059 text \<open>
  2060   Cancellation laws for @{term "c * a < c * b"} and @{term "a * c < b * c"},
  2061   also with the relations \<open>\<le>\<close> and equality.
  2062 \<close>
  2063 
  2064 text \<open>
  2065   These ``disjunction'' versions produce two cases when the comparison is
  2066   an assumption, but effectively four when the comparison is a goal.
  2067 \<close>
  2068 
  2069 lemma mult_less_cancel_right_disj: "a * c < b * c \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"
  2070   apply (cases "c = 0")
  2071    apply (auto simp add: neq_iff mult_strict_right_mono mult_strict_right_mono_neg)
  2072      apply (auto simp add: not_less not_le [symmetric, of "a*c"] not_le [symmetric, of a])
  2073      apply (erule_tac [!] notE)
  2074      apply (auto simp add: less_imp_le mult_right_mono mult_right_mono_neg)
  2075   done
  2076 
  2077 lemma mult_less_cancel_left_disj: "c * a < c * b \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"
  2078   apply (cases "c = 0")
  2079    apply (auto simp add: neq_iff mult_strict_left_mono mult_strict_left_mono_neg)
  2080      apply (auto simp add: not_less not_le [symmetric, of "c * a"] not_le [symmetric, of a])
  2081      apply (erule_tac [!] notE)
  2082      apply (auto simp add: less_imp_le mult_left_mono mult_left_mono_neg)
  2083   done
  2084 
  2085 text \<open>
  2086   The ``conjunction of implication'' lemmas produce two cases when the
  2087   comparison is a goal, but give four when the comparison is an assumption.
  2088 \<close>
  2089 
  2090 lemma mult_less_cancel_right: "a * c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)"
  2091   using mult_less_cancel_right_disj [of a c b] by auto
  2092 
  2093 lemma mult_less_cancel_left: "c * a < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)"
  2094   using mult_less_cancel_left_disj [of c a b] by auto
  2095 
  2096 lemma mult_le_cancel_right: "a * c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
  2097   by (simp add: not_less [symmetric] mult_less_cancel_right_disj)
  2098 
  2099 lemma mult_le_cancel_left: "c * a \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
  2100   by (simp add: not_less [symmetric] mult_less_cancel_left_disj)
  2101 
  2102 lemma mult_le_cancel_left_pos: "0 < c \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> a \<le> b"
  2103   by (auto simp: mult_le_cancel_left)
  2104 
  2105 lemma mult_le_cancel_left_neg: "c < 0 \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> b \<le> a"
  2106   by (auto simp: mult_le_cancel_left)
  2107 
  2108 lemma mult_less_cancel_left_pos: "0 < c \<Longrightarrow> c * a < c * b \<longleftrightarrow> a < b"
  2109   by (auto simp: mult_less_cancel_left)
  2110 
  2111 lemma mult_less_cancel_left_neg: "c < 0 \<Longrightarrow> c * a < c * b \<longleftrightarrow> b < a"
  2112   by (auto simp: mult_less_cancel_left)
  2113 
  2114 end
  2115 
  2116 lemmas mult_sign_intros =
  2117   mult_nonneg_nonneg mult_nonneg_nonpos
  2118   mult_nonpos_nonneg mult_nonpos_nonpos
  2119   mult_pos_pos mult_pos_neg
  2120   mult_neg_pos mult_neg_neg
  2121 
  2122 class ordered_comm_ring = comm_ring + ordered_comm_semiring
  2123 begin
  2124 
  2125 subclass ordered_ring ..
  2126 subclass ordered_cancel_comm_semiring ..
  2127 
  2128 end
  2129 
  2130 class linordered_nonzero_semiring = ordered_comm_semiring + monoid_mult + linorder + zero_less_one
  2131 begin
  2132 
  2133 subclass zero_neq_one
  2134   by standard (insert zero_less_one, blast)
  2135 
  2136 subclass comm_semiring_1
  2137   by standard (rule mult_1_left)
  2138 
  2139 lemma zero_le_one [simp]: "0 \<le> 1"
  2140   by (rule zero_less_one [THEN less_imp_le])
  2141 
  2142 lemma not_one_le_zero [simp]: "\<not> 1 \<le> 0"
  2143   by (simp add: not_le)
  2144 
  2145 lemma not_one_less_zero [simp]: "\<not> 1 < 0"
  2146   by (simp add: not_less)
  2147 
  2148 lemma mult_left_le: "c \<le> 1 \<Longrightarrow> 0 \<le> a \<Longrightarrow> a * c \<le> a"
  2149   using mult_left_mono[of c 1 a] by simp
  2150 
  2151 lemma mult_le_one: "a \<le> 1 \<Longrightarrow> 0 \<le> b \<Longrightarrow> b \<le> 1 \<Longrightarrow> a * b \<le> 1"
  2152   using mult_mono[of a 1 b 1] by simp
  2153 
  2154 lemma zero_less_two: "0 < 1 + 1"
  2155   using add_pos_pos[OF zero_less_one zero_less_one] .
  2156 
  2157 end
  2158 
  2159 class linordered_semidom = semidom + linordered_comm_semiring_strict + zero_less_one +
  2160   assumes le_add_diff_inverse2 [simp]: "b \<le> a \<Longrightarrow> a - b + b = a"
  2161 begin
  2162 
  2163 subclass linordered_nonzero_semiring ..
  2164 
  2165 text \<open>Addition is the inverse of subtraction.\<close>
  2166 
  2167 lemma le_add_diff_inverse [simp]: "b \<le> a \<Longrightarrow> b + (a - b) = a"
  2168   by (frule le_add_diff_inverse2) (simp add: add.commute)
  2169 
  2170 lemma add_diff_inverse: "\<not> a < b \<Longrightarrow> b + (a - b) = a"
  2171   by simp
  2172 
  2173 lemma add_le_imp_le_diff: "i + k \<le> n \<Longrightarrow> i \<le> n - k"
  2174   apply (subst add_le_cancel_right [where c=k, symmetric])
  2175   apply (frule le_add_diff_inverse2)
  2176   apply (simp only: add.assoc [symmetric])
  2177   using add_implies_diff
  2178   apply fastforce
  2179   done
  2180 
  2181 lemma add_le_add_imp_diff_le:
  2182   assumes 1: "i + k \<le> n"
  2183     and 2: "n \<le> j + k"
  2184   shows "i + k \<le> n \<Longrightarrow> n \<le> j + k \<Longrightarrow> n - k \<le> j"
  2185 proof -
  2186   have "n - (i + k) + (i + k) = n"
  2187     using 1 by simp
  2188   moreover have "n - k = n - k - i + i"
  2189     using 1 by (simp add: add_le_imp_le_diff)
  2190   ultimately show ?thesis
  2191     using 2
  2192     apply (simp add: add.assoc [symmetric])
  2193     apply (rule add_le_imp_le_diff [of _ k "j + k", simplified add_diff_cancel_right'])
  2194     apply (simp add: add.commute diff_diff_add)
  2195     done
  2196 qed
  2197 
  2198 lemma less_1_mult: "1 < m \<Longrightarrow> 1 < n \<Longrightarrow> 1 < m * n"
  2199   using mult_strict_mono [of 1 m 1 n] by (simp add: less_trans [OF zero_less_one])
  2200 
  2201 end
  2202 
  2203 class linordered_idom = comm_ring_1 + linordered_comm_semiring_strict +
  2204   ordered_ab_group_add + abs_if + sgn +
  2205   assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
  2206 begin
  2207 
  2208 subclass linordered_ring_strict ..
  2209 
  2210 subclass linordered_semiring_1_strict
  2211 proof
  2212   have "0 \<le> 1 * 1"
  2213     by (fact zero_le_square)
  2214   then show "0 < 1" 
  2215     by (simp add: le_less)
  2216 qed
  2217 
  2218 subclass ordered_comm_ring ..
  2219 subclass idom ..
  2220 
  2221 subclass linordered_semidom
  2222   by standard simp
  2223 
  2224 subclass idom_abs_sgn
  2225   by standard
  2226     (auto simp add: sgn_if abs_if zero_less_mult_iff)
  2227 
  2228 lemma linorder_neqE_linordered_idom:
  2229   assumes "x \<noteq> y"
  2230   obtains "x < y" | "y < x"
  2231   using assms by (rule neqE)
  2232 
  2233 text \<open>These cancellation simp rules also produce two cases when the comparison is a goal.\<close>
  2234 
  2235 lemma mult_le_cancel_right1: "c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)"
  2236   using mult_le_cancel_right [of 1 c b] by simp
  2237 
  2238 lemma mult_le_cancel_right2: "a * c \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)"
  2239   using mult_le_cancel_right [of a c 1] by simp
  2240 
  2241 lemma mult_le_cancel_left1: "c \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)"
  2242   using mult_le_cancel_left [of c 1 b] by simp
  2243 
  2244 lemma mult_le_cancel_left2: "c * a \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)"
  2245   using mult_le_cancel_left [of c a 1] by simp
  2246 
  2247 lemma mult_less_cancel_right1: "c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)"
  2248   using mult_less_cancel_right [of 1 c b] by simp
  2249 
  2250 lemma mult_less_cancel_right2: "a * c < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"
  2251   using mult_less_cancel_right [of a c 1] by simp
  2252 
  2253 lemma mult_less_cancel_left1: "c < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)"
  2254   using mult_less_cancel_left [of c 1 b] by simp
  2255 
  2256 lemma mult_less_cancel_left2: "c * a < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"
  2257   using mult_less_cancel_left [of c a 1] by simp
  2258 
  2259 lemma sgn_0_0: "sgn a = 0 \<longleftrightarrow> a = 0"
  2260   by (fact sgn_eq_0_iff)
  2261 
  2262 lemma sgn_1_pos: "sgn a = 1 \<longleftrightarrow> a > 0"
  2263   unfolding sgn_if by simp
  2264 
  2265 lemma sgn_1_neg: "sgn a = - 1 \<longleftrightarrow> a < 0"
  2266   unfolding sgn_if by auto
  2267 
  2268 lemma sgn_pos [simp]: "0 < a \<Longrightarrow> sgn a = 1"
  2269   by (simp only: sgn_1_pos)
  2270 
  2271 lemma sgn_neg [simp]: "a < 0 \<Longrightarrow> sgn a = - 1"
  2272   by (simp only: sgn_1_neg)
  2273 
  2274 lemma abs_sgn: "\<bar>k\<bar> = k * sgn k"
  2275   unfolding sgn_if abs_if by auto
  2276 
  2277 lemma sgn_greater [simp]: "0 < sgn a \<longleftrightarrow> 0 < a"
  2278   unfolding sgn_if by auto
  2279 
  2280 lemma sgn_less [simp]: "sgn a < 0 \<longleftrightarrow> a < 0"
  2281   unfolding sgn_if by auto
  2282 
  2283 lemma abs_sgn_eq_1 [simp]:
  2284   "a \<noteq> 0 \<Longrightarrow> \<bar>sgn a\<bar> = 1"
  2285   by simp
  2286 
  2287 lemma abs_sgn_eq: "\<bar>sgn a\<bar> = (if a = 0 then 0 else 1)"
  2288   by (simp add: sgn_if)
  2289 
  2290 lemma sgn_mult_self_eq [simp]:
  2291   "sgn a * sgn a = of_bool (a \<noteq> 0)"
  2292   by (cases "a > 0") simp_all
  2293 
  2294 lemma abs_mult_self_eq [simp]:
  2295   "\<bar>a\<bar> * \<bar>a\<bar> = a * a"
  2296   by (cases "a > 0") simp_all
  2297 
  2298 lemma same_sgn_sgn_add:
  2299   "sgn (a + b) = sgn a" if "sgn b = sgn a"
  2300 proof (cases a 0 rule: linorder_cases)
  2301   case equal
  2302   with that show ?thesis
  2303     by simp
  2304 next
  2305   case less
  2306   with that have "b < 0"
  2307     by (simp add: sgn_1_neg)
  2308   with \<open>a < 0\<close> have "a + b < 0"
  2309     by (rule add_neg_neg)
  2310   with \<open>a < 0\<close> show ?thesis
  2311     by simp
  2312 next
  2313   case greater
  2314   with that have "b > 0"
  2315     by (simp add: sgn_1_pos)
  2316   with \<open>a > 0\<close> have "a + b > 0"
  2317     by (rule add_pos_pos)
  2318   with \<open>a > 0\<close> show ?thesis
  2319     by simp
  2320 qed
  2321 
  2322 lemma same_sgn_abs_add:
  2323   "\<bar>a + b\<bar> = \<bar>a\<bar> + \<bar>b\<bar>" if "sgn b = sgn a"
  2324 proof -
  2325   have "a + b = sgn a * \<bar>a\<bar> + sgn b * \<bar>b\<bar>"
  2326     by (simp add: sgn_mult_abs)
  2327   also have "\<dots> = sgn a * (\<bar>a\<bar> + \<bar>b\<bar>)"
  2328     using that by (simp add: algebra_simps)
  2329   finally show ?thesis
  2330     by (auto simp add: abs_mult)
  2331 qed
  2332 
  2333 lemma sgn_not_eq_imp:
  2334   "sgn a = - sgn b" if "sgn b \<noteq> sgn a" and "sgn a \<noteq> 0" and "sgn b \<noteq> 0"
  2335   using that by (cases "a < 0") (auto simp add: sgn_0_0 sgn_1_pos sgn_1_neg)
  2336 
  2337 lemma abs_dvd_iff [simp]: "\<bar>m\<bar> dvd k \<longleftrightarrow> m dvd k"
  2338   by (simp add: abs_if)
  2339 
  2340 lemma dvd_abs_iff [simp]: "m dvd \<bar>k\<bar> \<longleftrightarrow> m dvd k"
  2341   by (simp add: abs_if)
  2342 
  2343 lemma dvd_if_abs_eq: "\<bar>l\<bar> = \<bar>k\<bar> \<Longrightarrow> l dvd k"
  2344   by (subst abs_dvd_iff [symmetric]) simp
  2345 
  2346 text \<open>
  2347   The following lemmas can be proven in more general structures, but
  2348   are dangerous as simp rules in absence of @{thm neg_equal_zero},
  2349   @{thm neg_less_pos}, @{thm neg_less_eq_nonneg}.
  2350 \<close>
  2351 
  2352 lemma equation_minus_iff_1 [simp, no_atp]: "1 = - a \<longleftrightarrow> a = - 1"
  2353   by (fact equation_minus_iff)
  2354 
  2355 lemma minus_equation_iff_1 [simp, no_atp]: "- a = 1 \<longleftrightarrow> a = - 1"
  2356   by (subst minus_equation_iff, auto)
  2357 
  2358 lemma le_minus_iff_1 [simp, no_atp]: "1 \<le> - b \<longleftrightarrow> b \<le> - 1"
  2359   by (fact le_minus_iff)
  2360 
  2361 lemma minus_le_iff_1 [simp, no_atp]: "- a \<le> 1 \<longleftrightarrow> - 1 \<le> a"
  2362   by (fact minus_le_iff)
  2363 
  2364 lemma less_minus_iff_1 [simp, no_atp]: "1 < - b \<longleftrightarrow> b < - 1"
  2365   by (fact less_minus_iff)
  2366 
  2367 lemma minus_less_iff_1 [simp, no_atp]: "- a < 1 \<longleftrightarrow> - 1 < a"
  2368   by (fact minus_less_iff)
  2369 
  2370 lemma add_less_zeroD:
  2371   shows "x+y < 0 \<Longrightarrow> x<0 \<or> y<0"
  2372   by (auto simp: not_less intro: le_less_trans [of _ "x+y"])
  2373 
  2374 end
  2375 
  2376 text \<open>Simprules for comparisons where common factors can be cancelled.\<close>
  2377 
  2378 lemmas mult_compare_simps =
  2379   mult_le_cancel_right mult_le_cancel_left
  2380   mult_le_cancel_right1 mult_le_cancel_right2
  2381   mult_le_cancel_left1 mult_le_cancel_left2
  2382   mult_less_cancel_right mult_less_cancel_left
  2383   mult_less_cancel_right1 mult_less_cancel_right2
  2384   mult_less_cancel_left1 mult_less_cancel_left2
  2385   mult_cancel_right mult_cancel_left
  2386   mult_cancel_right1 mult_cancel_right2
  2387   mult_cancel_left1 mult_cancel_left2
  2388 
  2389 
  2390 text \<open>Reasoning about inequalities with division\<close>
  2391 
  2392 context linordered_semidom
  2393 begin
  2394 
  2395 lemma less_add_one: "a < a + 1"
  2396 proof -
  2397   have "a + 0 < a + 1"
  2398     by (blast intro: zero_less_one add_strict_left_mono)
  2399   then show ?thesis by simp
  2400 qed
  2401 
  2402 end
  2403 
  2404 context linordered_idom
  2405 begin
  2406 
  2407 lemma mult_right_le_one_le: "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> x * y \<le> x"
  2408   by (rule mult_left_le)
  2409 
  2410 lemma mult_left_le_one_le: "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> y * x \<le> x"
  2411   by (auto simp add: mult_le_cancel_right2)
  2412 
  2413 end
  2414 
  2415 text \<open>Absolute Value\<close>
  2416 
  2417 context linordered_idom
  2418 begin
  2419 
  2420 lemma mult_sgn_abs: "sgn x * \<bar>x\<bar> = x"
  2421   by (fact sgn_mult_abs)
  2422 
  2423 lemma abs_one: "\<bar>1\<bar> = 1"
  2424   by (fact abs_1)
  2425 
  2426 end
  2427 
  2428 class ordered_ring_abs = ordered_ring + ordered_ab_group_add_abs +
  2429   assumes abs_eq_mult:
  2430     "(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>"
  2431 
  2432 context linordered_idom
  2433 begin
  2434 
  2435 subclass ordered_ring_abs
  2436   by standard (auto simp: abs_if not_less mult_less_0_iff)
  2437 
  2438 lemma abs_mult_self [simp]: "\<bar>a\<bar> * \<bar>a\<bar> = a * a"
  2439   by (simp add: abs_if)
  2440 
  2441 lemma abs_mult_less:
  2442   assumes ac: "\<bar>a\<bar> < c"
  2443     and bd: "\<bar>b\<bar> < d"
  2444   shows "\<bar>a\<bar> * \<bar>b\<bar> < c * d"
  2445 proof -
  2446   from ac have "0 < c"
  2447     by (blast intro: le_less_trans abs_ge_zero)
  2448   with bd show ?thesis by (simp add: ac mult_strict_mono)
  2449 qed
  2450 
  2451 lemma abs_less_iff: "\<bar>a\<bar> < b \<longleftrightarrow> a < b \<and> - a < b"
  2452   by (simp add: less_le abs_le_iff) (auto simp add: abs_if)
  2453 
  2454 lemma abs_mult_pos: "0 \<le> x \<Longrightarrow> \<bar>y\<bar> * x = \<bar>y * x\<bar>"
  2455   by (simp add: abs_mult)
  2456 
  2457 lemma abs_diff_less_iff: "\<bar>x - a\<bar> < r \<longleftrightarrow> a - r < x \<and> x < a + r"
  2458   by (auto simp add: diff_less_eq ac_simps abs_less_iff)
  2459 
  2460 lemma abs_diff_le_iff: "\<bar>x - a\<bar> \<le> r \<longleftrightarrow> a - r \<le> x \<and> x \<le> a + r"
  2461   by (auto simp add: diff_le_eq ac_simps abs_le_iff)
  2462 
  2463 lemma abs_add_one_gt_zero: "0 < 1 + \<bar>x\<bar>"
  2464   by (auto simp: abs_if not_less intro: zero_less_one add_strict_increasing less_trans)
  2465 
  2466 end
  2467 
  2468 subsection \<open>Dioids\<close>
  2469 
  2470 text \<open>
  2471   Dioids are the alternative extensions of semirings, a semiring can
  2472   either be a ring or a dioid but never both.
  2473 \<close>
  2474 
  2475 class dioid = semiring_1 + canonically_ordered_monoid_add
  2476 begin
  2477 
  2478 subclass ordered_semiring
  2479   by standard (auto simp: le_iff_add distrib_left distrib_right)
  2480 
  2481 end
  2482 
  2483 
  2484 hide_fact (open) comm_mult_left_mono comm_mult_strict_left_mono distrib
  2485 
  2486 code_identifier
  2487   code_module Rings \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
  2488 
  2489 end