src/HOL/Rings.thy
 author haftmann Wed Jul 08 20:19:12 2015 +0200 (2015-07-08) changeset 60690 a9e45c9588c3 parent 60688 01488b559910 child 60758 d8d85a8172b5 permissions -rw-r--r--
tuned facts
     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 {* Rings *}

    11

    12 theory Rings

    13 imports Groups

    14 begin

    15

    16 class semiring = ab_semigroup_add + semigroup_mult +

    17   assumes distrib_right[algebra_simps]: "(a + b) * c = a * c + b * c"

    18   assumes distrib_left[algebra_simps]: "a * (b + c) = a * b + a * c"

    19 begin

    20

    21 text{*For the @{text combine_numerals} simproc*}

    22 lemma combine_common_factor:

    23   "a * e + (b * e + c) = (a + b) * e + c"

    24 by (simp add: distrib_right ac_simps)

    25

    26 end

    27

    28 class mult_zero = times + zero +

    29   assumes mult_zero_left [simp]: "0 * a = 0"

    30   assumes mult_zero_right [simp]: "a * 0 = 0"

    31 begin

    32

    33 lemma mult_not_zero:

    34   "a * b \<noteq> 0 \<Longrightarrow> a \<noteq> 0 \<and> b \<noteq> 0"

    35   by auto

    36

    37 end

    38

    39 class semiring_0 = semiring + comm_monoid_add + mult_zero

    40

    41 class semiring_0_cancel = semiring + cancel_comm_monoid_add

    42 begin

    43

    44 subclass semiring_0

    45 proof

    46   fix a :: 'a

    47   have "0 * a + 0 * a = 0 * a + 0" by (simp add: distrib_right [symmetric])

    48   thus "0 * a = 0" by (simp only: add_left_cancel)

    49 next

    50   fix a :: 'a

    51   have "a * 0 + a * 0 = a * 0 + 0" by (simp add: distrib_left [symmetric])

    52   thus "a * 0 = 0" by (simp only: add_left_cancel)

    53 qed

    54

    55 end

    56

    57 class comm_semiring = ab_semigroup_add + ab_semigroup_mult +

    58   assumes distrib: "(a + b) * c = a * c + b * c"

    59 begin

    60

    61 subclass semiring

    62 proof

    63   fix a b c :: 'a

    64   show "(a + b) * c = a * c + b * c" by (simp add: distrib)

    65   have "a * (b + c) = (b + c) * a" by (simp add: ac_simps)

    66   also have "... = b * a + c * a" by (simp only: distrib)

    67   also have "... = a * b + a * c" by (simp add: ac_simps)

    68   finally show "a * (b + c) = a * b + a * c" by blast

    69 qed

    70

    71 end

    72

    73 class comm_semiring_0 = comm_semiring + comm_monoid_add + mult_zero

    74 begin

    75

    76 subclass semiring_0 ..

    77

    78 end

    79

    80 class comm_semiring_0_cancel = comm_semiring + cancel_comm_monoid_add

    81 begin

    82

    83 subclass semiring_0_cancel ..

    84

    85 subclass comm_semiring_0 ..

    86

    87 end

    88

    89 class zero_neq_one = zero + one +

    90   assumes zero_neq_one [simp]: "0 \<noteq> 1"

    91 begin

    92

    93 lemma one_neq_zero [simp]: "1 \<noteq> 0"

    94 by (rule not_sym) (rule zero_neq_one)

    95

    96 definition of_bool :: "bool \<Rightarrow> 'a"

    97 where

    98   "of_bool p = (if p then 1 else 0)"

    99

   100 lemma of_bool_eq [simp, code]:

   101   "of_bool False = 0"

   102   "of_bool True = 1"

   103   by (simp_all add: of_bool_def)

   104

   105 lemma of_bool_eq_iff:

   106   "of_bool p = of_bool q \<longleftrightarrow> p = q"

   107   by (simp add: of_bool_def)

   108

   109 lemma split_of_bool [split]:

   110   "P (of_bool p) \<longleftrightarrow> (p \<longrightarrow> P 1) \<and> (\<not> p \<longrightarrow> P 0)"

   111   by (cases p) simp_all

   112

   113 lemma split_of_bool_asm:

   114   "P (of_bool p) \<longleftrightarrow> \<not> (p \<and> \<not> P 1 \<or> \<not> p \<and> \<not> P 0)"

   115   by (cases p) simp_all

   116

   117 end

   118

   119 class semiring_1 = zero_neq_one + semiring_0 + monoid_mult

   120

   121 text {* Abstract divisibility *}

   122

   123 class dvd = times

   124 begin

   125

   126 definition dvd :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "dvd" 50) where

   127   "b dvd a \<longleftrightarrow> (\<exists>k. a = b * k)"

   128

   129 lemma dvdI [intro?]: "a = b * k \<Longrightarrow> b dvd a"

   130   unfolding dvd_def ..

   131

   132 lemma dvdE [elim?]: "b dvd a \<Longrightarrow> (\<And>k. a = b * k \<Longrightarrow> P) \<Longrightarrow> P"

   133   unfolding dvd_def by blast

   134

   135 end

   136

   137 context comm_monoid_mult

   138 begin

   139

   140 subclass dvd .

   141

   142 lemma dvd_refl [simp]:

   143   "a dvd a"

   144 proof

   145   show "a = a * 1" by simp

   146 qed

   147

   148 lemma dvd_trans:

   149   assumes "a dvd b" and "b dvd c"

   150   shows "a dvd c"

   151 proof -

   152   from assms obtain v where "b = a * v" by (auto elim!: dvdE)

   153   moreover from assms obtain w where "c = b * w" by (auto elim!: dvdE)

   154   ultimately have "c = a * (v * w)" by (simp add: mult.assoc)

   155   then show ?thesis ..

   156 qed

   157

   158 lemma one_dvd [simp]:

   159   "1 dvd a"

   160   by (auto intro!: dvdI)

   161

   162 lemma dvd_mult [simp]:

   163   "a dvd c \<Longrightarrow> a dvd (b * c)"

   164   by (auto intro!: mult.left_commute dvdI elim!: dvdE)

   165

   166 lemma dvd_mult2 [simp]:

   167   "a dvd b \<Longrightarrow> a dvd (b * c)"

   168   using dvd_mult [of a b c] by (simp add: ac_simps)

   169

   170 lemma dvd_triv_right [simp]:

   171   "a dvd b * a"

   172   by (rule dvd_mult) (rule dvd_refl)

   173

   174 lemma dvd_triv_left [simp]:

   175   "a dvd a * b"

   176   by (rule dvd_mult2) (rule dvd_refl)

   177

   178 lemma mult_dvd_mono:

   179   assumes "a dvd b"

   180     and "c dvd d"

   181   shows "a * c dvd b * d"

   182 proof -

   183   from a dvd b obtain b' where "b = a * b'" ..

   184   moreover from c dvd d obtain d' where "d = c * d'" ..

   185   ultimately have "b * d = (a * c) * (b' * d')" by (simp add: ac_simps)

   186   then show ?thesis ..

   187 qed

   188

   189 lemma dvd_mult_left:

   190   "a * b dvd c \<Longrightarrow> a dvd c"

   191   by (simp add: dvd_def mult.assoc) blast

   192

   193 lemma dvd_mult_right:

   194   "a * b dvd c \<Longrightarrow> b dvd c"

   195   using dvd_mult_left [of b a c] by (simp add: ac_simps)

   196

   197 end

   198

   199 class comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult

   200 begin

   201

   202 subclass semiring_1 ..

   203

   204 lemma dvd_0_left_iff [simp]:

   205   "0 dvd a \<longleftrightarrow> a = 0"

   206   by (auto intro: dvd_refl elim!: dvdE)

   207

   208 lemma dvd_0_right [iff]:

   209   "a dvd 0"

   210 proof

   211   show "0 = a * 0" by simp

   212 qed

   213

   214 lemma dvd_0_left:

   215   "0 dvd a \<Longrightarrow> a = 0"

   216   by simp

   217

   218 lemma dvd_add [simp]:

   219   assumes "a dvd b" and "a dvd c"

   220   shows "a dvd (b + c)"

   221 proof -

   222   from a dvd b obtain b' where "b = a * b'" ..

   223   moreover from a dvd c obtain c' where "c = a * c'" ..

   224   ultimately have "b + c = a * (b' + c')" by (simp add: distrib_left)

   225   then show ?thesis ..

   226 qed

   227

   228 end

   229

   230 class semiring_1_cancel = semiring + cancel_comm_monoid_add

   231   + zero_neq_one + monoid_mult

   232 begin

   233

   234 subclass semiring_0_cancel ..

   235

   236 subclass semiring_1 ..

   237

   238 end

   239

   240 class comm_semiring_1_cancel = comm_semiring + cancel_comm_monoid_add +

   241                                zero_neq_one + comm_monoid_mult +

   242   assumes right_diff_distrib' [algebra_simps]: "a * (b - c) = a * b - a * c"

   243 begin

   244

   245 subclass semiring_1_cancel ..

   246 subclass comm_semiring_0_cancel ..

   247 subclass comm_semiring_1 ..

   248

   249 lemma left_diff_distrib' [algebra_simps]:

   250   "(b - c) * a = b * a - c * a"

   251   by (simp add: algebra_simps)

   252

   253 lemma dvd_add_times_triv_left_iff [simp]:

   254   "a dvd c * a + b \<longleftrightarrow> a dvd b"

   255 proof -

   256   have "a dvd a * c + b \<longleftrightarrow> a dvd b" (is "?P \<longleftrightarrow> ?Q")

   257   proof

   258     assume ?Q then show ?P by simp

   259   next

   260     assume ?P

   261     then obtain d where "a * c + b = a * d" ..

   262     then have "a * c + b - a * c = a * d - a * c" by simp

   263     then have "b = a * d - a * c" by simp

   264     then have "b = a * (d - c)" by (simp add: algebra_simps)

   265     then show ?Q ..

   266   qed

   267   then show "a dvd c * a + b \<longleftrightarrow> a dvd b" by (simp add: ac_simps)

   268 qed

   269

   270 lemma dvd_add_times_triv_right_iff [simp]:

   271   "a dvd b + c * a \<longleftrightarrow> a dvd b"

   272   using dvd_add_times_triv_left_iff [of a c b] by (simp add: ac_simps)

   273

   274 lemma dvd_add_triv_left_iff [simp]:

   275   "a dvd a + b \<longleftrightarrow> a dvd b"

   276   using dvd_add_times_triv_left_iff [of a 1 b] by simp

   277

   278 lemma dvd_add_triv_right_iff [simp]:

   279   "a dvd b + a \<longleftrightarrow> a dvd b"

   280   using dvd_add_times_triv_right_iff [of a b 1] by simp

   281

   282 lemma dvd_add_right_iff:

   283   assumes "a dvd b"

   284   shows "a dvd b + c \<longleftrightarrow> a dvd c" (is "?P \<longleftrightarrow> ?Q")

   285 proof

   286   assume ?P then obtain d where "b + c = a * d" ..

   287   moreover from a dvd b obtain e where "b = a * e" ..

   288   ultimately have "a * e + c = a * d" by simp

   289   then have "a * e + c - a * e = a * d - a * e" by simp

   290   then have "c = a * d - a * e" by simp

   291   then have "c = a * (d - e)" by (simp add: algebra_simps)

   292   then show ?Q ..

   293 next

   294   assume ?Q with assms show ?P by simp

   295 qed

   296

   297 lemma dvd_add_left_iff:

   298   assumes "a dvd c"

   299   shows "a dvd b + c \<longleftrightarrow> a dvd b"

   300   using assms dvd_add_right_iff [of a c b] by (simp add: ac_simps)

   301

   302 end

   303

   304 class ring = semiring + ab_group_add

   305 begin

   306

   307 subclass semiring_0_cancel ..

   308

   309 text {* Distribution rules *}

   310

   311 lemma minus_mult_left: "- (a * b) = - a * b"

   312 by (rule minus_unique) (simp add: distrib_right [symmetric])

   313

   314 lemma minus_mult_right: "- (a * b) = a * - b"

   315 by (rule minus_unique) (simp add: distrib_left [symmetric])

   316

   317 text{*Extract signs from products*}

   318 lemmas mult_minus_left [simp] = minus_mult_left [symmetric]

   319 lemmas mult_minus_right [simp] = minus_mult_right [symmetric]

   320

   321 lemma minus_mult_minus [simp]: "- a * - b = a * b"

   322 by simp

   323

   324 lemma minus_mult_commute: "- a * b = a * - b"

   325 by simp

   326

   327 lemma right_diff_distrib [algebra_simps]:

   328   "a * (b - c) = a * b - a * c"

   329   using distrib_left [of a b "-c "] by simp

   330

   331 lemma left_diff_distrib [algebra_simps]:

   332   "(a - b) * c = a * c - b * c"

   333   using distrib_right [of a "- b" c] by simp

   334

   335 lemmas ring_distribs =

   336   distrib_left distrib_right left_diff_distrib right_diff_distrib

   337

   338 lemma eq_add_iff1:

   339   "a * e + c = b * e + d \<longleftrightarrow> (a - b) * e + c = d"

   340 by (simp add: algebra_simps)

   341

   342 lemma eq_add_iff2:

   343   "a * e + c = b * e + d \<longleftrightarrow> c = (b - a) * e + d"

   344 by (simp add: algebra_simps)

   345

   346 end

   347

   348 lemmas ring_distribs =

   349   distrib_left distrib_right left_diff_distrib right_diff_distrib

   350

   351 class comm_ring = comm_semiring + ab_group_add

   352 begin

   353

   354 subclass ring ..

   355 subclass comm_semiring_0_cancel ..

   356

   357 lemma square_diff_square_factored:

   358   "x * x - y * y = (x + y) * (x - y)"

   359   by (simp add: algebra_simps)

   360

   361 end

   362

   363 class ring_1 = ring + zero_neq_one + monoid_mult

   364 begin

   365

   366 subclass semiring_1_cancel ..

   367

   368 lemma square_diff_one_factored:

   369   "x * x - 1 = (x + 1) * (x - 1)"

   370   by (simp add: algebra_simps)

   371

   372 end

   373

   374 class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult

   375 begin

   376

   377 subclass ring_1 ..

   378 subclass comm_semiring_1_cancel

   379   by unfold_locales (simp add: algebra_simps)

   380

   381 lemma dvd_minus_iff [simp]: "x dvd - y \<longleftrightarrow> x dvd y"

   382 proof

   383   assume "x dvd - y"

   384   then have "x dvd - 1 * - y" by (rule dvd_mult)

   385   then show "x dvd y" by simp

   386 next

   387   assume "x dvd y"

   388   then have "x dvd - 1 * y" by (rule dvd_mult)

   389   then show "x dvd - y" by simp

   390 qed

   391

   392 lemma minus_dvd_iff [simp]: "- x dvd y \<longleftrightarrow> x dvd y"

   393 proof

   394   assume "- x dvd y"

   395   then obtain k where "y = - x * k" ..

   396   then have "y = x * - k" by simp

   397   then show "x dvd y" ..

   398 next

   399   assume "x dvd y"

   400   then obtain k where "y = x * k" ..

   401   then have "y = - x * - k" by simp

   402   then show "- x dvd y" ..

   403 qed

   404

   405 lemma dvd_diff [simp]:

   406   "x dvd y \<Longrightarrow> x dvd z \<Longrightarrow> x dvd (y - z)"

   407   using dvd_add [of x y "- z"] by simp

   408

   409 end

   410

   411 class semiring_no_zero_divisors = semiring_0 +

   412   assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"

   413 begin

   414

   415 lemma divisors_zero:

   416   assumes "a * b = 0"

   417   shows "a = 0 \<or> b = 0"

   418 proof (rule classical)

   419   assume "\<not> (a = 0 \<or> b = 0)"

   420   then have "a \<noteq> 0" and "b \<noteq> 0" by auto

   421   with no_zero_divisors have "a * b \<noteq> 0" by blast

   422   with assms show ?thesis by simp

   423 qed

   424

   425 lemma mult_eq_0_iff [simp]:

   426   shows "a * b = 0 \<longleftrightarrow> a = 0 \<or> b = 0"

   427 proof (cases "a = 0 \<or> b = 0")

   428   case False then have "a \<noteq> 0" and "b \<noteq> 0" by auto

   429     then show ?thesis using no_zero_divisors by simp

   430 next

   431   case True then show ?thesis by auto

   432 qed

   433

   434 end

   435

   436 class semiring_no_zero_divisors_cancel = semiring_no_zero_divisors +

   437   assumes mult_cancel_right [simp]: "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b"

   438     and mult_cancel_left [simp]: "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b"

   439 begin

   440

   441 lemma mult_left_cancel:

   442   "c \<noteq> 0 \<Longrightarrow> c * a = c * b \<longleftrightarrow> a = b"

   443   by simp

   444

   445 lemma mult_right_cancel:

   446   "c \<noteq> 0 \<Longrightarrow> a * c = b * c \<longleftrightarrow> a = b"

   447   by simp

   448

   449 end

   450

   451 class ring_no_zero_divisors = ring + semiring_no_zero_divisors

   452 begin

   453

   454 subclass semiring_no_zero_divisors_cancel

   455 proof

   456   fix a b c

   457   have "a * c = b * c \<longleftrightarrow> (a - b) * c = 0"

   458     by (simp add: algebra_simps)

   459   also have "\<dots> \<longleftrightarrow> c = 0 \<or> a = b"

   460     by auto

   461   finally show "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b" .

   462   have "c * a = c * b \<longleftrightarrow> c * (a - b) = 0"

   463     by (simp add: algebra_simps)

   464   also have "\<dots> \<longleftrightarrow> c = 0 \<or> a = b"

   465     by auto

   466   finally show "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b" .

   467 qed

   468

   469 end

   470

   471 class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors

   472 begin

   473

   474 lemma square_eq_1_iff:

   475   "x * x = 1 \<longleftrightarrow> x = 1 \<or> x = - 1"

   476 proof -

   477   have "(x - 1) * (x + 1) = x * x - 1"

   478     by (simp add: algebra_simps)

   479   hence "x * x = 1 \<longleftrightarrow> (x - 1) * (x + 1) = 0"

   480     by simp

   481   thus ?thesis

   482     by (simp add: eq_neg_iff_add_eq_0)

   483 qed

   484

   485 lemma mult_cancel_right1 [simp]:

   486   "c = b * c \<longleftrightarrow> c = 0 \<or> b = 1"

   487 by (insert mult_cancel_right [of 1 c b], force)

   488

   489 lemma mult_cancel_right2 [simp]:

   490   "a * c = c \<longleftrightarrow> c = 0 \<or> a = 1"

   491 by (insert mult_cancel_right [of a c 1], simp)

   492

   493 lemma mult_cancel_left1 [simp]:

   494   "c = c * b \<longleftrightarrow> c = 0 \<or> b = 1"

   495 by (insert mult_cancel_left [of c 1 b], force)

   496

   497 lemma mult_cancel_left2 [simp]:

   498   "c * a = c \<longleftrightarrow> c = 0 \<or> a = 1"

   499 by (insert mult_cancel_left [of c a 1], simp)

   500

   501 end

   502

   503 class semidom = comm_semiring_1_cancel + semiring_no_zero_divisors

   504

   505 class idom = comm_ring_1 + semiring_no_zero_divisors

   506 begin

   507

   508 subclass semidom ..

   509

   510 subclass ring_1_no_zero_divisors ..

   511

   512 lemma dvd_mult_cancel_right [simp]:

   513   "a * c dvd b * c \<longleftrightarrow> c = 0 \<or> a dvd b"

   514 proof -

   515   have "a * c dvd b * c \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)"

   516     unfolding dvd_def by (simp add: ac_simps)

   517   also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b"

   518     unfolding dvd_def by simp

   519   finally show ?thesis .

   520 qed

   521

   522 lemma dvd_mult_cancel_left [simp]:

   523   "c * a dvd c * b \<longleftrightarrow> c = 0 \<or> a dvd b"

   524 proof -

   525   have "c * a dvd c * b \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)"

   526     unfolding dvd_def by (simp add: ac_simps)

   527   also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b"

   528     unfolding dvd_def by simp

   529   finally show ?thesis .

   530 qed

   531

   532 lemma square_eq_iff: "a * a = b * b \<longleftrightarrow> a = b \<or> a = - b"

   533 proof

   534   assume "a * a = b * b"

   535   then have "(a - b) * (a + b) = 0"

   536     by (simp add: algebra_simps)

   537   then show "a = b \<or> a = - b"

   538     by (simp add: eq_neg_iff_add_eq_0)

   539 next

   540   assume "a = b \<or> a = - b"

   541   then show "a * a = b * b" by auto

   542 qed

   543

   544 end

   545

   546 text {*

   547   The theory of partially ordered rings is taken from the books:

   548   \begin{itemize}

   549   \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979

   550   \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963

   551   \end{itemize}

   552   Most of the used notions can also be looked up in

   553   \begin{itemize}

   554   \item @{url "http://www.mathworld.com"} by Eric Weisstein et. al.

   555   \item \emph{Algebra I} by van der Waerden, Springer.

   556   \end{itemize}

   557 *}

   558

   559 class divide =

   560   fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "div" 70)

   561

   562 setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a \<Rightarrow> 'a \<Rightarrow> 'a"}) *}

   563

   564 context semiring

   565 begin

   566

   567 lemma [field_simps]:

   568   shows distrib_left_NO_MATCH: "NO_MATCH (x div y) a \<Longrightarrow> a * (b + c) = a * b + a * c"

   569     and distrib_right_NO_MATCH: "NO_MATCH (x div y) c \<Longrightarrow> (a + b) * c = a * c + b * c"

   570   by (rule distrib_left distrib_right)+

   571

   572 end

   573

   574 context ring

   575 begin

   576

   577 lemma [field_simps]:

   578   shows left_diff_distrib_NO_MATCH: "NO_MATCH (x div y) c \<Longrightarrow> (a - b) * c = a * c - b * c"

   579     and right_diff_distrib_NO_MATCH: "NO_MATCH (x div y) a \<Longrightarrow> a * (b - c) = a * b - a * c"

   580   by (rule left_diff_distrib right_diff_distrib)+

   581

   582 end

   583

   584 setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a::divide \<Rightarrow> 'a \<Rightarrow> 'a"}) *}

   585

   586 class semidom_divide = semidom + divide +

   587   assumes nonzero_mult_divide_cancel_right [simp]: "b \<noteq> 0 \<Longrightarrow> (a * b) div b = a"

   588   assumes divide_zero [simp]: "a div 0 = 0"

   589 begin

   590

   591 lemma nonzero_mult_divide_cancel_left [simp]:

   592   "a \<noteq> 0 \<Longrightarrow> (a * b) div a = b"

   593   using nonzero_mult_divide_cancel_right [of a b] by (simp add: ac_simps)

   594

   595 subclass semiring_no_zero_divisors_cancel

   596 proof

   597   fix a b c

   598   { fix a b c

   599     show "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b"

   600     proof (cases "c = 0")

   601       case True then show ?thesis by simp

   602     next

   603       case False

   604       { assume "a * c = b * c"

   605         then have "a * c div c = b * c div c"

   606           by simp

   607         with False have "a = b"

   608           by simp

   609       } then show ?thesis by auto

   610     qed

   611   }

   612   from this [of a c b]

   613   show "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b"

   614     by (simp add: ac_simps)

   615 qed

   616

   617 lemma div_self [simp]:

   618   assumes "a \<noteq> 0"

   619   shows "a div a = 1"

   620   using assms nonzero_mult_divide_cancel_left [of a 1] by simp

   621

   622 lemma divide_zero_left [simp]:

   623   "0 div a = 0"

   624 proof (cases "a = 0")

   625   case True then show ?thesis by simp

   626 next

   627   case False then have "a * 0 div a = 0"

   628     by (rule nonzero_mult_divide_cancel_left)

   629   then show ?thesis by simp

   630 qed

   631

   632 lemma divide_1 [simp]:

   633   "a div 1 = a"

   634   using nonzero_mult_divide_cancel_left [of 1 a] by simp

   635

   636 lemma dvd_times_left_cancel_iff [simp]:

   637   assumes "a \<noteq> 0"

   638   shows "a * b dvd a * c \<longleftrightarrow> b dvd c" (is "?P \<longleftrightarrow> ?Q")

   639 proof

   640   assume ?P then obtain d where "a * c = a * b * d" ..

   641   with assms have "c = b * d" by (simp add: ac_simps)

   642   then show ?Q ..

   643 next

   644   assume ?Q then obtain d where "c = b * d" ..

   645   then have "a * c = a * b * d" by (simp add: ac_simps)

   646   then show ?P ..

   647 qed

   648

   649 lemma dvd_times_right_cancel_iff [simp]:

   650   assumes "a \<noteq> 0"

   651   shows "b * a dvd c * a \<longleftrightarrow> b dvd c" (is "?P \<longleftrightarrow> ?Q")

   652 using dvd_times_left_cancel_iff [of a b c] assms by (simp add: ac_simps)

   653

   654 lemma div_dvd_iff_mult:

   655   assumes "b \<noteq> 0" and "b dvd a"

   656   shows "a div b dvd c \<longleftrightarrow> a dvd c * b"

   657 proof -

   658   from \<open>b dvd a\<close> obtain d where "a = b * d" ..

   659   with \<open>b \<noteq> 0\<close> show ?thesis by (simp add: ac_simps)

   660 qed

   661

   662 lemma dvd_div_iff_mult:

   663   assumes "c \<noteq> 0" and "c dvd b"

   664   shows "a dvd b div c \<longleftrightarrow> a * c dvd b"

   665 proof -

   666   from \<open>c dvd b\<close> obtain d where "b = c * d" ..

   667   with \<open>c \<noteq> 0\<close> show ?thesis by (simp add: mult.commute [of a])

   668 qed

   669

   670 end

   671

   672 class idom_divide = idom + semidom_divide

   673

   674 class algebraic_semidom = semidom_divide

   675 begin

   676

   677 text \<open>

   678   Class @{class algebraic_semidom} enriches a integral domain

   679   by notions from algebra, like units in a ring.

   680   It is a separate class to avoid spoiling fields with notions

   681   which are degenerated there.

   682 \<close>

   683

   684 lemma dvd_div_mult_self [simp]:

   685   "a dvd b \<Longrightarrow> b div a * a = b"

   686   by (cases "a = 0") (auto elim: dvdE simp add: ac_simps)

   687

   688 lemma dvd_mult_div_cancel [simp]:

   689   "a dvd b \<Longrightarrow> a * (b div a) = b"

   690   using dvd_div_mult_self [of a b] by (simp add: ac_simps)

   691

   692 lemma div_mult_swap:

   693   assumes "c dvd b"

   694   shows "a * (b div c) = (a * b) div c"

   695 proof (cases "c = 0")

   696   case True then show ?thesis by simp

   697 next

   698   case False from assms obtain d where "b = c * d" ..

   699   moreover from False have "a * divide (d * c) c = ((a * d) * c) div c"

   700     by simp

   701   ultimately show ?thesis by (simp add: ac_simps)

   702 qed

   703

   704 lemma dvd_div_mult:

   705   assumes "c dvd b"

   706   shows "b div c * a = (b * a) div c"

   707   using assms div_mult_swap [of c b a] by (simp add: ac_simps)

   708

   709 lemma dvd_div_mult2_eq:

   710   assumes "b * c dvd a"

   711   shows "a div (b * c) = a div b div c"

   712 using assms proof

   713   fix k

   714   assume "a = b * c * k"

   715   then show ?thesis

   716     by (cases "b = 0 \<or> c = 0") (auto, simp add: ac_simps)

   717 qed

   718

   719

   720 text \<open>Units: invertible elements in a ring\<close>

   721

   722 abbreviation is_unit :: "'a \<Rightarrow> bool"

   723 where

   724   "is_unit a \<equiv> a dvd 1"

   725

   726 lemma not_is_unit_0 [simp]:

   727   "\<not> is_unit 0"

   728   by simp

   729

   730 lemma unit_imp_dvd [dest]:

   731   "is_unit b \<Longrightarrow> b dvd a"

   732   by (rule dvd_trans [of _ 1]) simp_all

   733

   734 lemma unit_dvdE:

   735   assumes "is_unit a"

   736   obtains c where "a \<noteq> 0" and "b = a * c"

   737 proof -

   738   from assms have "a dvd b" by auto

   739   then obtain c where "b = a * c" ..

   740   moreover from assms have "a \<noteq> 0" by auto

   741   ultimately show thesis using that by blast

   742 qed

   743

   744 lemma dvd_unit_imp_unit:

   745   "a dvd b \<Longrightarrow> is_unit b \<Longrightarrow> is_unit a"

   746   by (rule dvd_trans)

   747

   748 lemma unit_div_1_unit [simp, intro]:

   749   assumes "is_unit a"

   750   shows "is_unit (1 div a)"

   751 proof -

   752   from assms have "1 = 1 div a * a" by simp

   753   then show "is_unit (1 div a)" by (rule dvdI)

   754 qed

   755

   756 lemma is_unitE [elim?]:

   757   assumes "is_unit a"

   758   obtains b where "a \<noteq> 0" and "b \<noteq> 0"

   759     and "is_unit b" and "1 div a = b" and "1 div b = a"

   760     and "a * b = 1" and "c div a = c * b"

   761 proof (rule that)

   762   def b \<equiv> "1 div a"

   763   then show "1 div a = b" by simp

   764   from b_def is_unit a show "is_unit b" by simp

   765   from is_unit a and is_unit b show "a \<noteq> 0" and "b \<noteq> 0" by auto

   766   from b_def is_unit a show "a * b = 1" by simp

   767   then have "1 = a * b" ..

   768   with b_def b \<noteq> 0 show "1 div b = a" by simp

   769   from is_unit a have "a dvd c" ..

   770   then obtain d where "c = a * d" ..

   771   with a \<noteq> 0 a * b = 1 show "c div a = c * b"

   772     by (simp add: mult.assoc mult.left_commute [of a])

   773 qed

   774

   775 lemma unit_prod [intro]:

   776   "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a * b)"

   777   by (subst mult_1_left [of 1, symmetric]) (rule mult_dvd_mono)

   778

   779 lemma unit_div [intro]:

   780   "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a div b)"

   781   by (erule is_unitE [of b a]) (simp add: ac_simps unit_prod)

   782

   783 lemma mult_unit_dvd_iff:

   784   assumes "is_unit b"

   785   shows "a * b dvd c \<longleftrightarrow> a dvd c"

   786 proof

   787   assume "a * b dvd c"

   788   with assms show "a dvd c"

   789     by (simp add: dvd_mult_left)

   790 next

   791   assume "a dvd c"

   792   then obtain k where "c = a * k" ..

   793   with assms have "c = (a * b) * (1 div b * k)"

   794     by (simp add: mult_ac)

   795   then show "a * b dvd c" by (rule dvdI)

   796 qed

   797

   798 lemma dvd_mult_unit_iff:

   799   assumes "is_unit b"

   800   shows "a dvd c * b \<longleftrightarrow> a dvd c"

   801 proof

   802   assume "a dvd c * b"

   803   with assms have "c * b dvd c * (b * (1 div b))"

   804     by (subst mult_assoc [symmetric]) simp

   805   also from is_unit b have "b * (1 div b) = 1" by (rule is_unitE) simp

   806   finally have "c * b dvd c" by simp

   807   with a dvd c * b show "a dvd c" by (rule dvd_trans)

   808 next

   809   assume "a dvd c"

   810   then show "a dvd c * b" by simp

   811 qed

   812

   813 lemma div_unit_dvd_iff:

   814   "is_unit b \<Longrightarrow> a div b dvd c \<longleftrightarrow> a dvd c"

   815   by (erule is_unitE [of _ a]) (auto simp add: mult_unit_dvd_iff)

   816

   817 lemma dvd_div_unit_iff:

   818   "is_unit b \<Longrightarrow> a dvd c div b \<longleftrightarrow> a dvd c"

   819   by (erule is_unitE [of _ c]) (simp add: dvd_mult_unit_iff)

   820

   821 lemmas unit_dvd_iff = mult_unit_dvd_iff div_unit_dvd_iff

   822   dvd_mult_unit_iff dvd_div_unit_iff -- \<open>FIXME consider fact collection\<close>

   823

   824 lemma unit_mult_div_div [simp]:

   825   "is_unit a \<Longrightarrow> b * (1 div a) = b div a"

   826   by (erule is_unitE [of _ b]) simp

   827

   828 lemma unit_div_mult_self [simp]:

   829   "is_unit a \<Longrightarrow> b div a * a = b"

   830   by (rule dvd_div_mult_self) auto

   831

   832 lemma unit_div_1_div_1 [simp]:

   833   "is_unit a \<Longrightarrow> 1 div (1 div a) = a"

   834   by (erule is_unitE) simp

   835

   836 lemma unit_div_mult_swap:

   837   "is_unit c \<Longrightarrow> a * (b div c) = (a * b) div c"

   838   by (erule unit_dvdE [of _ b]) (simp add: mult.left_commute [of _ c])

   839

   840 lemma unit_div_commute:

   841   "is_unit b \<Longrightarrow> (a div b) * c = (a * c) div b"

   842   using unit_div_mult_swap [of b c a] by (simp add: ac_simps)

   843

   844 lemma unit_eq_div1:

   845   "is_unit b \<Longrightarrow> a div b = c \<longleftrightarrow> a = c * b"

   846   by (auto elim: is_unitE)

   847

   848 lemma unit_eq_div2:

   849   "is_unit b \<Longrightarrow> a = c div b \<longleftrightarrow> a * b = c"

   850   using unit_eq_div1 [of b c a] by auto

   851

   852 lemma unit_mult_left_cancel:

   853   assumes "is_unit a"

   854   shows "a * b = a * c \<longleftrightarrow> b = c" (is "?P \<longleftrightarrow> ?Q")

   855   using assms mult_cancel_left [of a b c] by auto

   856

   857 lemma unit_mult_right_cancel:

   858   "is_unit a \<Longrightarrow> b * a = c * a \<longleftrightarrow> b = c"

   859   using unit_mult_left_cancel [of a b c] by (auto simp add: ac_simps)

   860

   861 lemma unit_div_cancel:

   862   assumes "is_unit a"

   863   shows "b div a = c div a \<longleftrightarrow> b = c"

   864 proof -

   865   from assms have "is_unit (1 div a)" by simp

   866   then have "b * (1 div a) = c * (1 div a) \<longleftrightarrow> b = c"

   867     by (rule unit_mult_right_cancel)

   868   with assms show ?thesis by simp

   869 qed

   870

   871 lemma is_unit_div_mult2_eq:

   872   assumes "is_unit b" and "is_unit c"

   873   shows "a div (b * c) = a div b div c"

   874 proof -

   875   from assms have "is_unit (b * c)" by (simp add: unit_prod)

   876   then have "b * c dvd a"

   877     by (rule unit_imp_dvd)

   878   then show ?thesis

   879     by (rule dvd_div_mult2_eq)

   880 qed

   881

   882 lemmas unit_simps = mult_unit_dvd_iff div_unit_dvd_iff dvd_mult_unit_iff

   883   dvd_div_unit_iff unit_div_mult_swap unit_div_commute

   884   unit_mult_left_cancel unit_mult_right_cancel unit_div_cancel

   885   unit_eq_div1 unit_eq_div2

   886

   887 lemma is_unit_divide_mult_cancel_left:

   888   assumes "a \<noteq> 0" and "is_unit b"

   889   shows "a div (a * b) = 1 div b"

   890 proof -

   891   from assms have "a div (a * b) = a div a div b"

   892     by (simp add: mult_unit_dvd_iff dvd_div_mult2_eq)

   893   with assms show ?thesis by simp

   894 qed

   895

   896 lemma is_unit_divide_mult_cancel_right:

   897   assumes "a \<noteq> 0" and "is_unit b"

   898   shows "a div (b * a) = 1 div b"

   899   using assms is_unit_divide_mult_cancel_left [of a b] by (simp add: ac_simps)

   900

   901 end

   902

   903 class normalization_semidom = algebraic_semidom +

   904   fixes normalize :: "'a \<Rightarrow> 'a"

   905     and unit_factor :: "'a \<Rightarrow> 'a"

   906   assumes unit_factor_mult_normalize [simp]: "unit_factor a * normalize a = a"

   907   assumes normalize_0 [simp]: "normalize 0 = 0"

   908     and unit_factor_0 [simp]: "unit_factor 0 = 0"

   909   assumes is_unit_normalize:

   910     "is_unit a  \<Longrightarrow> normalize a = 1"

   911   assumes unit_factor_is_unit [iff]:

   912     "a \<noteq> 0 \<Longrightarrow> is_unit (unit_factor a)"

   913   assumes unit_factor_mult: "unit_factor (a * b) = unit_factor a * unit_factor b"

   914 begin

   915

   916 text \<open>

   917   Class @{class normalization_semidom} cultivates the idea that

   918   each integral domain can be split into equivalence classes

   919   whose representants are associated, i.e. divide each other.

   920   @{const normalize} specifies a canonical representant for each equivalence

   921   class.  The rationale behind this is that it is easier to reason about equality

   922   than equivalences, hence we prefer to think about equality of normalized

   923   values rather than associated elements.

   924 \<close>

   925

   926 lemma unit_factor_dvd [simp]:

   927   "a \<noteq> 0 \<Longrightarrow> unit_factor a dvd b"

   928   by (rule unit_imp_dvd) simp

   929

   930 lemma unit_factor_self [simp]:

   931   "unit_factor a dvd a"

   932   by (cases "a = 0") simp_all

   933

   934 lemma normalize_mult_unit_factor [simp]:

   935   "normalize a * unit_factor a = a"

   936   using unit_factor_mult_normalize [of a] by (simp add: ac_simps)

   937

   938 lemma normalize_eq_0_iff [simp]:

   939   "normalize a = 0 \<longleftrightarrow> a = 0" (is "?P \<longleftrightarrow> ?Q")

   940 proof

   941   assume ?P

   942   moreover have "unit_factor a * normalize a = a" by simp

   943   ultimately show ?Q by simp

   944 next

   945   assume ?Q then show ?P by simp

   946 qed

   947

   948 lemma unit_factor_eq_0_iff [simp]:

   949   "unit_factor a = 0 \<longleftrightarrow> a = 0" (is "?P \<longleftrightarrow> ?Q")

   950 proof

   951   assume ?P

   952   moreover have "unit_factor a * normalize a = a" by simp

   953   ultimately show ?Q by simp

   954 next

   955   assume ?Q then show ?P by simp

   956 qed

   957

   958 lemma is_unit_unit_factor:

   959   assumes "is_unit a" shows "unit_factor a = a"

   960 proof -

   961   from assms have "normalize a = 1" by (rule is_unit_normalize)

   962   moreover from unit_factor_mult_normalize have "unit_factor a * normalize a = a" .

   963   ultimately show ?thesis by simp

   964 qed

   965

   966 lemma unit_factor_1 [simp]:

   967   "unit_factor 1 = 1"

   968   by (rule is_unit_unit_factor) simp

   969

   970 lemma normalize_1 [simp]:

   971   "normalize 1 = 1"

   972   by (rule is_unit_normalize) simp

   973

   974 lemma normalize_1_iff:

   975   "normalize a = 1 \<longleftrightarrow> is_unit a" (is "?P \<longleftrightarrow> ?Q")

   976 proof

   977   assume ?Q then show ?P by (rule is_unit_normalize)

   978 next

   979   assume ?P

   980   then have "a \<noteq> 0" by auto

   981   from \<open>?P\<close> have "unit_factor a * normalize a = unit_factor a * 1"

   982     by simp

   983   then have "unit_factor a = a"

   984     by simp

   985   moreover have "is_unit (unit_factor a)"

   986     using \<open>a \<noteq> 0\<close> by simp

   987   ultimately show ?Q by simp

   988 qed

   989

   990 lemma div_normalize [simp]:

   991   "a div normalize a = unit_factor a"

   992 proof (cases "a = 0")

   993   case True then show ?thesis by simp

   994 next

   995   case False then have "normalize a \<noteq> 0" by simp

   996   with nonzero_mult_divide_cancel_right

   997   have "unit_factor a * normalize a div normalize a = unit_factor a" by blast

   998   then show ?thesis by simp

   999 qed

  1000

  1001 lemma div_unit_factor [simp]:

  1002   "a div unit_factor a = normalize a"

  1003 proof (cases "a = 0")

  1004   case True then show ?thesis by simp

  1005 next

  1006   case False then have "unit_factor a \<noteq> 0" by simp

  1007   with nonzero_mult_divide_cancel_left

  1008   have "unit_factor a * normalize a div unit_factor a = normalize a" by blast

  1009   then show ?thesis by simp

  1010 qed

  1011

  1012 lemma normalize_div [simp]:

  1013   "normalize a div a = 1 div unit_factor a"

  1014 proof (cases "a = 0")

  1015   case True then show ?thesis by simp

  1016 next

  1017   case False

  1018   have "normalize a div a = normalize a div (unit_factor a * normalize a)"

  1019     by simp

  1020   also have "\<dots> = 1 div unit_factor a"

  1021     using False by (subst is_unit_divide_mult_cancel_right) simp_all

  1022   finally show ?thesis .

  1023 qed

  1024

  1025 lemma mult_one_div_unit_factor [simp]:

  1026   "a * (1 div unit_factor b) = a div unit_factor b"

  1027   by (cases "b = 0") simp_all

  1028

  1029 lemma normalize_mult:

  1030   "normalize (a * b) = normalize a * normalize b"

  1031 proof (cases "a = 0 \<or> b = 0")

  1032   case True then show ?thesis by auto

  1033 next

  1034   case False

  1035   from unit_factor_mult_normalize have "unit_factor (a * b) * normalize (a * b) = a * b" .

  1036   then have "normalize (a * b) = a * b div unit_factor (a * b)" by simp

  1037   also have "\<dots> = a * b div unit_factor (b * a)" by (simp add: ac_simps)

  1038   also have "\<dots> = a * b div unit_factor b div unit_factor a"

  1039     using False by (simp add: unit_factor_mult is_unit_div_mult2_eq [symmetric])

  1040   also have "\<dots> = a * (b div unit_factor b) div unit_factor a"

  1041     using False by (subst unit_div_mult_swap) simp_all

  1042   also have "\<dots> = normalize a * normalize b"

  1043     using False by (simp add: mult.commute [of a] mult.commute [of "normalize a"] unit_div_mult_swap [symmetric])

  1044   finally show ?thesis .

  1045 qed

  1046

  1047 lemma unit_factor_idem [simp]:

  1048   "unit_factor (unit_factor a) = unit_factor a"

  1049   by (cases "a = 0") (auto intro: is_unit_unit_factor)

  1050

  1051 lemma normalize_unit_factor [simp]:

  1052   "a \<noteq> 0 \<Longrightarrow> normalize (unit_factor a) = 1"

  1053   by (rule is_unit_normalize) simp

  1054

  1055 lemma normalize_idem [simp]:

  1056   "normalize (normalize a) = normalize a"

  1057 proof (cases "a = 0")

  1058   case True then show ?thesis by simp

  1059 next

  1060   case False

  1061   have "normalize a = normalize (unit_factor a * normalize a)" by simp

  1062   also have "\<dots> = normalize (unit_factor a) * normalize (normalize a)"

  1063     by (simp only: normalize_mult)

  1064   finally show ?thesis using False by simp_all

  1065 qed

  1066

  1067 lemma unit_factor_normalize [simp]:

  1068   assumes "a \<noteq> 0"

  1069   shows "unit_factor (normalize a) = 1"

  1070 proof -

  1071   from assms have "normalize a \<noteq> 0" by simp

  1072   have "unit_factor (normalize a) * normalize (normalize a) = normalize a"

  1073     by (simp only: unit_factor_mult_normalize)

  1074   then have "unit_factor (normalize a) * normalize a = normalize a"

  1075     by simp

  1076   with \<open>normalize a \<noteq> 0\<close>

  1077   have "unit_factor (normalize a) * normalize a div normalize a = normalize a div normalize a"

  1078     by simp

  1079   with \<open>normalize a \<noteq> 0\<close>

  1080   show ?thesis by simp

  1081 qed

  1082

  1083 lemma dvd_unit_factor_div:

  1084   assumes "b dvd a"

  1085   shows "unit_factor (a div b) = unit_factor a div unit_factor b"

  1086 proof -

  1087   from assms have "a = a div b * b"

  1088     by simp

  1089   then have "unit_factor a = unit_factor (a div b * b)"

  1090     by simp

  1091   then show ?thesis

  1092     by (cases "b = 0") (simp_all add: unit_factor_mult)

  1093 qed

  1094

  1095 lemma dvd_normalize_div:

  1096   assumes "b dvd a"

  1097   shows "normalize (a div b) = normalize a div normalize b"

  1098 proof -

  1099   from assms have "a = a div b * b"

  1100     by simp

  1101   then have "normalize a = normalize (a div b * b)"

  1102     by simp

  1103   then show ?thesis

  1104     by (cases "b = 0") (simp_all add: normalize_mult)

  1105 qed

  1106

  1107 lemma normalize_dvd_iff [simp]:

  1108   "normalize a dvd b \<longleftrightarrow> a dvd b"

  1109 proof -

  1110   have "normalize a dvd b \<longleftrightarrow> unit_factor a * normalize a dvd b"

  1111     using mult_unit_dvd_iff [of "unit_factor a" "normalize a" b]

  1112       by (cases "a = 0") simp_all

  1113   then show ?thesis by simp

  1114 qed

  1115

  1116 lemma dvd_normalize_iff [simp]:

  1117   "a dvd normalize b \<longleftrightarrow> a dvd b"

  1118 proof -

  1119   have "a dvd normalize  b \<longleftrightarrow> a dvd normalize b * unit_factor b"

  1120     using dvd_mult_unit_iff [of "unit_factor b" a "normalize b"]

  1121       by (cases "b = 0") simp_all

  1122   then show ?thesis by simp

  1123 qed

  1124

  1125 text \<open>

  1126   We avoid an explicit definition of associated elements but prefer

  1127   explicit normalisation instead.  In theory we could define an abbreviation

  1128   like @{prop "associated a b \<longleftrightarrow> normalize a = normalize b"} but this is

  1129   counterproductive without suggestive infix syntax, which we do not want

  1130   to sacrifice for this purpose here.

  1131 \<close>

  1132

  1133 lemma associatedI:

  1134   assumes "a dvd b" and "b dvd a"

  1135   shows "normalize a = normalize b"

  1136 proof (cases "a = 0 \<or> b = 0")

  1137   case True with assms show ?thesis by auto

  1138 next

  1139   case False

  1140   from \<open>a dvd b\<close> obtain c where b: "b = a * c" ..

  1141   moreover from \<open>b dvd a\<close> obtain d where a: "a = b * d" ..

  1142   ultimately have "b * 1 = b * (c * d)" by (simp add: ac_simps)

  1143   with False have "1 = c * d"

  1144     unfolding mult_cancel_left by simp

  1145   then have "is_unit c" and "is_unit d" by auto

  1146   with a b show ?thesis by (simp add: normalize_mult is_unit_normalize)

  1147 qed

  1148

  1149 lemma associatedD1:

  1150   "normalize a = normalize b \<Longrightarrow> a dvd b"

  1151   using dvd_normalize_iff [of _ b, symmetric] normalize_dvd_iff [of a _, symmetric]

  1152   by simp

  1153

  1154 lemma associatedD2:

  1155   "normalize a = normalize b \<Longrightarrow> b dvd a"

  1156   using dvd_normalize_iff [of _ a, symmetric] normalize_dvd_iff [of b _, symmetric]

  1157   by simp

  1158

  1159 lemma associated_unit:

  1160   "normalize a = normalize b \<Longrightarrow> is_unit a \<Longrightarrow> is_unit b"

  1161   using dvd_unit_imp_unit by (auto dest!: associatedD1 associatedD2)

  1162

  1163 lemma associated_iff_dvd:

  1164   "normalize a = normalize b \<longleftrightarrow> a dvd b \<and> b dvd a" (is "?P \<longleftrightarrow> ?Q")

  1165 proof

  1166   assume ?Q then show ?P by (auto intro!: associatedI)

  1167 next

  1168   assume ?P

  1169   then have "unit_factor a * normalize a = unit_factor a * normalize b"

  1170     by simp

  1171   then have *: "normalize b * unit_factor a = a"

  1172     by (simp add: ac_simps)

  1173   show ?Q

  1174   proof (cases "a = 0 \<or> b = 0")

  1175     case True with \<open>?P\<close> show ?thesis by auto

  1176   next

  1177     case False

  1178     then have "b dvd normalize b * unit_factor a" and "normalize b * unit_factor a dvd b"

  1179       by (simp_all add: mult_unit_dvd_iff dvd_mult_unit_iff)

  1180     with * show ?thesis by simp

  1181   qed

  1182 qed

  1183

  1184 lemma associated_eqI:

  1185   assumes "a dvd b" and "b dvd a"

  1186   assumes "normalize a = a" and "normalize b = b"

  1187   shows "a = b"

  1188 proof -

  1189   from assms have "normalize a = normalize b"

  1190     unfolding associated_iff_dvd by simp

  1191   with \<open>normalize a = a\<close> have "a = normalize b" by simp

  1192   with \<open>normalize b = b\<close> show "a = b" by simp

  1193 qed

  1194

  1195 end

  1196

  1197 class ordered_semiring = semiring + comm_monoid_add + ordered_ab_semigroup_add +

  1198   assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"

  1199   assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"

  1200 begin

  1201

  1202 lemma mult_mono:

  1203   "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * d"

  1204 apply (erule mult_right_mono [THEN order_trans], assumption)

  1205 apply (erule mult_left_mono, assumption)

  1206 done

  1207

  1208 lemma mult_mono':

  1209   "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * d"

  1210 apply (rule mult_mono)

  1211 apply (fast intro: order_trans)+

  1212 done

  1213

  1214 end

  1215

  1216 class ordered_cancel_semiring = ordered_semiring + cancel_comm_monoid_add

  1217 begin

  1218

  1219 subclass semiring_0_cancel ..

  1220

  1221 lemma mult_nonneg_nonneg[simp]: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b"

  1222 using mult_left_mono [of 0 b a] by simp

  1223

  1224 lemma mult_nonneg_nonpos: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> a * b \<le> 0"

  1225 using mult_left_mono [of b 0 a] by simp

  1226

  1227 lemma mult_nonpos_nonneg: "a \<le> 0 \<Longrightarrow> 0 \<le> b \<Longrightarrow> a * b \<le> 0"

  1228 using mult_right_mono [of a 0 b] by simp

  1229

  1230 text {* Legacy - use @{text mult_nonpos_nonneg} *}

  1231 lemma mult_nonneg_nonpos2: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> b * a \<le> 0"

  1232 by (drule mult_right_mono [of b 0], auto)

  1233

  1234 lemma split_mult_neg_le: "(0 \<le> a & b \<le> 0) | (a \<le> 0 & 0 \<le> b) \<Longrightarrow> a * b \<le> 0"

  1235 by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)

  1236

  1237 end

  1238

  1239 class linordered_semiring = ordered_semiring + linordered_cancel_ab_semigroup_add

  1240 begin

  1241

  1242 subclass ordered_cancel_semiring ..

  1243

  1244 subclass ordered_comm_monoid_add ..

  1245

  1246 lemma mult_left_less_imp_less:

  1247   "c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"

  1248 by (force simp add: mult_left_mono not_le [symmetric])

  1249

  1250 lemma mult_right_less_imp_less:

  1251   "a * c < b * c \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"

  1252 by (force simp add: mult_right_mono not_le [symmetric])

  1253

  1254 end

  1255

  1256 class linordered_semiring_1 = linordered_semiring + semiring_1

  1257 begin

  1258

  1259 lemma convex_bound_le:

  1260   assumes "x \<le> a" "y \<le> a" "0 \<le> u" "0 \<le> v" "u + v = 1"

  1261   shows "u * x + v * y \<le> a"

  1262 proof-

  1263   from assms have "u * x + v * y \<le> u * a + v * a"

  1264     by (simp add: add_mono mult_left_mono)

  1265   thus ?thesis using assms unfolding distrib_right[symmetric] by simp

  1266 qed

  1267

  1268 end

  1269

  1270 class linordered_semiring_strict = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add +

  1271   assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"

  1272   assumes mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c"

  1273 begin

  1274

  1275 subclass semiring_0_cancel ..

  1276

  1277 subclass linordered_semiring

  1278 proof

  1279   fix a b c :: 'a

  1280   assume A: "a \<le> b" "0 \<le> c"

  1281   from A show "c * a \<le> c * b"

  1282     unfolding le_less

  1283     using mult_strict_left_mono by (cases "c = 0") auto

  1284   from A show "a * c \<le> b * c"

  1285     unfolding le_less

  1286     using mult_strict_right_mono by (cases "c = 0") auto

  1287 qed

  1288

  1289 lemma mult_left_le_imp_le:

  1290   "c * a \<le> c * b \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"

  1291 by (force simp add: mult_strict_left_mono _not_less [symmetric])

  1292

  1293 lemma mult_right_le_imp_le:

  1294   "a * c \<le> b * c \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"

  1295 by (force simp add: mult_strict_right_mono not_less [symmetric])

  1296

  1297 lemma mult_pos_pos[simp]: "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a * b"

  1298 using mult_strict_left_mono [of 0 b a] by simp

  1299

  1300 lemma mult_pos_neg: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> a * b < 0"

  1301 using mult_strict_left_mono [of b 0 a] by simp

  1302

  1303 lemma mult_neg_pos: "a < 0 \<Longrightarrow> 0 < b \<Longrightarrow> a * b < 0"

  1304 using mult_strict_right_mono [of a 0 b] by simp

  1305

  1306 text {* Legacy - use @{text mult_neg_pos} *}

  1307 lemma mult_pos_neg2: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> b * a < 0"

  1308 by (drule mult_strict_right_mono [of b 0], auto)

  1309

  1310 lemma zero_less_mult_pos:

  1311   "0 < a * b \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"

  1312 apply (cases "b\<le>0")

  1313  apply (auto simp add: le_less not_less)

  1314 apply (drule_tac mult_pos_neg [of a b])

  1315  apply (auto dest: less_not_sym)

  1316 done

  1317

  1318 lemma zero_less_mult_pos2:

  1319   "0 < b * a \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"

  1320 apply (cases "b\<le>0")

  1321  apply (auto simp add: le_less not_less)

  1322 apply (drule_tac mult_pos_neg2 [of a b])

  1323  apply (auto dest: less_not_sym)

  1324 done

  1325

  1326 text{*Strict monotonicity in both arguments*}

  1327 lemma mult_strict_mono:

  1328   assumes "a < b" and "c < d" and "0 < b" and "0 \<le> c"

  1329   shows "a * c < b * d"

  1330   using assms apply (cases "c=0")

  1331   apply (simp)

  1332   apply (erule mult_strict_right_mono [THEN less_trans])

  1333   apply (force simp add: le_less)

  1334   apply (erule mult_strict_left_mono, assumption)

  1335   done

  1336

  1337 text{*This weaker variant has more natural premises*}

  1338 lemma mult_strict_mono':

  1339   assumes "a < b" and "c < d" and "0 \<le> a" and "0 \<le> c"

  1340   shows "a * c < b * d"

  1341 by (rule mult_strict_mono) (insert assms, auto)

  1342

  1343 lemma mult_less_le_imp_less:

  1344   assumes "a < b" and "c \<le> d" and "0 \<le> a" and "0 < c"

  1345   shows "a * c < b * d"

  1346   using assms apply (subgoal_tac "a * c < b * c")

  1347   apply (erule less_le_trans)

  1348   apply (erule mult_left_mono)

  1349   apply simp

  1350   apply (erule mult_strict_right_mono)

  1351   apply assumption

  1352   done

  1353

  1354 lemma mult_le_less_imp_less:

  1355   assumes "a \<le> b" and "c < d" and "0 < a" and "0 \<le> c"

  1356   shows "a * c < b * d"

  1357   using assms apply (subgoal_tac "a * c \<le> b * c")

  1358   apply (erule le_less_trans)

  1359   apply (erule mult_strict_left_mono)

  1360   apply simp

  1361   apply (erule mult_right_mono)

  1362   apply simp

  1363   done

  1364

  1365 end

  1366

  1367 class linordered_semiring_1_strict = linordered_semiring_strict + semiring_1

  1368 begin

  1369

  1370 subclass linordered_semiring_1 ..

  1371

  1372 lemma convex_bound_lt:

  1373   assumes "x < a" "y < a" "0 \<le> u" "0 \<le> v" "u + v = 1"

  1374   shows "u * x + v * y < a"

  1375 proof -

  1376   from assms have "u * x + v * y < u * a + v * a"

  1377     by (cases "u = 0")

  1378        (auto intro!: add_less_le_mono mult_strict_left_mono mult_left_mono)

  1379   thus ?thesis using assms unfolding distrib_right[symmetric] by simp

  1380 qed

  1381

  1382 end

  1383

  1384 class ordered_comm_semiring = comm_semiring_0 + ordered_ab_semigroup_add +

  1385   assumes comm_mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"

  1386 begin

  1387

  1388 subclass ordered_semiring

  1389 proof

  1390   fix a b c :: 'a

  1391   assume "a \<le> b" "0 \<le> c"

  1392   thus "c * a \<le> c * b" by (rule comm_mult_left_mono)

  1393   thus "a * c \<le> b * c" by (simp only: mult.commute)

  1394 qed

  1395

  1396 end

  1397

  1398 class ordered_cancel_comm_semiring = ordered_comm_semiring + cancel_comm_monoid_add

  1399 begin

  1400

  1401 subclass comm_semiring_0_cancel ..

  1402 subclass ordered_comm_semiring ..

  1403 subclass ordered_cancel_semiring ..

  1404

  1405 end

  1406

  1407 class linordered_comm_semiring_strict = comm_semiring_0 + linordered_cancel_ab_semigroup_add +

  1408   assumes comm_mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"

  1409 begin

  1410

  1411 subclass linordered_semiring_strict

  1412 proof

  1413   fix a b c :: 'a

  1414   assume "a < b" "0 < c"

  1415   thus "c * a < c * b" by (rule comm_mult_strict_left_mono)

  1416   thus "a * c < b * c" by (simp only: mult.commute)

  1417 qed

  1418

  1419 subclass ordered_cancel_comm_semiring

  1420 proof

  1421   fix a b c :: 'a

  1422   assume "a \<le> b" "0 \<le> c"

  1423   thus "c * a \<le> c * b"

  1424     unfolding le_less

  1425     using mult_strict_left_mono by (cases "c = 0") auto

  1426 qed

  1427

  1428 end

  1429

  1430 class ordered_ring = ring + ordered_cancel_semiring

  1431 begin

  1432

  1433 subclass ordered_ab_group_add ..

  1434

  1435 lemma less_add_iff1:

  1436   "a * e + c < b * e + d \<longleftrightarrow> (a - b) * e + c < d"

  1437 by (simp add: algebra_simps)

  1438

  1439 lemma less_add_iff2:

  1440   "a * e + c < b * e + d \<longleftrightarrow> c < (b - a) * e + d"

  1441 by (simp add: algebra_simps)

  1442

  1443 lemma le_add_iff1:

  1444   "a * e + c \<le> b * e + d \<longleftrightarrow> (a - b) * e + c \<le> d"

  1445 by (simp add: algebra_simps)

  1446

  1447 lemma le_add_iff2:

  1448   "a * e + c \<le> b * e + d \<longleftrightarrow> c \<le> (b - a) * e + d"

  1449 by (simp add: algebra_simps)

  1450

  1451 lemma mult_left_mono_neg:

  1452   "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> c * a \<le> c * b"

  1453   apply (drule mult_left_mono [of _ _ "- c"])

  1454   apply simp_all

  1455   done

  1456

  1457 lemma mult_right_mono_neg:

  1458   "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> a * c \<le> b * c"

  1459   apply (drule mult_right_mono [of _ _ "- c"])

  1460   apply simp_all

  1461   done

  1462

  1463 lemma mult_nonpos_nonpos: "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> 0 \<le> a * b"

  1464 using mult_right_mono_neg [of a 0 b] by simp

  1465

  1466 lemma split_mult_pos_le:

  1467   "(0 \<le> a \<and> 0 \<le> b) \<or> (a \<le> 0 \<and> b \<le> 0) \<Longrightarrow> 0 \<le> a * b"

  1468 by (auto simp add: mult_nonpos_nonpos)

  1469

  1470 end

  1471

  1472 class linordered_ring = ring + linordered_semiring + linordered_ab_group_add + abs_if

  1473 begin

  1474

  1475 subclass ordered_ring ..

  1476

  1477 subclass ordered_ab_group_add_abs

  1478 proof

  1479   fix a b

  1480   show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"

  1481     by (auto simp add: abs_if not_le not_less algebra_simps simp del: add.commute dest: add_neg_neg add_nonneg_nonneg)

  1482 qed (auto simp add: abs_if)

  1483

  1484 lemma zero_le_square [simp]: "0 \<le> a * a"

  1485   using linear [of 0 a]

  1486   by (auto simp add: mult_nonpos_nonpos)

  1487

  1488 lemma not_square_less_zero [simp]: "\<not> (a * a < 0)"

  1489   by (simp add: not_less)

  1490

  1491 end

  1492

  1493 class linordered_ring_strict = ring + linordered_semiring_strict

  1494   + ordered_ab_group_add + abs_if

  1495 begin

  1496

  1497 subclass linordered_ring ..

  1498

  1499 lemma mult_strict_left_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> c * a < c * b"

  1500 using mult_strict_left_mono [of b a "- c"] by simp

  1501

  1502 lemma mult_strict_right_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> a * c < b * c"

  1503 using mult_strict_right_mono [of b a "- c"] by simp

  1504

  1505 lemma mult_neg_neg: "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> 0 < a * b"

  1506 using mult_strict_right_mono_neg [of a 0 b] by simp

  1507

  1508 subclass ring_no_zero_divisors

  1509 proof

  1510   fix a b

  1511   assume "a \<noteq> 0" then have A: "a < 0 \<or> 0 < a" by (simp add: neq_iff)

  1512   assume "b \<noteq> 0" then have B: "b < 0 \<or> 0 < b" by (simp add: neq_iff)

  1513   have "a * b < 0 \<or> 0 < a * b"

  1514   proof (cases "a < 0")

  1515     case True note A' = this

  1516     show ?thesis proof (cases "b < 0")

  1517       case True with A'

  1518       show ?thesis by (auto dest: mult_neg_neg)

  1519     next

  1520       case False with B have "0 < b" by auto

  1521       with A' show ?thesis by (auto dest: mult_strict_right_mono)

  1522     qed

  1523   next

  1524     case False with A have A': "0 < a" by auto

  1525     show ?thesis proof (cases "b < 0")

  1526       case True with A'

  1527       show ?thesis by (auto dest: mult_strict_right_mono_neg)

  1528     next

  1529       case False with B have "0 < b" by auto

  1530       with A' show ?thesis by auto

  1531     qed

  1532   qed

  1533   then show "a * b \<noteq> 0" by (simp add: neq_iff)

  1534 qed

  1535

  1536 lemma zero_less_mult_iff: "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0"

  1537   by (cases a 0 b 0 rule: linorder_cases[case_product linorder_cases])

  1538      (auto simp add: mult_neg_neg not_less le_less dest: zero_less_mult_pos zero_less_mult_pos2)

  1539

  1540 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"

  1541   by (auto simp add: eq_commute [of 0] le_less not_less zero_less_mult_iff)

  1542

  1543 lemma mult_less_0_iff:

  1544   "a * b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b"

  1545   apply (insert zero_less_mult_iff [of "-a" b])

  1546   apply force

  1547   done

  1548

  1549 lemma mult_le_0_iff:

  1550   "a * b \<le> 0 \<longleftrightarrow> 0 \<le> a \<and> b \<le> 0 \<or> a \<le> 0 \<and> 0 \<le> b"

  1551   apply (insert zero_le_mult_iff [of "-a" b])

  1552   apply force

  1553   done

  1554

  1555 text{*Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"},

  1556    also with the relations @{text "\<le>"} and equality.*}

  1557

  1558 text{*These disjunction'' versions produce two cases when the comparison is

  1559  an assumption, but effectively four when the comparison is a goal.*}

  1560

  1561 lemma mult_less_cancel_right_disj:

  1562   "a * c < b * c \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"

  1563   apply (cases "c = 0")

  1564   apply (auto simp add: neq_iff mult_strict_right_mono

  1565                       mult_strict_right_mono_neg)

  1566   apply (auto simp add: not_less

  1567                       not_le [symmetric, of "a*c"]

  1568                       not_le [symmetric, of a])

  1569   apply (erule_tac [!] notE)

  1570   apply (auto simp add: less_imp_le mult_right_mono

  1571                       mult_right_mono_neg)

  1572   done

  1573

  1574 lemma mult_less_cancel_left_disj:

  1575   "c * a < c * b \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"

  1576   apply (cases "c = 0")

  1577   apply (auto simp add: neq_iff mult_strict_left_mono

  1578                       mult_strict_left_mono_neg)

  1579   apply (auto simp add: not_less

  1580                       not_le [symmetric, of "c*a"]

  1581                       not_le [symmetric, of a])

  1582   apply (erule_tac [!] notE)

  1583   apply (auto simp add: less_imp_le mult_left_mono

  1584                       mult_left_mono_neg)

  1585   done

  1586

  1587 text{*The conjunction of implication'' lemmas produce two cases when the

  1588 comparison is a goal, but give four when the comparison is an assumption.*}

  1589

  1590 lemma mult_less_cancel_right:

  1591   "a * c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)"

  1592   using mult_less_cancel_right_disj [of a c b] by auto

  1593

  1594 lemma mult_less_cancel_left:

  1595   "c * a < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)"

  1596   using mult_less_cancel_left_disj [of c a b] by auto

  1597

  1598 lemma mult_le_cancel_right:

  1599    "a * c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"

  1600 by (simp add: not_less [symmetric] mult_less_cancel_right_disj)

  1601

  1602 lemma mult_le_cancel_left:

  1603   "c * a \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"

  1604 by (simp add: not_less [symmetric] mult_less_cancel_left_disj)

  1605

  1606 lemma mult_le_cancel_left_pos:

  1607   "0 < c \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> a \<le> b"

  1608 by (auto simp: mult_le_cancel_left)

  1609

  1610 lemma mult_le_cancel_left_neg:

  1611   "c < 0 \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> b \<le> a"

  1612 by (auto simp: mult_le_cancel_left)

  1613

  1614 lemma mult_less_cancel_left_pos:

  1615   "0 < c \<Longrightarrow> c * a < c * b \<longleftrightarrow> a < b"

  1616 by (auto simp: mult_less_cancel_left)

  1617

  1618 lemma mult_less_cancel_left_neg:

  1619   "c < 0 \<Longrightarrow> c * a < c * b \<longleftrightarrow> b < a"

  1620 by (auto simp: mult_less_cancel_left)

  1621

  1622 end

  1623

  1624 lemmas mult_sign_intros =

  1625   mult_nonneg_nonneg mult_nonneg_nonpos

  1626   mult_nonpos_nonneg mult_nonpos_nonpos

  1627   mult_pos_pos mult_pos_neg

  1628   mult_neg_pos mult_neg_neg

  1629

  1630 class ordered_comm_ring = comm_ring + ordered_comm_semiring

  1631 begin

  1632

  1633 subclass ordered_ring ..

  1634 subclass ordered_cancel_comm_semiring ..

  1635

  1636 end

  1637

  1638 class linordered_semidom = semidom + linordered_comm_semiring_strict +

  1639   assumes zero_less_one [simp]: "0 < 1"

  1640   assumes le_add_diff_inverse2 [simp]: "b \<le> a \<Longrightarrow> a - b + b = a"

  1641 begin

  1642

  1643 text {* Addition is the inverse of subtraction. *}

  1644

  1645 lemma le_add_diff_inverse [simp]: "b \<le> a \<Longrightarrow> b + (a - b) = a"

  1646   by (frule le_add_diff_inverse2) (simp add: add.commute)

  1647

  1648 lemma add_diff_inverse: "~ a<b \<Longrightarrow> b + (a - b) = a"

  1649   by simp

  1650

  1651 lemma add_le_imp_le_diff:

  1652   shows "i + k \<le> n \<Longrightarrow> i \<le> n - k"

  1653   apply (subst add_le_cancel_right [where c=k, symmetric])

  1654   apply (frule le_add_diff_inverse2)

  1655   apply (simp only: add.assoc [symmetric])

  1656   using add_implies_diff by fastforce

  1657

  1658 lemma add_le_add_imp_diff_le:

  1659   assumes a1: "i + k \<le> n"

  1660       and a2: "n \<le> j + k"

  1661   shows "\<lbrakk>i + k \<le> n; n \<le> j + k\<rbrakk> \<Longrightarrow> n - k \<le> j"

  1662 proof -

  1663   have "n - (i + k) + (i + k) = n"

  1664     using a1 by simp

  1665   moreover have "n - k = n - k - i + i"

  1666     using a1 by (simp add: add_le_imp_le_diff)

  1667   ultimately show ?thesis

  1668     using a2

  1669     apply (simp add: add.assoc [symmetric])

  1670     apply (rule add_le_imp_le_diff [of _ k "j+k", simplified add_diff_cancel_right'])

  1671     by (simp add: add.commute diff_diff_add)

  1672 qed

  1673

  1674 lemma pos_add_strict:

  1675   shows "0 < a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"

  1676   using add_strict_mono [of 0 a b c] by simp

  1677

  1678 lemma zero_le_one [simp]: "0 \<le> 1"

  1679 by (rule zero_less_one [THEN less_imp_le])

  1680

  1681 lemma not_one_le_zero [simp]: "\<not> 1 \<le> 0"

  1682 by (simp add: not_le)

  1683

  1684 lemma not_one_less_zero [simp]: "\<not> 1 < 0"

  1685 by (simp add: not_less)

  1686

  1687 lemma less_1_mult:

  1688   assumes "1 < m" and "1 < n"

  1689   shows "1 < m * n"

  1690   using assms mult_strict_mono [of 1 m 1 n]

  1691     by (simp add:  less_trans [OF zero_less_one])

  1692

  1693 lemma mult_left_le: "c \<le> 1 \<Longrightarrow> 0 \<le> a \<Longrightarrow> a * c \<le> a"

  1694   using mult_left_mono[of c 1 a] by simp

  1695

  1696 lemma mult_le_one: "a \<le> 1 \<Longrightarrow> 0 \<le> b \<Longrightarrow> b \<le> 1 \<Longrightarrow> a * b \<le> 1"

  1697   using mult_mono[of a 1 b 1] by simp

  1698

  1699 end

  1700

  1701 class linordered_idom = comm_ring_1 +

  1702   linordered_comm_semiring_strict + ordered_ab_group_add +

  1703   abs_if + sgn_if

  1704 begin

  1705

  1706 subclass linordered_semiring_1_strict ..

  1707 subclass linordered_ring_strict ..

  1708 subclass ordered_comm_ring ..

  1709 subclass idom ..

  1710

  1711 subclass linordered_semidom

  1712 proof

  1713   have "0 \<le> 1 * 1" by (rule zero_le_square)

  1714   thus "0 < 1" by (simp add: le_less)

  1715   show "\<And>b a. b \<le> a \<Longrightarrow> a - b + b = a"

  1716     by simp

  1717 qed

  1718

  1719 lemma linorder_neqE_linordered_idom:

  1720   assumes "x \<noteq> y" obtains "x < y" | "y < x"

  1721   using assms by (rule neqE)

  1722

  1723 text {* These cancellation simprules also produce two cases when the comparison is a goal. *}

  1724

  1725 lemma mult_le_cancel_right1:

  1726   "c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)"

  1727 by (insert mult_le_cancel_right [of 1 c b], simp)

  1728

  1729 lemma mult_le_cancel_right2:

  1730   "a * c \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)"

  1731 by (insert mult_le_cancel_right [of a c 1], simp)

  1732

  1733 lemma mult_le_cancel_left1:

  1734   "c \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)"

  1735 by (insert mult_le_cancel_left [of c 1 b], simp)

  1736

  1737 lemma mult_le_cancel_left2:

  1738   "c * a \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)"

  1739 by (insert mult_le_cancel_left [of c a 1], simp)

  1740

  1741 lemma mult_less_cancel_right1:

  1742   "c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)"

  1743 by (insert mult_less_cancel_right [of 1 c b], simp)

  1744

  1745 lemma mult_less_cancel_right2:

  1746   "a * c < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"

  1747 by (insert mult_less_cancel_right [of a c 1], simp)

  1748

  1749 lemma mult_less_cancel_left1:

  1750   "c < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)"

  1751 by (insert mult_less_cancel_left [of c 1 b], simp)

  1752

  1753 lemma mult_less_cancel_left2:

  1754   "c * a < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"

  1755 by (insert mult_less_cancel_left [of c a 1], simp)

  1756

  1757 lemma sgn_sgn [simp]:

  1758   "sgn (sgn a) = sgn a"

  1759 unfolding sgn_if by simp

  1760

  1761 lemma sgn_0_0:

  1762   "sgn a = 0 \<longleftrightarrow> a = 0"

  1763 unfolding sgn_if by simp

  1764

  1765 lemma sgn_1_pos:

  1766   "sgn a = 1 \<longleftrightarrow> a > 0"

  1767 unfolding sgn_if by simp

  1768

  1769 lemma sgn_1_neg:

  1770   "sgn a = - 1 \<longleftrightarrow> a < 0"

  1771 unfolding sgn_if by auto

  1772

  1773 lemma sgn_pos [simp]:

  1774   "0 < a \<Longrightarrow> sgn a = 1"

  1775 unfolding sgn_1_pos .

  1776

  1777 lemma sgn_neg [simp]:

  1778   "a < 0 \<Longrightarrow> sgn a = - 1"

  1779 unfolding sgn_1_neg .

  1780

  1781 lemma sgn_times:

  1782   "sgn (a * b) = sgn a * sgn b"

  1783 by (auto simp add: sgn_if zero_less_mult_iff)

  1784

  1785 lemma abs_sgn: "\<bar>k\<bar> = k * sgn k"

  1786 unfolding sgn_if abs_if by auto

  1787

  1788 lemma sgn_greater [simp]:

  1789   "0 < sgn a \<longleftrightarrow> 0 < a"

  1790   unfolding sgn_if by auto

  1791

  1792 lemma sgn_less [simp]:

  1793   "sgn a < 0 \<longleftrightarrow> a < 0"

  1794   unfolding sgn_if by auto

  1795

  1796 lemma abs_dvd_iff [simp]: "\<bar>m\<bar> dvd k \<longleftrightarrow> m dvd k"

  1797   by (simp add: abs_if)

  1798

  1799 lemma dvd_abs_iff [simp]: "m dvd \<bar>k\<bar> \<longleftrightarrow> m dvd k"

  1800   by (simp add: abs_if)

  1801

  1802 lemma dvd_if_abs_eq:

  1803   "\<bar>l\<bar> = \<bar>k\<bar> \<Longrightarrow> l dvd k"

  1804 by(subst abs_dvd_iff[symmetric]) simp

  1805

  1806 text {* The following lemmas can be proven in more general structures, but

  1807 are dangerous as simp rules in absence of @{thm neg_equal_zero},

  1808 @{thm neg_less_pos}, @{thm neg_less_eq_nonneg}. *}

  1809

  1810 lemma equation_minus_iff_1 [simp, no_atp]:

  1811   "1 = - a \<longleftrightarrow> a = - 1"

  1812   by (fact equation_minus_iff)

  1813

  1814 lemma minus_equation_iff_1 [simp, no_atp]:

  1815   "- a = 1 \<longleftrightarrow> a = - 1"

  1816   by (subst minus_equation_iff, auto)

  1817

  1818 lemma le_minus_iff_1 [simp, no_atp]:

  1819   "1 \<le> - b \<longleftrightarrow> b \<le> - 1"

  1820   by (fact le_minus_iff)

  1821

  1822 lemma minus_le_iff_1 [simp, no_atp]:

  1823   "- a \<le> 1 \<longleftrightarrow> - 1 \<le> a"

  1824   by (fact minus_le_iff)

  1825

  1826 lemma less_minus_iff_1 [simp, no_atp]:

  1827   "1 < - b \<longleftrightarrow> b < - 1"

  1828   by (fact less_minus_iff)

  1829

  1830 lemma minus_less_iff_1 [simp, no_atp]:

  1831   "- a < 1 \<longleftrightarrow> - 1 < a"

  1832   by (fact minus_less_iff)

  1833

  1834 end

  1835

  1836 text {* Simprules for comparisons where common factors can be cancelled. *}

  1837

  1838 lemmas mult_compare_simps =

  1839     mult_le_cancel_right mult_le_cancel_left

  1840     mult_le_cancel_right1 mult_le_cancel_right2

  1841     mult_le_cancel_left1 mult_le_cancel_left2

  1842     mult_less_cancel_right mult_less_cancel_left

  1843     mult_less_cancel_right1 mult_less_cancel_right2

  1844     mult_less_cancel_left1 mult_less_cancel_left2

  1845     mult_cancel_right mult_cancel_left

  1846     mult_cancel_right1 mult_cancel_right2

  1847     mult_cancel_left1 mult_cancel_left2

  1848

  1849 text {* Reasoning about inequalities with division *}

  1850

  1851 context linordered_semidom

  1852 begin

  1853

  1854 lemma less_add_one: "a < a + 1"

  1855 proof -

  1856   have "a + 0 < a + 1"

  1857     by (blast intro: zero_less_one add_strict_left_mono)

  1858   thus ?thesis by simp

  1859 qed

  1860

  1861 lemma zero_less_two: "0 < 1 + 1"

  1862 by (blast intro: less_trans zero_less_one less_add_one)

  1863

  1864 end

  1865

  1866 context linordered_idom

  1867 begin

  1868

  1869 lemma mult_right_le_one_le:

  1870   "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> x * y \<le> x"

  1871   by (rule mult_left_le)

  1872

  1873 lemma mult_left_le_one_le:

  1874   "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> y * x \<le> x"

  1875   by (auto simp add: mult_le_cancel_right2)

  1876

  1877 end

  1878

  1879 text {* Absolute Value *}

  1880

  1881 context linordered_idom

  1882 begin

  1883

  1884 lemma mult_sgn_abs:

  1885   "sgn x * \<bar>x\<bar> = x"

  1886   unfolding abs_if sgn_if by auto

  1887

  1888 lemma abs_one [simp]:

  1889   "\<bar>1\<bar> = 1"

  1890   by (simp add: abs_if)

  1891

  1892 end

  1893

  1894 class ordered_ring_abs = ordered_ring + ordered_ab_group_add_abs +

  1895   assumes abs_eq_mult:

  1896     "(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>"

  1897

  1898 context linordered_idom

  1899 begin

  1900

  1901 subclass ordered_ring_abs proof

  1902 qed (auto simp add: abs_if not_less mult_less_0_iff)

  1903

  1904 lemma abs_mult:

  1905   "\<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>"

  1906   by (rule abs_eq_mult) auto

  1907

  1908 lemma abs_mult_self:

  1909   "\<bar>a\<bar> * \<bar>a\<bar> = a * a"

  1910   by (simp add: abs_if)

  1911

  1912 lemma abs_mult_less:

  1913   "\<bar>a\<bar> < c \<Longrightarrow> \<bar>b\<bar> < d \<Longrightarrow> \<bar>a\<bar> * \<bar>b\<bar> < c * d"

  1914 proof -

  1915   assume ac: "\<bar>a\<bar> < c"

  1916   hence cpos: "0<c" by (blast intro: le_less_trans abs_ge_zero)

  1917   assume "\<bar>b\<bar> < d"

  1918   thus ?thesis by (simp add: ac cpos mult_strict_mono)

  1919 qed

  1920

  1921 lemma abs_less_iff:

  1922   "\<bar>a\<bar> < b \<longleftrightarrow> a < b \<and> - a < b"

  1923   by (simp add: less_le abs_le_iff) (auto simp add: abs_if)

  1924

  1925 lemma abs_mult_pos:

  1926   "0 \<le> x \<Longrightarrow> \<bar>y\<bar> * x = \<bar>y * x\<bar>"

  1927   by (simp add: abs_mult)

  1928

  1929 lemma abs_diff_less_iff:

  1930   "\<bar>x - a\<bar> < r \<longleftrightarrow> a - r < x \<and> x < a + r"

  1931   by (auto simp add: diff_less_eq ac_simps abs_less_iff)

  1932

  1933 lemma abs_diff_le_iff:

  1934    "\<bar>x - a\<bar> \<le> r \<longleftrightarrow> a - r \<le> x \<and> x \<le> a + r"

  1935   by (auto simp add: diff_le_eq ac_simps abs_le_iff)

  1936

  1937 end

  1938

  1939 hide_fact (open) comm_mult_left_mono comm_mult_strict_left_mono distrib

  1940

  1941 code_identifier

  1942   code_module Rings \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith

  1943

  1944 end