src/HOL/Rings.thy
 author paulson Tue Jun 23 16:55:28 2015 +0100 (2015-06-23) changeset 60562 24af00b010cf parent 60529 24c2ef12318b child 60570 7ed2cde6806d permissions -rw-r--r--
Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
 haftmann@35050  1 (* Title: HOL/Rings.thy  wenzelm@32960  2  Author: Gertrud Bauer  wenzelm@32960  3  Author: Steven Obua  wenzelm@32960  4  Author: Tobias Nipkow  wenzelm@32960  5  Author: Lawrence C Paulson  wenzelm@32960  6  Author: Markus Wenzel  wenzelm@32960  7  Author: Jeremy Avigad  paulson@14265  8 *)  paulson@14265  9 wenzelm@58889  10 section {* Rings *}  paulson@14265  11 haftmann@35050  12 theory Rings  haftmann@35050  13 imports Groups  nipkow@15131  14 begin  paulson@14504  15 haftmann@22390  16 class semiring = ab_semigroup_add + semigroup_mult +  hoelzl@58776  17  assumes distrib_right[algebra_simps]: "(a + b) * c = a * c + b * c"  hoelzl@58776  18  assumes distrib_left[algebra_simps]: "a * (b + c) = a * b + a * c"  haftmann@25152  19 begin  haftmann@25152  20 haftmann@25152  21 text{*For the @{text combine_numerals} simproc*}  haftmann@25152  22 lemma combine_common_factor:  haftmann@25152  23  "a * e + (b * e + c) = (a + b) * e + c"  haftmann@57514  24 by (simp add: distrib_right ac_simps)  haftmann@25152  25 haftmann@25152  26 end  paulson@14504  27 haftmann@22390  28 class mult_zero = times + zero +  haftmann@25062  29  assumes mult_zero_left [simp]: "0 * a = 0"  haftmann@25062  30  assumes mult_zero_right [simp]: "a * 0 = 0"  haftmann@58195  31 begin  haftmann@58195  32 haftmann@58195  33 lemma mult_not_zero:  haftmann@58195  34  "a * b \ 0 \ a \ 0 \ b \ 0"  haftmann@58195  35  by auto  haftmann@58195  36 haftmann@58195  37 end  krauss@21199  38 haftmann@58198  39 class semiring_0 = semiring + comm_monoid_add + mult_zero  haftmann@58198  40 huffman@29904  41 class semiring_0_cancel = semiring + cancel_comm_monoid_add  haftmann@25186  42 begin  paulson@14504  43 haftmann@25186  44 subclass semiring_0  haftmann@28823  45 proof  krauss@21199  46  fix a :: 'a  webertj@49962  47  have "0 * a + 0 * a = 0 * a + 0" by (simp add: distrib_right [symmetric])  nipkow@29667  48  thus "0 * a = 0" by (simp only: add_left_cancel)  haftmann@25152  49 next  haftmann@25152  50  fix a :: 'a  webertj@49962  51  have "a * 0 + a * 0 = a * 0 + 0" by (simp add: distrib_left [symmetric])  nipkow@29667  52  thus "a * 0 = 0" by (simp only: add_left_cancel)  krauss@21199  53 qed  obua@14940  54 haftmann@25186  55 end  haftmann@25152  56 haftmann@22390  57 class comm_semiring = ab_semigroup_add + ab_semigroup_mult +  haftmann@25062  58  assumes distrib: "(a + b) * c = a * c + b * c"  haftmann@25152  59 begin  paulson@14504  60 haftmann@25152  61 subclass semiring  haftmann@28823  62 proof  obua@14738  63  fix a b c :: 'a  obua@14738  64  show "(a + b) * c = a * c + b * c" by (simp add: distrib)  haftmann@57514  65  have "a * (b + c) = (b + c) * a" by (simp add: ac_simps)  obua@14738  66  also have "... = b * a + c * a" by (simp only: distrib)  haftmann@57514  67  also have "... = a * b + a * c" by (simp add: ac_simps)  obua@14738  68  finally show "a * (b + c) = a * b + a * c" by blast  paulson@14504  69 qed  paulson@14504  70 haftmann@25152  71 end  paulson@14504  72 haftmann@25152  73 class comm_semiring_0 = comm_semiring + comm_monoid_add + mult_zero  haftmann@25152  74 begin  haftmann@25152  75 huffman@27516  76 subclass semiring_0 ..  haftmann@25152  77 haftmann@25152  78 end  paulson@14504  79 huffman@29904  80 class comm_semiring_0_cancel = comm_semiring + cancel_comm_monoid_add  haftmann@25186  81 begin  obua@14940  82 huffman@27516  83 subclass semiring_0_cancel ..  obua@14940  84 huffman@28141  85 subclass comm_semiring_0 ..  huffman@28141  86 haftmann@25186  87 end  krauss@21199  88 haftmann@22390  89 class zero_neq_one = zero + one +  haftmann@25062  90  assumes zero_neq_one [simp]: "0 \ 1"  haftmann@26193  91 begin  haftmann@26193  92 haftmann@26193  93 lemma one_neq_zero [simp]: "1 \ 0"  nipkow@29667  94 by (rule not_sym) (rule zero_neq_one)  haftmann@26193  95 haftmann@54225  96 definition of_bool :: "bool \ 'a"  haftmann@54225  97 where  lp15@60562  98  "of_bool p = (if p then 1 else 0)"  haftmann@54225  99 haftmann@54225  100 lemma of_bool_eq [simp, code]:  haftmann@54225  101  "of_bool False = 0"  haftmann@54225  102  "of_bool True = 1"  haftmann@54225  103  by (simp_all add: of_bool_def)  haftmann@54225  104 haftmann@54225  105 lemma of_bool_eq_iff:  haftmann@54225  106  "of_bool p = of_bool q \ p = q"  haftmann@54225  107  by (simp add: of_bool_def)  haftmann@54225  108 haftmann@55187  109 lemma split_of_bool [split]:  haftmann@55187  110  "P (of_bool p) \ (p \ P 1) \ (\ p \ P 0)"  haftmann@55187  111  by (cases p) simp_all  haftmann@55187  112 haftmann@55187  113 lemma split_of_bool_asm:  haftmann@55187  114  "P (of_bool p) \ \ (p \ \ P 1 \ \ p \ \ P 0)"  haftmann@55187  115  by (cases p) simp_all  lp15@60562  116 lp15@60562  117 end  paulson@14265  118 haftmann@22390  119 class semiring_1 = zero_neq_one + semiring_0 + monoid_mult  paulson@14504  120 haftmann@27651  121 text {* Abstract divisibility *}  haftmann@27651  122 haftmann@27651  123 class dvd = times  haftmann@27651  124 begin  haftmann@27651  125 nipkow@50420  126 definition dvd :: "'a \ 'a \ bool" (infix "dvd" 50) where  haftmann@37767  127  "b dvd a \ (\k. a = b * k)"  haftmann@27651  128 haftmann@27651  129 lemma dvdI [intro?]: "a = b * k \ b dvd a"  haftmann@27651  130  unfolding dvd_def ..  haftmann@27651  131 haftmann@27651  132 lemma dvdE [elim?]: "b dvd a \ (\k. a = b * k \ P) \ P"  lp15@60562  133  unfolding dvd_def by blast  haftmann@27651  134 haftmann@27651  135 end  haftmann@27651  136 haftmann@59009  137 context comm_monoid_mult  haftmann@25152  138 begin  obua@14738  139 haftmann@59009  140 subclass dvd .  haftmann@25152  141 haftmann@59009  142 lemma dvd_refl [simp]:  haftmann@59009  143  "a dvd a"  haftmann@28559  144 proof  haftmann@28559  145  show "a = a * 1" by simp  haftmann@27651  146 qed  haftmann@27651  147 haftmann@27651  148 lemma dvd_trans:  haftmann@27651  149  assumes "a dvd b" and "b dvd c"  haftmann@27651  150  shows "a dvd c"  haftmann@27651  151 proof -  haftmann@28559  152  from assms obtain v where "b = a * v" by (auto elim!: dvdE)  haftmann@28559  153  moreover from assms obtain w where "c = b * w" by (auto elim!: dvdE)  haftmann@57512  154  ultimately have "c = a * (v * w)" by (simp add: mult.assoc)  haftmann@28559  155  then show ?thesis ..  haftmann@27651  156 qed  haftmann@27651  157 haftmann@59009  158 lemma one_dvd [simp]:  haftmann@59009  159  "1 dvd a"  haftmann@59009  160  by (auto intro!: dvdI)  haftmann@28559  161 haftmann@59009  162 lemma dvd_mult [simp]:  haftmann@59009  163  "a dvd c \ a dvd (b * c)"  haftmann@59009  164  by (auto intro!: mult.left_commute dvdI elim!: dvdE)  haftmann@27651  165 haftmann@59009  166 lemma dvd_mult2 [simp]:  haftmann@59009  167  "a dvd b \ a dvd (b * c)"  lp15@60562  168  using dvd_mult [of a b c] by (simp add: ac_simps)  haftmann@27651  169 haftmann@59009  170 lemma dvd_triv_right [simp]:  haftmann@59009  171  "a dvd b * a"  haftmann@59009  172  by (rule dvd_mult) (rule dvd_refl)  haftmann@27651  173 haftmann@59009  174 lemma dvd_triv_left [simp]:  haftmann@59009  175  "a dvd a * b"  haftmann@59009  176  by (rule dvd_mult2) (rule dvd_refl)  haftmann@27651  177 haftmann@27651  178 lemma mult_dvd_mono:  nipkow@30042  179  assumes "a dvd b"  nipkow@30042  180  and "c dvd d"  haftmann@27651  181  shows "a * c dvd b * d"  haftmann@27651  182 proof -  nipkow@30042  183  from a dvd b obtain b' where "b = a * b'" ..  nipkow@30042  184  moreover from c dvd d obtain d' where "d = c * d'" ..  haftmann@57514  185  ultimately have "b * d = (a * c) * (b' * d')" by (simp add: ac_simps)  haftmann@27651  186  then show ?thesis ..  haftmann@27651  187 qed  haftmann@27651  188 haftmann@59009  189 lemma dvd_mult_left:  haftmann@59009  190  "a * b dvd c \ a dvd c"  haftmann@59009  191  by (simp add: dvd_def mult.assoc) blast  haftmann@27651  192 haftmann@59009  193 lemma dvd_mult_right:  haftmann@59009  194  "a * b dvd c \ b dvd c"  haftmann@59009  195  using dvd_mult_left [of b a c] by (simp add: ac_simps)  lp15@60562  196 haftmann@59009  197 end  haftmann@59009  198 haftmann@59009  199 class comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult  haftmann@59009  200 begin  haftmann@59009  201 haftmann@59009  202 subclass semiring_1 ..  haftmann@27651  203 haftmann@59009  204 lemma dvd_0_left_iff [simp]:  haftmann@59009  205  "0 dvd a \ a = 0"  haftmann@59009  206  by (auto intro: dvd_refl elim!: dvdE)  haftmann@27651  207 haftmann@59009  208 lemma dvd_0_right [iff]:  haftmann@59009  209  "a dvd 0"  haftmann@59009  210 proof  haftmann@59009  211  show "0 = a * 0" by simp  haftmann@59009  212 qed  haftmann@59009  213 haftmann@59009  214 lemma dvd_0_left:  haftmann@59009  215  "0 dvd a \ a = 0"  haftmann@59009  216  by simp  haftmann@59009  217 haftmann@59009  218 lemma dvd_add [simp]:  haftmann@59009  219  assumes "a dvd b" and "a dvd c"  haftmann@59009  220  shows "a dvd (b + c)"  haftmann@27651  221 proof -  nipkow@29925  222  from a dvd b obtain b' where "b = a * b'" ..  nipkow@29925  223  moreover from a dvd c obtain c' where "c = a * c'" ..  webertj@49962  224  ultimately have "b + c = a * (b' + c')" by (simp add: distrib_left)  haftmann@27651  225  then show ?thesis ..  haftmann@27651  226 qed  haftmann@27651  227 haftmann@25152  228 end  paulson@14421  229 huffman@29904  230 class semiring_1_cancel = semiring + cancel_comm_monoid_add  huffman@29904  231  + zero_neq_one + monoid_mult  haftmann@25267  232 begin  obua@14940  233 huffman@27516  234 subclass semiring_0_cancel ..  haftmann@25512  235 huffman@27516  236 subclass semiring_1 ..  haftmann@25267  237 haftmann@25267  238 end  krauss@21199  239 lp15@60562  240 class comm_semiring_1_cancel = comm_semiring + cancel_comm_monoid_add +  lp15@60562  241  zero_neq_one + comm_monoid_mult +  lp15@60562  242  assumes right_diff_distrib' [algebra_simps]: "a * (b - c) = a * b - a * c"  haftmann@25267  243 begin  obua@14738  244 huffman@27516  245 subclass semiring_1_cancel ..  huffman@27516  246 subclass comm_semiring_0_cancel ..  huffman@27516  247 subclass comm_semiring_1 ..  haftmann@25267  248 haftmann@59816  249 lemma left_diff_distrib' [algebra_simps]:  haftmann@59816  250  "(b - c) * a = b * a - c * a"  haftmann@59816  251  by (simp add: algebra_simps)  haftmann@59816  252 haftmann@59816  253 lemma dvd_add_times_triv_left_iff [simp]:  haftmann@59816  254  "a dvd c * a + b \ a dvd b"  haftmann@59816  255 proof -  haftmann@59816  256  have "a dvd a * c + b \ a dvd b" (is "?P \ ?Q")  haftmann@59816  257  proof  haftmann@59816  258  assume ?Q then show ?P by simp  haftmann@59816  259  next  haftmann@59816  260  assume ?P  haftmann@59816  261  then obtain d where "a * c + b = a * d" ..  haftmann@59816  262  then have "a * c + b - a * c = a * d - a * c" by simp  haftmann@59816  263  then have "b = a * d - a * c" by simp  lp15@60562  264  then have "b = a * (d - c)" by (simp add: algebra_simps)  haftmann@59816  265  then show ?Q ..  haftmann@59816  266  qed  haftmann@59816  267  then show "a dvd c * a + b \ a dvd b" by (simp add: ac_simps)  haftmann@59816  268 qed  haftmann@59816  269 haftmann@59816  270 lemma dvd_add_times_triv_right_iff [simp]:  haftmann@59816  271  "a dvd b + c * a \ a dvd b"  haftmann@59816  272  using dvd_add_times_triv_left_iff [of a c b] by (simp add: ac_simps)  haftmann@59816  273 haftmann@59816  274 lemma dvd_add_triv_left_iff [simp]:  haftmann@59816  275  "a dvd a + b \ a dvd b"  haftmann@59816  276  using dvd_add_times_triv_left_iff [of a 1 b] by simp  haftmann@59816  277 haftmann@59816  278 lemma dvd_add_triv_right_iff [simp]:  haftmann@59816  279  "a dvd b + a \ a dvd b"  haftmann@59816  280  using dvd_add_times_triv_right_iff [of a b 1] by simp  haftmann@59816  281 haftmann@59816  282 lemma dvd_add_right_iff:  haftmann@59816  283  assumes "a dvd b"  haftmann@59816  284  shows "a dvd b + c \ a dvd c" (is "?P \ ?Q")  haftmann@59816  285 proof  haftmann@59816  286  assume ?P then obtain d where "b + c = a * d" ..  haftmann@59816  287  moreover from a dvd b obtain e where "b = a * e" ..  haftmann@59816  288  ultimately have "a * e + c = a * d" by simp  haftmann@59816  289  then have "a * e + c - a * e = a * d - a * e" by simp  haftmann@59816  290  then have "c = a * d - a * e" by simp  haftmann@59816  291  then have "c = a * (d - e)" by (simp add: algebra_simps)  haftmann@59816  292  then show ?Q ..  haftmann@59816  293 next  haftmann@59816  294  assume ?Q with assms show ?P by simp  haftmann@59816  295 qed  haftmann@59816  296 haftmann@59816  297 lemma dvd_add_left_iff:  haftmann@59816  298  assumes "a dvd c"  haftmann@59816  299  shows "a dvd b + c \ a dvd b"  haftmann@59816  300  using assms dvd_add_right_iff [of a c b] by (simp add: ac_simps)  haftmann@59816  301 haftmann@59816  302 end  haftmann@59816  303 haftmann@22390  304 class ring = semiring + ab_group_add  haftmann@25267  305 begin  haftmann@25152  306 huffman@27516  307 subclass semiring_0_cancel ..  haftmann@25152  308 haftmann@25152  309 text {* Distribution rules *}  haftmann@25152  310 haftmann@25152  311 lemma minus_mult_left: "- (a * b) = - a * b"  lp15@60562  312 by (rule minus_unique) (simp add: distrib_right [symmetric])  haftmann@25152  313 haftmann@25152  314 lemma minus_mult_right: "- (a * b) = a * - b"  lp15@60562  315 by (rule minus_unique) (simp add: distrib_left [symmetric])  haftmann@25152  316 huffman@29407  317 text{*Extract signs from products*}  blanchet@54147  318 lemmas mult_minus_left [simp] = minus_mult_left [symmetric]  blanchet@54147  319 lemmas mult_minus_right [simp] = minus_mult_right [symmetric]  huffman@29407  320 haftmann@25152  321 lemma minus_mult_minus [simp]: "- a * - b = a * b"  nipkow@29667  322 by simp  haftmann@25152  323 haftmann@25152  324 lemma minus_mult_commute: "- a * b = a * - b"  nipkow@29667  325 by simp  nipkow@29667  326 hoelzl@58776  327 lemma right_diff_distrib [algebra_simps]:  haftmann@54230  328  "a * (b - c) = a * b - a * c"  haftmann@54230  329  using distrib_left [of a b "-c "] by simp  nipkow@29667  330 hoelzl@58776  331 lemma left_diff_distrib [algebra_simps]:  haftmann@54230  332  "(a - b) * c = a * c - b * c"  haftmann@54230  333  using distrib_right [of a "- b" c] by simp  haftmann@25152  334 blanchet@54147  335 lemmas ring_distribs =  webertj@49962  336  distrib_left distrib_right left_diff_distrib right_diff_distrib  haftmann@25152  337 haftmann@25230  338 lemma eq_add_iff1:  haftmann@25230  339  "a * e + c = b * e + d \ (a - b) * e + c = d"  nipkow@29667  340 by (simp add: algebra_simps)  haftmann@25230  341 haftmann@25230  342 lemma eq_add_iff2:  haftmann@25230  343  "a * e + c = b * e + d \ c = (b - a) * e + d"  nipkow@29667  344 by (simp add: algebra_simps)  haftmann@25230  345 haftmann@25152  346 end  haftmann@25152  347 blanchet@54147  348 lemmas ring_distribs =  webertj@49962  349  distrib_left distrib_right left_diff_distrib right_diff_distrib  haftmann@25152  350 haftmann@22390  351 class comm_ring = comm_semiring + ab_group_add  haftmann@25267  352 begin  obua@14738  353 huffman@27516  354 subclass ring ..  huffman@28141  355 subclass comm_semiring_0_cancel ..  haftmann@25267  356 huffman@44350  357 lemma square_diff_square_factored:  huffman@44350  358  "x * x - y * y = (x + y) * (x - y)"  huffman@44350  359  by (simp add: algebra_simps)  huffman@44350  360 haftmann@25267  361 end  obua@14738  362 haftmann@22390  363 class ring_1 = ring + zero_neq_one + monoid_mult  haftmann@25267  364 begin  paulson@14265  365 huffman@27516  366 subclass semiring_1_cancel ..  haftmann@25267  367 huffman@44346  368 lemma square_diff_one_factored:  huffman@44346  369  "x * x - 1 = (x + 1) * (x - 1)"  huffman@44346  370  by (simp add: algebra_simps)  huffman@44346  371 haftmann@25267  372 end  haftmann@25152  373 haftmann@22390  374 class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult  haftmann@25267  375 begin  obua@14738  376 huffman@27516  377 subclass ring_1 ..  lp15@60562  378 subclass comm_semiring_1_cancel  haftmann@59816  379  by unfold_locales (simp add: algebra_simps)  haftmann@58647  380 huffman@29465  381 lemma dvd_minus_iff [simp]: "x dvd - y \ x dvd y"  huffman@29408  382 proof  huffman@29408  383  assume "x dvd - y"  huffman@29408  384  then have "x dvd - 1 * - y" by (rule dvd_mult)  huffman@29408  385  then show "x dvd y" by simp  huffman@29408  386 next  huffman@29408  387  assume "x dvd y"  huffman@29408  388  then have "x dvd - 1 * y" by (rule dvd_mult)  huffman@29408  389  then show "x dvd - y" by simp  huffman@29408  390 qed  huffman@29408  391 huffman@29465  392 lemma minus_dvd_iff [simp]: "- x dvd y \ x dvd y"  huffman@29408  393 proof  huffman@29408  394  assume "- x dvd y"  huffman@29408  395  then obtain k where "y = - x * k" ..  huffman@29408  396  then have "y = x * - k" by simp  huffman@29408  397  then show "x dvd y" ..  huffman@29408  398 next  huffman@29408  399  assume "x dvd y"  huffman@29408  400  then obtain k where "y = x * k" ..  huffman@29408  401  then have "y = - x * - k" by simp  huffman@29408  402  then show "- x dvd y" ..  huffman@29408  403 qed  huffman@29408  404 haftmann@54230  405 lemma dvd_diff [simp]:  haftmann@54230  406  "x dvd y \ x dvd z \ x dvd (y - z)"  haftmann@54230  407  using dvd_add [of x y "- z"] by simp  huffman@29409  408 haftmann@25267  409 end  haftmann@25152  410 haftmann@59833  411 class semiring_no_zero_divisors = semiring_0 +  haftmann@59833  412  assumes no_zero_divisors: "a \ 0 \ b \ 0 \ a * b \ 0"  haftmann@25230  413 begin  haftmann@25230  414 haftmann@59833  415 lemma divisors_zero:  haftmann@59833  416  assumes "a * b = 0"  haftmann@59833  417  shows "a = 0 \ b = 0"  haftmann@59833  418 proof (rule classical)  haftmann@59833  419  assume "\ (a = 0 \ b = 0)"  haftmann@59833  420  then have "a \ 0" and "b \ 0" by auto  haftmann@59833  421  with no_zero_divisors have "a * b \ 0" by blast  haftmann@59833  422  with assms show ?thesis by simp  haftmann@59833  423 qed  haftmann@59833  424 haftmann@25230  425 lemma mult_eq_0_iff [simp]:  haftmann@58952  426  shows "a * b = 0 \ a = 0 \ b = 0"  haftmann@25230  427 proof (cases "a = 0 \ b = 0")  haftmann@25230  428  case False then have "a \ 0" and "b \ 0" by auto  haftmann@25230  429  then show ?thesis using no_zero_divisors by simp  haftmann@25230  430 next  haftmann@25230  431  case True then show ?thesis by auto  haftmann@25230  432 qed  haftmann@25230  433 haftmann@58952  434 end  haftmann@58952  435 haftmann@60516  436 class semiring_no_zero_divisors_cancel = semiring_no_zero_divisors +  haftmann@60516  437  assumes mult_cancel_right [simp]: "a * c = b * c \ c = 0 \ a = b"  haftmann@60516  438  and mult_cancel_left [simp]: "c * a = c * b \ c = 0 \ a = b"  haftmann@58952  439 begin  haftmann@58952  440 haftmann@58952  441 lemma mult_left_cancel:  haftmann@58952  442  "c \ 0 \ c * a = c * b \ a = b"  lp15@60562  443  by simp  lp15@56217  444 haftmann@58952  445 lemma mult_right_cancel:  haftmann@58952  446  "c \ 0 \ a * c = b * c \ a = b"  lp15@60562  447  by simp  lp15@56217  448 haftmann@25230  449 end  huffman@22990  450 haftmann@60516  451 class ring_no_zero_divisors = ring + semiring_no_zero_divisors  haftmann@60516  452 begin  haftmann@60516  453 haftmann@60516  454 subclass semiring_no_zero_divisors_cancel  haftmann@60516  455 proof  haftmann@60516  456  fix a b c  haftmann@60516  457  have "a * c = b * c \ (a - b) * c = 0"  haftmann@60516  458  by (simp add: algebra_simps)  haftmann@60516  459  also have "\ \ c = 0 \ a = b"  haftmann@60516  460  by auto  haftmann@60516  461  finally show "a * c = b * c \ c = 0 \ a = b" .  haftmann@60516  462  have "c * a = c * b \ c * (a - b) = 0"  haftmann@60516  463  by (simp add: algebra_simps)  haftmann@60516  464  also have "\ \ c = 0 \ a = b"  haftmann@60516  465  by auto  haftmann@60516  466  finally show "c * a = c * b \ c = 0 \ a = b" .  haftmann@60516  467 qed  haftmann@60516  468 haftmann@60516  469 end  haftmann@60516  470 huffman@23544  471 class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors  haftmann@26274  472 begin  haftmann@26274  473 huffman@36970  474 lemma square_eq_1_iff:  huffman@36821  475  "x * x = 1 \ x = 1 \ x = - 1"  huffman@36821  476 proof -  huffman@36821  477  have "(x - 1) * (x + 1) = x * x - 1"  huffman@36821  478  by (simp add: algebra_simps)  huffman@36821  479  hence "x * x = 1 \ (x - 1) * (x + 1) = 0"  huffman@36821  480  by simp  huffman@36821  481  thus ?thesis  huffman@36821  482  by (simp add: eq_neg_iff_add_eq_0)  huffman@36821  483 qed  huffman@36821  484 haftmann@26274  485 lemma mult_cancel_right1 [simp]:  haftmann@26274  486  "c = b * c \ c = 0 \ b = 1"  nipkow@29667  487 by (insert mult_cancel_right [of 1 c b], force)  haftmann@26274  488 haftmann@26274  489 lemma mult_cancel_right2 [simp]:  haftmann@26274  490  "a * c = c \ c = 0 \ a = 1"  nipkow@29667  491 by (insert mult_cancel_right [of a c 1], simp)  lp15@60562  492 haftmann@26274  493 lemma mult_cancel_left1 [simp]:  haftmann@26274  494  "c = c * b \ c = 0 \ b = 1"  nipkow@29667  495 by (insert mult_cancel_left [of c 1 b], force)  haftmann@26274  496 haftmann@26274  497 lemma mult_cancel_left2 [simp]:  haftmann@26274  498  "c * a = c \ c = 0 \ a = 1"  nipkow@29667  499 by (insert mult_cancel_left [of c a 1], simp)  haftmann@26274  500 haftmann@26274  501 end  huffman@22990  502 lp15@60562  503 class semidom = comm_semiring_1_cancel + semiring_no_zero_divisors  haftmann@59833  504 haftmann@59833  505 class idom = comm_ring_1 + semiring_no_zero_divisors  haftmann@25186  506 begin  paulson@14421  507 haftmann@59833  508 subclass semidom ..  haftmann@59833  509 huffman@27516  510 subclass ring_1_no_zero_divisors ..  huffman@22990  511 huffman@29981  512 lemma dvd_mult_cancel_right [simp]:  huffman@29981  513  "a * c dvd b * c \ c = 0 \ a dvd b"  huffman@29981  514 proof -  huffman@29981  515  have "a * c dvd b * c \ (\k. b * c = (a * k) * c)"  haftmann@57514  516  unfolding dvd_def by (simp add: ac_simps)  huffman@29981  517  also have "(\k. b * c = (a * k) * c) \ c = 0 \ a dvd b"  huffman@29981  518  unfolding dvd_def by simp  huffman@29981  519  finally show ?thesis .  huffman@29981  520 qed  huffman@29981  521 huffman@29981  522 lemma dvd_mult_cancel_left [simp]:  huffman@29981  523  "c * a dvd c * b \ c = 0 \ a dvd b"  huffman@29981  524 proof -  huffman@29981  525  have "c * a dvd c * b \ (\k. b * c = (a * k) * c)"  haftmann@57514  526  unfolding dvd_def by (simp add: ac_simps)  huffman@29981  527  also have "(\k. b * c = (a * k) * c) \ c = 0 \ a dvd b"  huffman@29981  528  unfolding dvd_def by simp  huffman@29981  529  finally show ?thesis .  huffman@29981  530 qed  huffman@29981  531 haftmann@60516  532 lemma square_eq_iff: "a * a = b * b \ a = b \ a = - b"  haftmann@59833  533 proof  haftmann@59833  534  assume "a * a = b * b"  haftmann@59833  535  then have "(a - b) * (a + b) = 0"  haftmann@59833  536  by (simp add: algebra_simps)  haftmann@59833  537  then show "a = b \ a = - b"  haftmann@59833  538  by (simp add: eq_neg_iff_add_eq_0)  haftmann@59833  539 next  haftmann@59833  540  assume "a = b \ a = - b"  haftmann@59833  541  then show "a * a = b * b" by auto  haftmann@59833  542 qed  haftmann@59833  543 haftmann@25186  544 end  haftmann@25152  545 haftmann@35302  546 text {*  haftmann@35302  547  The theory of partially ordered rings is taken from the books:  haftmann@35302  548  \begin{itemize}  lp15@60562  549  \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979  haftmann@35302  550  \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963  haftmann@35302  551  \end{itemize}  lp15@60562  552  Most of the used notions can also be looked up in  haftmann@35302  553  \begin{itemize}  wenzelm@54703  554  \item @{url "http://www.mathworld.com"} by Eric Weisstein et. al.  haftmann@35302  555  \item \emph{Algebra I} by van der Waerden, Springer.  haftmann@35302  556  \end{itemize}  haftmann@35302  557 *}  haftmann@35302  558 haftmann@60353  559 class divide =  haftmann@60429  560  fixes divide :: "'a \ 'a \ 'a" (infixl "div" 70)  haftmann@60353  561 haftmann@60353  562 setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a \ 'a \ 'a"}) *}  haftmann@60353  563 haftmann@60353  564 context semiring  haftmann@60353  565 begin  haftmann@60353  566 haftmann@60353  567 lemma [field_simps]:  haftmann@60429  568  shows distrib_left_NO_MATCH: "NO_MATCH (x div y) a \ a * (b + c) = a * b + a * c"  haftmann@60429  569  and distrib_right_NO_MATCH: "NO_MATCH (x div y) c \ (a + b) * c = a * c + b * c"  haftmann@60353  570  by (rule distrib_left distrib_right)+  haftmann@60353  571 haftmann@60353  572 end  haftmann@60353  573 haftmann@60353  574 context ring  haftmann@60353  575 begin  haftmann@60353  576 haftmann@60353  577 lemma [field_simps]:  haftmann@60429  578  shows left_diff_distrib_NO_MATCH: "NO_MATCH (x div y) c \ (a - b) * c = a * c - b * c"  haftmann@60429  579  and right_diff_distrib_NO_MATCH: "NO_MATCH (x div y) a \ a * (b - c) = a * b - a * c"  haftmann@60353  580  by (rule left_diff_distrib right_diff_distrib)+  haftmann@60353  581 haftmann@60353  582 end  haftmann@60353  583 haftmann@60353  584 setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a::divide \ 'a \ 'a"}) *}  haftmann@60353  585 haftmann@60353  586 class semidom_divide = semidom + divide +  haftmann@60429  587  assumes nonzero_mult_divide_cancel_right [simp]: "b \ 0 \ (a * b) div b = a"  haftmann@60429  588  assumes divide_zero [simp]: "a div 0 = 0"  haftmann@60353  589 begin  haftmann@60353  590 haftmann@60353  591 lemma nonzero_mult_divide_cancel_left [simp]:  haftmann@60429  592  "a \ 0 \ (a * b) div a = b"  haftmann@60353  593  using nonzero_mult_divide_cancel_right [of a b] by (simp add: ac_simps)  haftmann@60353  594 haftmann@60516  595 subclass semiring_no_zero_divisors_cancel  haftmann@60516  596 proof  haftmann@60516  597  fix a b c  haftmann@60516  598  { fix a b c  haftmann@60516  599  show "a * c = b * c \ c = 0 \ a = b"  haftmann@60516  600  proof (cases "c = 0")  haftmann@60516  601  case True then show ?thesis by simp  haftmann@60516  602  next  haftmann@60516  603  case False  haftmann@60516  604  { assume "a * c = b * c"  haftmann@60516  605  then have "a * c div c = b * c div c"  haftmann@60516  606  by simp  haftmann@60516  607  with False have "a = b"  haftmann@60516  608  by simp  haftmann@60516  609  } then show ?thesis by auto  haftmann@60516  610  qed  haftmann@60516  611  }  haftmann@60516  612  from this [of a c b]  haftmann@60516  613  show "c * a = c * b \ c = 0 \ a = b"  haftmann@60516  614  by (simp add: ac_simps)  haftmann@60516  615 qed  haftmann@60516  616 haftmann@60516  617 lemma div_self [simp]:  haftmann@60516  618  assumes "a \ 0"  haftmann@60516  619  shows "a div a = 1"  haftmann@60516  620  using assms nonzero_mult_divide_cancel_left [of a 1] by simp  haftmann@60516  621 haftmann@60353  622 end  haftmann@60353  623 haftmann@60353  624 class idom_divide = idom + semidom_divide  haftmann@60353  625 haftmann@60517  626 class algebraic_semidom = semidom_divide  haftmann@60517  627 begin  haftmann@60517  628 haftmann@60517  629 lemma dvd_div_mult_self [simp]:  haftmann@60517  630  "a dvd b \ b div a * a = b"  haftmann@60517  631  by (cases "a = 0") (auto elim: dvdE simp add: ac_simps)  haftmann@60517  632 haftmann@60517  633 lemma dvd_mult_div_cancel [simp]:  haftmann@60517  634  "a dvd b \ a * (b div a) = b"  haftmann@60517  635  using dvd_div_mult_self [of a b] by (simp add: ac_simps)  lp15@60562  636 haftmann@60517  637 lemma div_mult_swap:  haftmann@60517  638  assumes "c dvd b"  haftmann@60517  639  shows "a * (b div c) = (a * b) div c"  haftmann@60517  640 proof (cases "c = 0")  haftmann@60517  641  case True then show ?thesis by simp  haftmann@60517  642 next  haftmann@60517  643  case False from assms obtain d where "b = c * d" ..  haftmann@60517  644  moreover from False have "a * divide (d * c) c = ((a * d) * c) div c"  haftmann@60517  645  by simp  haftmann@60517  646  ultimately show ?thesis by (simp add: ac_simps)  haftmann@60517  647 qed  haftmann@60517  648 haftmann@60517  649 lemma dvd_div_mult:  haftmann@60517  650  assumes "c dvd b"  haftmann@60517  651  shows "b div c * a = (b * a) div c"  haftmann@60517  652  using assms div_mult_swap [of c b a] by (simp add: ac_simps)  haftmann@60517  653 lp15@60562  654 haftmann@60517  655 text \Units: invertible elements in a ring\  haftmann@60517  656 haftmann@60517  657 abbreviation is_unit :: "'a \ bool"  haftmann@60517  658 where  haftmann@60517  659  "is_unit a \ a dvd 1"  haftmann@60517  660 haftmann@60517  661 lemma not_is_unit_0 [simp]:  haftmann@60517  662  "\ is_unit 0"  haftmann@60517  663  by simp  haftmann@60517  664 lp15@60562  665 lemma unit_imp_dvd [dest]:  haftmann@60517  666  "is_unit b \ b dvd a"  haftmann@60517  667  by (rule dvd_trans [of _ 1]) simp_all  haftmann@60517  668 haftmann@60517  669 lemma unit_dvdE:  haftmann@60517  670  assumes "is_unit a"  haftmann@60517  671  obtains c where "a \ 0" and "b = a * c"  haftmann@60517  672 proof -  haftmann@60517  673  from assms have "a dvd b" by auto  haftmann@60517  674  then obtain c where "b = a * c" ..  haftmann@60517  675  moreover from assms have "a \ 0" by auto  haftmann@60517  676  ultimately show thesis using that by blast  haftmann@60517  677 qed  haftmann@60517  678 haftmann@60517  679 lemma dvd_unit_imp_unit:  haftmann@60517  680  "a dvd b \ is_unit b \ is_unit a"  haftmann@60517  681  by (rule dvd_trans)  haftmann@60517  682 haftmann@60517  683 lemma unit_div_1_unit [simp, intro]:  haftmann@60517  684  assumes "is_unit a"  haftmann@60517  685  shows "is_unit (1 div a)"  haftmann@60517  686 proof -  haftmann@60517  687  from assms have "1 = 1 div a * a" by simp  haftmann@60517  688  then show "is_unit (1 div a)" by (rule dvdI)  haftmann@60517  689 qed  haftmann@60517  690 haftmann@60517  691 lemma is_unitE [elim?]:  haftmann@60517  692  assumes "is_unit a"  haftmann@60517  693  obtains b where "a \ 0" and "b \ 0"  haftmann@60517  694  and "is_unit b" and "1 div a = b" and "1 div b = a"  haftmann@60517  695  and "a * b = 1" and "c div a = c * b"  haftmann@60517  696 proof (rule that)  haftmann@60517  697  def b \ "1 div a"  haftmann@60517  698  then show "1 div a = b" by simp  haftmann@60517  699  from b_def is_unit a show "is_unit b" by simp  haftmann@60517  700  from is_unit a and is_unit b show "a \ 0" and "b \ 0" by auto  haftmann@60517  701  from b_def is_unit a show "a * b = 1" by simp  haftmann@60517  702  then have "1 = a * b" ..  haftmann@60517  703  with b_def b \ 0 show "1 div b = a" by simp  haftmann@60517  704  from is_unit a have "a dvd c" ..  haftmann@60517  705  then obtain d where "c = a * d" ..  haftmann@60517  706  with a \ 0 a * b = 1 show "c div a = c * b"  haftmann@60517  707  by (simp add: mult.assoc mult.left_commute [of a])  haftmann@60517  708 qed  haftmann@60517  709 haftmann@60517  710 lemma unit_prod [intro]:  haftmann@60517  711  "is_unit a \ is_unit b \ is_unit (a * b)"  lp15@60562  712  by (subst mult_1_left [of 1, symmetric]) (rule mult_dvd_mono)  lp15@60562  713 haftmann@60517  714 lemma unit_div [intro]:  haftmann@60517  715  "is_unit a \ is_unit b \ is_unit (a div b)"  haftmann@60517  716  by (erule is_unitE [of b a]) (simp add: ac_simps unit_prod)  haftmann@60517  717 haftmann@60517  718 lemma mult_unit_dvd_iff:  haftmann@60517  719  assumes "is_unit b"  haftmann@60517  720  shows "a * b dvd c \ a dvd c"  haftmann@60517  721 proof  haftmann@60517  722  assume "a * b dvd c"  haftmann@60517  723  with assms show "a dvd c"  haftmann@60517  724  by (simp add: dvd_mult_left)  haftmann@60517  725 next  haftmann@60517  726  assume "a dvd c"  haftmann@60517  727  then obtain k where "c = a * k" ..  haftmann@60517  728  with assms have "c = (a * b) * (1 div b * k)"  haftmann@60517  729  by (simp add: mult_ac)  haftmann@60517  730  then show "a * b dvd c" by (rule dvdI)  haftmann@60517  731 qed  haftmann@60517  732 haftmann@60517  733 lemma dvd_mult_unit_iff:  haftmann@60517  734  assumes "is_unit b"  haftmann@60517  735  shows "a dvd c * b \ a dvd c"  haftmann@60517  736 proof  haftmann@60517  737  assume "a dvd c * b"  haftmann@60517  738  with assms have "c * b dvd c * (b * (1 div b))"  haftmann@60517  739  by (subst mult_assoc [symmetric]) simp  haftmann@60517  740  also from is_unit b have "b * (1 div b) = 1" by (rule is_unitE) simp  haftmann@60517  741  finally have "c * b dvd c" by simp  haftmann@60517  742  with a dvd c * b show "a dvd c" by (rule dvd_trans)  haftmann@60517  743 next  haftmann@60517  744  assume "a dvd c"  haftmann@60517  745  then show "a dvd c * b" by simp  haftmann@60517  746 qed  haftmann@60517  747 haftmann@60517  748 lemma div_unit_dvd_iff:  haftmann@60517  749  "is_unit b \ a div b dvd c \ a dvd c"  haftmann@60517  750  by (erule is_unitE [of _ a]) (auto simp add: mult_unit_dvd_iff)  haftmann@60517  751 haftmann@60517  752 lemma dvd_div_unit_iff:  haftmann@60517  753  "is_unit b \ a dvd c div b \ a dvd c"  haftmann@60517  754  by (erule is_unitE [of _ c]) (simp add: dvd_mult_unit_iff)  haftmann@60517  755 haftmann@60517  756 lemmas unit_dvd_iff = mult_unit_dvd_iff div_unit_dvd_iff  haftmann@60517  757  dvd_mult_unit_iff dvd_div_unit_iff -- \FIXME consider fact collection\  haftmann@60517  758 haftmann@60517  759 lemma unit_mult_div_div [simp]:  haftmann@60517  760  "is_unit a \ b * (1 div a) = b div a"  haftmann@60517  761  by (erule is_unitE [of _ b]) simp  haftmann@60517  762 haftmann@60517  763 lemma unit_div_mult_self [simp]:  haftmann@60517  764  "is_unit a \ b div a * a = b"  haftmann@60517  765  by (rule dvd_div_mult_self) auto  haftmann@60517  766 haftmann@60517  767 lemma unit_div_1_div_1 [simp]:  haftmann@60517  768  "is_unit a \ 1 div (1 div a) = a"  haftmann@60517  769  by (erule is_unitE) simp  haftmann@60517  770 haftmann@60517  771 lemma unit_div_mult_swap:  haftmann@60517  772  "is_unit c \ a * (b div c) = (a * b) div c"  haftmann@60517  773  by (erule unit_dvdE [of _ b]) (simp add: mult.left_commute [of _ c])  haftmann@60517  774 haftmann@60517  775 lemma unit_div_commute:  haftmann@60517  776  "is_unit b \ (a div b) * c = (a * c) div b"  haftmann@60517  777  using unit_div_mult_swap [of b c a] by (simp add: ac_simps)  haftmann@60517  778 haftmann@60517  779 lemma unit_eq_div1:  haftmann@60517  780  "is_unit b \ a div b = c \ a = c * b"  haftmann@60517  781  by (auto elim: is_unitE)  haftmann@60517  782 haftmann@60517  783 lemma unit_eq_div2:  haftmann@60517  784  "is_unit b \ a = c div b \ a * b = c"  haftmann@60517  785  using unit_eq_div1 [of b c a] by auto  haftmann@60517  786 haftmann@60517  787 lemma unit_mult_left_cancel:  haftmann@60517  788  assumes "is_unit a"  haftmann@60517  789  shows "a * b = a * c \ b = c" (is "?P \ ?Q")  lp15@60562  790  using assms mult_cancel_left [of a b c] by auto  haftmann@60517  791 haftmann@60517  792 lemma unit_mult_right_cancel:  haftmann@60517  793  "is_unit a \ b * a = c * a \ b = c"  haftmann@60517  794  using unit_mult_left_cancel [of a b c] by (auto simp add: ac_simps)  haftmann@60517  795 haftmann@60517  796 lemma unit_div_cancel:  haftmann@60517  797  assumes "is_unit a"  haftmann@60517  798  shows "b div a = c div a \ b = c"  haftmann@60517  799 proof -  haftmann@60517  800  from assms have "is_unit (1 div a)" by simp  haftmann@60517  801  then have "b * (1 div a) = c * (1 div a) \ b = c"  haftmann@60517  802  by (rule unit_mult_right_cancel)  haftmann@60517  803  with assms show ?thesis by simp  haftmann@60517  804 qed  lp15@60562  805 haftmann@60517  806 wenzelm@60529  807 text \Associated elements in a ring --- an equivalence relation induced  wenzelm@60529  808  by the quasi-order divisibility.\  haftmann@60517  809 lp15@60562  810 definition associated :: "'a \ 'a \ bool"  haftmann@60517  811 where  haftmann@60517  812  "associated a b \ a dvd b \ b dvd a"  haftmann@60517  813 haftmann@60517  814 lemma associatedI:  haftmann@60517  815  "a dvd b \ b dvd a \ associated a b"  haftmann@60517  816  by (simp add: associated_def)  haftmann@60517  817 haftmann@60517  818 lemma associatedD1:  haftmann@60517  819  "associated a b \ a dvd b"  haftmann@60517  820  by (simp add: associated_def)  haftmann@60517  821 haftmann@60517  822 lemma associatedD2:  haftmann@60517  823  "associated a b \ b dvd a"  haftmann@60517  824  by (simp add: associated_def)  haftmann@60517  825 haftmann@60517  826 lemma associated_refl [simp]:  haftmann@60517  827  "associated a a"  haftmann@60517  828  by (auto intro: associatedI)  haftmann@60517  829 haftmann@60517  830 lemma associated_sym:  haftmann@60517  831  "associated b a \ associated a b"  haftmann@60517  832  by (auto intro: associatedI dest: associatedD1 associatedD2)  haftmann@60517  833 haftmann@60517  834 lemma associated_trans:  haftmann@60517  835  "associated a b \ associated b c \ associated a c"  haftmann@60517  836  by (auto intro: associatedI dvd_trans dest: associatedD1 associatedD2)  haftmann@60517  837 haftmann@60517  838 lemma associated_0 [simp]:  haftmann@60517  839  "associated 0 b \ b = 0"  haftmann@60517  840  "associated a 0 \ a = 0"  haftmann@60517  841  by (auto dest: associatedD1 associatedD2)  haftmann@60517  842 haftmann@60517  843 lemma associated_unit:  haftmann@60517  844  "associated a b \ is_unit a \ is_unit b"  haftmann@60517  845  using dvd_unit_imp_unit by (auto dest!: associatedD1 associatedD2)  haftmann@60517  846 haftmann@60517  847 lemma is_unit_associatedI:  haftmann@60517  848  assumes "is_unit c" and "a = c * b"  haftmann@60517  849  shows "associated a b"  haftmann@60517  850 proof (rule associatedI)  haftmann@60517  851  from a = c * b show "b dvd a" by auto  haftmann@60517  852  from is_unit c obtain d where "c * d = 1" by (rule is_unitE)  haftmann@60517  853  moreover from a = c * b have "d * a = d * (c * b)" by simp  haftmann@60517  854  ultimately have "b = a * d" by (simp add: ac_simps)  haftmann@60517  855  then show "a dvd b" ..  haftmann@60517  856 qed  haftmann@60517  857 haftmann@60517  858 lemma associated_is_unitE:  haftmann@60517  859  assumes "associated a b"  haftmann@60517  860  obtains c where "is_unit c" and "a = c * b"  haftmann@60517  861 proof (cases "b = 0")  haftmann@60517  862  case True with assms have "is_unit 1" and "a = 1 * b" by simp_all  haftmann@60517  863  with that show thesis .  haftmann@60517  864 next  haftmann@60517  865  case False  haftmann@60517  866  from assms have "a dvd b" and "b dvd a" by (auto dest: associatedD1 associatedD2)  haftmann@60517  867  then obtain c d where "b = a * d" and "a = b * c" by (blast elim: dvdE)  haftmann@60517  868  then have "a = c * b" and "(c * d) * b = 1 * b" by (simp_all add: ac_simps)  haftmann@60517  869  with False have "c * d = 1" using mult_cancel_right [of "c * d" b 1] by simp  haftmann@60517  870  then have "is_unit c" by auto  haftmann@60517  871  with a = c * b that show thesis by blast  haftmann@60517  872 qed  lp15@60562  873 lp15@60562  874 lemmas unit_simps = mult_unit_dvd_iff div_unit_dvd_iff dvd_mult_unit_iff  haftmann@60517  875  dvd_div_unit_iff unit_div_mult_swap unit_div_commute  lp15@60562  876  unit_mult_left_cancel unit_mult_right_cancel unit_div_cancel  haftmann@60517  877  unit_eq_div1 unit_eq_div2  haftmann@60517  878 haftmann@60517  879 end  haftmann@60517  880 haftmann@38642  881 class ordered_semiring = semiring + comm_monoid_add + ordered_ab_semigroup_add +  haftmann@38642  882  assumes mult_left_mono: "a \ b \ 0 \ c \ c * a \ c * b"  haftmann@38642  883  assumes mult_right_mono: "a \ b \ 0 \ c \ a * c \ b * c"  haftmann@25230  884 begin  haftmann@25230  885 haftmann@25230  886 lemma mult_mono:  haftmann@38642  887  "a \ b \ c \ d \ 0 \ b \ 0 \ c \ a * c \ b * d"  haftmann@25230  888 apply (erule mult_right_mono [THEN order_trans], assumption)  haftmann@25230  889 apply (erule mult_left_mono, assumption)  haftmann@25230  890 done  haftmann@25230  891 haftmann@25230  892 lemma mult_mono':  haftmann@38642  893  "a \ b \ c \ d \ 0 \ a \ 0 \ c \ a * c \ b * d"  haftmann@25230  894 apply (rule mult_mono)  haftmann@25230  895 apply (fast intro: order_trans)+  haftmann@25230  896 done  haftmann@25230  897 haftmann@25230  898 end  krauss@21199  899 haftmann@38642  900 class ordered_cancel_semiring = ordered_semiring + cancel_comm_monoid_add  haftmann@25267  901 begin  paulson@14268  902 huffman@27516  903 subclass semiring_0_cancel ..  obua@23521  904 nipkow@56536  905 lemma mult_nonneg_nonneg[simp]: "0 \ a \ 0 \ b \ 0 \ a * b"  haftmann@36301  906 using mult_left_mono [of 0 b a] by simp  haftmann@25230  907 haftmann@25230  908 lemma mult_nonneg_nonpos: "0 \ a \ b \ 0 \ a * b \ 0"  haftmann@36301  909 using mult_left_mono [of b 0 a] by simp  huffman@30692  910 huffman@30692  911 lemma mult_nonpos_nonneg: "a \ 0 \ 0 \ b \ a * b \ 0"  haftmann@36301  912 using mult_right_mono [of a 0 b] by simp  huffman@30692  913 huffman@30692  914 text {* Legacy - use @{text mult_nonpos_nonneg} *}  lp15@60562  915 lemma mult_nonneg_nonpos2: "0 \ a \ b \ 0 \ b * a \ 0"  haftmann@36301  916 by (drule mult_right_mono [of b 0], auto)  haftmann@25230  917 lp15@60562  918 lemma split_mult_neg_le: "(0 \ a & b \ 0) | (a \ 0 & 0 \ b) \ a * b \ 0"  nipkow@29667  919 by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)  haftmann@25230  920 haftmann@25230  921 end  haftmann@25230  922 haftmann@38642  923 class linordered_semiring = ordered_semiring + linordered_cancel_ab_semigroup_add  haftmann@25267  924 begin  haftmann@25230  925 haftmann@35028  926 subclass ordered_cancel_semiring ..  haftmann@35028  927 haftmann@35028  928 subclass ordered_comm_monoid_add ..  haftmann@25304  929 haftmann@25230  930 lemma mult_left_less_imp_less:  haftmann@25230  931  "c * a < c * b \ 0 \ c \ a < b"  nipkow@29667  932 by (force simp add: mult_left_mono not_le [symmetric])  lp15@60562  933 haftmann@25230  934 lemma mult_right_less_imp_less:  haftmann@25230  935  "a * c < b * c \ 0 \ c \ a < b"  nipkow@29667  936 by (force simp add: mult_right_mono not_le [symmetric])  obua@23521  937 haftmann@25186  938 end  haftmann@25152  939 haftmann@35043  940 class linordered_semiring_1 = linordered_semiring + semiring_1  hoelzl@36622  941 begin  hoelzl@36622  942 hoelzl@36622  943 lemma convex_bound_le:  hoelzl@36622  944  assumes "x \ a" "y \ a" "0 \ u" "0 \ v" "u + v = 1"  hoelzl@36622  945  shows "u * x + v * y \ a"  hoelzl@36622  946 proof-  hoelzl@36622  947  from assms have "u * x + v * y \ u * a + v * a"  hoelzl@36622  948  by (simp add: add_mono mult_left_mono)  webertj@49962  949  thus ?thesis using assms unfolding distrib_right[symmetric] by simp  hoelzl@36622  950 qed  hoelzl@36622  951 hoelzl@36622  952 end  haftmann@35043  953 haftmann@35043  954 class linordered_semiring_strict = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add +  haftmann@25062  955  assumes mult_strict_left_mono: "a < b \ 0 < c \ c * a < c * b"  haftmann@25062  956  assumes mult_strict_right_mono: "a < b \ 0 < c \ a * c < b * c"  haftmann@25267  957 begin  paulson@14341  958 huffman@27516  959 subclass semiring_0_cancel ..  obua@14940  960 haftmann@35028  961 subclass linordered_semiring  haftmann@28823  962 proof  huffman@23550  963  fix a b c :: 'a  huffman@23550  964  assume A: "a \ b" "0 \ c"  huffman@23550  965  from A show "c * a \ c * b"  haftmann@25186  966  unfolding le_less  haftmann@25186  967  using mult_strict_left_mono by (cases "c = 0") auto  huffman@23550  968  from A show "a * c \ b * c"  haftmann@25152  969  unfolding le_less  haftmann@25186  970  using mult_strict_right_mono by (cases "c = 0") auto  haftmann@25152  971 qed  haftmann@25152  972 haftmann@25230  973 lemma mult_left_le_imp_le:  haftmann@25230  974  "c * a \ c * b \ 0 < c \ a \ b"  nipkow@29667  975 by (force simp add: mult_strict_left_mono _not_less [symmetric])  lp15@60562  976 haftmann@25230  977 lemma mult_right_le_imp_le:  haftmann@25230  978  "a * c \ b * c \ 0 < c \ a \ b"  nipkow@29667  979 by (force simp add: mult_strict_right_mono not_less [symmetric])  haftmann@25230  980 nipkow@56544  981 lemma mult_pos_pos[simp]: "0 < a \ 0 < b \ 0 < a * b"  haftmann@36301  982 using mult_strict_left_mono [of 0 b a] by simp  huffman@30692  983 huffman@30692  984 lemma mult_pos_neg: "0 < a \ b < 0 \ a * b < 0"  haftmann@36301  985 using mult_strict_left_mono [of b 0 a] by simp  huffman@30692  986 huffman@30692  987 lemma mult_neg_pos: "a < 0 \ 0 < b \ a * b < 0"  haftmann@36301  988 using mult_strict_right_mono [of a 0 b] by simp  huffman@30692  989 huffman@30692  990 text {* Legacy - use @{text mult_neg_pos} *}  lp15@60562  991 lemma mult_pos_neg2: "0 < a \ b < 0 \ b * a < 0"  haftmann@36301  992 by (drule mult_strict_right_mono [of b 0], auto)  haftmann@25230  993 haftmann@25230  994 lemma zero_less_mult_pos:  haftmann@25230  995  "0 < a * b \ 0 < a \ 0 < b"  huffman@30692  996 apply (cases "b\0")  haftmann@25230  997  apply (auto simp add: le_less not_less)  huffman@30692  998 apply (drule_tac mult_pos_neg [of a b])  haftmann@25230  999  apply (auto dest: less_not_sym)  haftmann@25230  1000 done  haftmann@25230  1001 haftmann@25230  1002 lemma zero_less_mult_pos2:  haftmann@25230  1003  "0 < b * a \ 0 < a \ 0 < b"  huffman@30692  1004 apply (cases "b\0")  haftmann@25230  1005  apply (auto simp add: le_less not_less)  huffman@30692  1006 apply (drule_tac mult_pos_neg2 [of a b])  haftmann@25230  1007  apply (auto dest: less_not_sym)  haftmann@25230  1008 done  haftmann@25230  1009 haftmann@26193  1010 text{*Strict monotonicity in both arguments*}  haftmann@26193  1011 lemma mult_strict_mono:  haftmann@26193  1012  assumes "a < b" and "c < d" and "0 < b" and "0 \ c"  haftmann@26193  1013  shows "a * c < b * d"  haftmann@26193  1014  using assms apply (cases "c=0")  nipkow@56544  1015  apply (simp)  haftmann@26193  1016  apply (erule mult_strict_right_mono [THEN less_trans])  huffman@30692  1017  apply (force simp add: le_less)  haftmann@26193  1018  apply (erule mult_strict_left_mono, assumption)  haftmann@26193  1019  done  haftmann@26193  1020 haftmann@26193  1021 text{*This weaker variant has more natural premises*}  haftmann@26193  1022 lemma mult_strict_mono':  haftmann@26193  1023  assumes "a < b" and "c < d" and "0 \ a" and "0 \ c"  haftmann@26193  1024  shows "a * c < b * d"  nipkow@29667  1025 by (rule mult_strict_mono) (insert assms, auto)  haftmann@26193  1026 haftmann@26193  1027 lemma mult_less_le_imp_less:  haftmann@26193  1028  assumes "a < b" and "c \ d" and "0 \ a" and "0 < c"  haftmann@26193  1029  shows "a * c < b * d"  haftmann@26193  1030  using assms apply (subgoal_tac "a * c < b * c")  haftmann@26193  1031  apply (erule less_le_trans)  haftmann@26193  1032  apply (erule mult_left_mono)  haftmann@26193  1033  apply simp  haftmann@26193  1034  apply (erule mult_strict_right_mono)  haftmann@26193  1035  apply assumption  haftmann@26193  1036  done  haftmann@26193  1037 haftmann@26193  1038 lemma mult_le_less_imp_less:  haftmann@26193  1039  assumes "a \ b" and "c < d" and "0 < a" and "0 \ c"  haftmann@26193  1040  shows "a * c < b * d"  haftmann@26193  1041  using assms apply (subgoal_tac "a * c \ b * c")  haftmann@26193  1042  apply (erule le_less_trans)  haftmann@26193  1043  apply (erule mult_strict_left_mono)  haftmann@26193  1044  apply simp  haftmann@26193  1045  apply (erule mult_right_mono)  haftmann@26193  1046  apply simp  haftmann@26193  1047  done  haftmann@26193  1048 haftmann@25230  1049 end  haftmann@25230  1050 haftmann@35097  1051 class linordered_semiring_1_strict = linordered_semiring_strict + semiring_1  hoelzl@36622  1052 begin  hoelzl@36622  1053 hoelzl@36622  1054 subclass linordered_semiring_1 ..  hoelzl@36622  1055 hoelzl@36622  1056 lemma convex_bound_lt:  hoelzl@36622  1057  assumes "x < a" "y < a" "0 \ u" "0 \ v" "u + v = 1"  hoelzl@36622  1058  shows "u * x + v * y < a"  hoelzl@36622  1059 proof -  hoelzl@36622  1060  from assms have "u * x + v * y < u * a + v * a"  hoelzl@36622  1061  by (cases "u = 0")  hoelzl@36622  1062  (auto intro!: add_less_le_mono mult_strict_left_mono mult_left_mono)  webertj@49962  1063  thus ?thesis using assms unfolding distrib_right[symmetric] by simp  hoelzl@36622  1064 qed  hoelzl@36622  1065 hoelzl@36622  1066 end  haftmann@33319  1067 lp15@60562  1068 class ordered_comm_semiring = comm_semiring_0 + ordered_ab_semigroup_add +  haftmann@38642  1069  assumes comm_mult_left_mono: "a \ b \ 0 \ c \ c * a \ c * b"  haftmann@25186  1070 begin  haftmann@25152  1071 haftmann@35028  1072 subclass ordered_semiring  haftmann@28823  1073 proof  krauss@21199  1074  fix a b c :: 'a  huffman@23550  1075  assume "a \ b" "0 \ c"  haftmann@38642  1076  thus "c * a \ c * b" by (rule comm_mult_left_mono)  haftmann@57512  1077  thus "a * c \ b * c" by (simp only: mult.commute)  krauss@21199  1078 qed  paulson@14265  1079 haftmann@25267  1080 end  haftmann@25267  1081 haftmann@38642  1082 class ordered_cancel_comm_semiring = ordered_comm_semiring + cancel_comm_monoid_add  haftmann@25267  1083 begin  paulson@14265  1084 haftmann@38642  1085 subclass comm_semiring_0_cancel ..  haftmann@35028  1086 subclass ordered_comm_semiring ..  haftmann@35028  1087 subclass ordered_cancel_semiring ..  haftmann@25267  1088 haftmann@25267  1089 end  haftmann@25267  1090 haftmann@35028  1091 class linordered_comm_semiring_strict = comm_semiring_0 + linordered_cancel_ab_semigroup_add +  haftmann@38642  1092  assumes comm_mult_strict_left_mono: "a < b \ 0 < c \ c * a < c * b"  haftmann@25267  1093 begin  haftmann@25267  1094 haftmann@35043  1095 subclass linordered_semiring_strict  haftmann@28823  1096 proof  huffman@23550  1097  fix a b c :: 'a  huffman@23550  1098  assume "a < b" "0 < c"  haftmann@38642  1099  thus "c * a < c * b" by (rule comm_mult_strict_left_mono)  haftmann@57512  1100  thus "a * c < b * c" by (simp only: mult.commute)  huffman@23550  1101 qed  paulson@14272  1102 haftmann@35028  1103 subclass ordered_cancel_comm_semiring  haftmann@28823  1104 proof  huffman@23550  1105  fix a b c :: 'a  huffman@23550  1106  assume "a \ b" "0 \ c"  huffman@23550  1107  thus "c * a \ c * b"  haftmann@25186  1108  unfolding le_less  haftmann@26193  1109  using mult_strict_left_mono by (cases "c = 0") auto  huffman@23550  1110 qed  paulson@14272  1111 haftmann@25267  1112 end  haftmann@25230  1113 lp15@60562  1114 class ordered_ring = ring + ordered_cancel_semiring  haftmann@25267  1115 begin  haftmann@25230  1116 haftmann@35028  1117 subclass ordered_ab_group_add ..  paulson@14270  1118 haftmann@25230  1119 lemma less_add_iff1:  haftmann@25230  1120  "a * e + c < b * e + d \ (a - b) * e + c < d"  nipkow@29667  1121 by (simp add: algebra_simps)  haftmann@25230  1122 haftmann@25230  1123 lemma less_add_iff2:  haftmann@25230  1124  "a * e + c < b * e + d \ c < (b - a) * e + d"  nipkow@29667  1125 by (simp add: algebra_simps)  haftmann@25230  1126 haftmann@25230  1127 lemma le_add_iff1:  haftmann@25230  1128  "a * e + c \ b * e + d \ (a - b) * e + c \ d"  nipkow@29667  1129 by (simp add: algebra_simps)  haftmann@25230  1130 haftmann@25230  1131 lemma le_add_iff2:  haftmann@25230  1132  "a * e + c \ b * e + d \ c \ (b - a) * e + d"  nipkow@29667  1133 by (simp add: algebra_simps)  haftmann@25230  1134 haftmann@25230  1135 lemma mult_left_mono_neg:  haftmann@25230  1136  "b \ a \ c \ 0 \ c * a \ c * b"  haftmann@36301  1137  apply (drule mult_left_mono [of _ _ "- c"])  huffman@35216  1138  apply simp_all  haftmann@25230  1139  done  haftmann@25230  1140 haftmann@25230  1141 lemma mult_right_mono_neg:  haftmann@25230  1142  "b \ a \ c \ 0 \ a * c \ b * c"  haftmann@36301  1143  apply (drule mult_right_mono [of _ _ "- c"])  huffman@35216  1144  apply simp_all  haftmann@25230  1145  done  haftmann@25230  1146 huffman@30692  1147 lemma mult_nonpos_nonpos: "a \ 0 \ b \ 0 \ 0 \ a * b"  haftmann@36301  1148 using mult_right_mono_neg [of a 0 b] by simp  haftmann@25230  1149 haftmann@25230  1150 lemma split_mult_pos_le:  haftmann@25230  1151  "(0 \ a \ 0 \ b) \ (a \ 0 \ b \ 0) \ 0 \ a * b"  nipkow@56536  1152 by (auto simp add: mult_nonpos_nonpos)  haftmann@25186  1153 haftmann@25186  1154 end  paulson@14270  1155 haftmann@35028  1156 class linordered_ring = ring + linordered_semiring + linordered_ab_group_add + abs_if  haftmann@25304  1157 begin  haftmann@25304  1158 haftmann@35028  1159 subclass ordered_ring ..  haftmann@35028  1160 haftmann@35028  1161 subclass ordered_ab_group_add_abs  haftmann@28823  1162 proof  haftmann@25304  1163  fix a b  haftmann@25304  1164  show "\a + b\ \ \a\ + \b\"  haftmann@54230  1165  by (auto simp add: abs_if not_le not_less algebra_simps simp del: add.commute dest: add_neg_neg add_nonneg_nonneg)  huffman@35216  1166 qed (auto simp add: abs_if)  haftmann@25304  1167 huffman@35631  1168 lemma zero_le_square [simp]: "0 \ a * a"  huffman@35631  1169  using linear [of 0 a]  nipkow@56536  1170  by (auto simp add: mult_nonpos_nonpos)  huffman@35631  1171 huffman@35631  1172 lemma not_square_less_zero [simp]: "\ (a * a < 0)"  huffman@35631  1173  by (simp add: not_less)  huffman@35631  1174 haftmann@25304  1175 end  obua@23521  1176 haftmann@35043  1177 class linordered_ring_strict = ring + linordered_semiring_strict  haftmann@25304  1178  + ordered_ab_group_add + abs_if  haftmann@25230  1179 begin  paulson@14348  1180 haftmann@35028  1181 subclass linordered_ring ..  haftmann@25304  1182 huffman@30692  1183 lemma mult_strict_left_mono_neg: "b < a \ c < 0 \ c * a < c * b"  huffman@30692  1184 using mult_strict_left_mono [of b a "- c"] by simp  huffman@30692  1185 huffman@30692  1186 lemma mult_strict_right_mono_neg: "b < a \ c < 0 \ a * c < b * c"  huffman@30692  1187 using mult_strict_right_mono [of b a "- c"] by simp  huffman@30692  1188 huffman@30692  1189 lemma mult_neg_neg: "a < 0 \ b < 0 \ 0 < a * b"  haftmann@36301  1190 using mult_strict_right_mono_neg [of a 0 b] by simp  obua@14738  1191 haftmann@25917  1192 subclass ring_no_zero_divisors  haftmann@28823  1193 proof  haftmann@25917  1194  fix a b  haftmann@25917  1195  assume "a \ 0" then have A: "a < 0 \ 0 < a" by (simp add: neq_iff)  haftmann@25917  1196  assume "b \ 0" then have B: "b < 0 \ 0 < b" by (simp add: neq_iff)  haftmann@25917  1197  have "a * b < 0 \ 0 < a * b"  haftmann@25917  1198  proof (cases "a < 0")  haftmann@25917  1199  case True note A' = this  haftmann@25917  1200  show ?thesis proof (cases "b < 0")  haftmann@25917  1201  case True with A'  haftmann@25917  1202  show ?thesis by (auto dest: mult_neg_neg)  haftmann@25917  1203  next  haftmann@25917  1204  case False with B have "0 < b" by auto  haftmann@25917  1205  with A' show ?thesis by (auto dest: mult_strict_right_mono)  haftmann@25917  1206  qed  haftmann@25917  1207  next  haftmann@25917  1208  case False with A have A': "0 < a" by auto  haftmann@25917  1209  show ?thesis proof (cases "b < 0")  haftmann@25917  1210  case True with A'  haftmann@25917  1211  show ?thesis by (auto dest: mult_strict_right_mono_neg)  haftmann@25917  1212  next  haftmann@25917  1213  case False with B have "0 < b" by auto  nipkow@56544  1214  with A' show ?thesis by auto  haftmann@25917  1215  qed  haftmann@25917  1216  qed  haftmann@25917  1217  then show "a * b \ 0" by (simp add: neq_iff)  haftmann@25917  1218 qed  haftmann@25304  1219 hoelzl@56480  1220 lemma zero_less_mult_iff: "0 < a * b \ 0 < a \ 0 < b \ a < 0 \ b < 0"  hoelzl@56480  1221  by (cases a 0 b 0 rule: linorder_cases[case_product linorder_cases])  nipkow@56544  1222  (auto simp add: mult_neg_neg not_less le_less dest: zero_less_mult_pos zero_less_mult_pos2)  huffman@22990  1223 hoelzl@56480  1224 lemma zero_le_mult_iff: "0 \ a * b \ 0 \ a \ 0 \ b \ a \ 0 \ b \ 0"  hoelzl@56480  1225  by (auto simp add: eq_commute [of 0] le_less not_less zero_less_mult_iff)  paulson@14265  1226 paulson@14265  1227 lemma mult_less_0_iff:  haftmann@25917  1228  "a * b < 0 \ 0 < a \ b < 0 \ a < 0 \ 0 < b"  huffman@35216  1229  apply (insert zero_less_mult_iff [of "-a" b])  huffman@35216  1230  apply force  haftmann@25917  1231  done  paulson@14265  1232 paulson@14265  1233 lemma mult_le_0_iff:  haftmann@25917  1234  "a * b \ 0 \ 0 \ a \ b \ 0 \ a \ 0 \ 0 \ b"  lp15@60562  1235  apply (insert zero_le_mult_iff [of "-a" b])  huffman@35216  1236  apply force  haftmann@25917  1237  done  haftmann@25917  1238 haftmann@26193  1239 text{*Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"},  haftmann@26193  1240  also with the relations @{text "\"} and equality.*}  haftmann@26193  1241 haftmann@26193  1242 text{*These disjunction'' versions produce two cases when the comparison is  haftmann@26193  1243  an assumption, but effectively four when the comparison is a goal.*}  haftmann@26193  1244 haftmann@26193  1245 lemma mult_less_cancel_right_disj:  haftmann@26193  1246  "a * c < b * c \ 0 < c \ a < b \ c < 0 \ b < a"  haftmann@26193  1247  apply (cases "c = 0")  lp15@60562  1248  apply (auto simp add: neq_iff mult_strict_right_mono  haftmann@26193  1249  mult_strict_right_mono_neg)  lp15@60562  1250  apply (auto simp add: not_less  haftmann@26193  1251  not_le [symmetric, of "a*c"]  haftmann@26193  1252  not_le [symmetric, of a])  haftmann@26193  1253  apply (erule_tac [!] notE)  lp15@60562  1254  apply (auto simp add: less_imp_le mult_right_mono  haftmann@26193  1255  mult_right_mono_neg)  haftmann@26193  1256  done  haftmann@26193  1257 haftmann@26193  1258 lemma mult_less_cancel_left_disj:  haftmann@26193  1259  "c * a < c * b \ 0 < c \ a < b \ c < 0 \ b < a"  haftmann@26193  1260  apply (cases "c = 0")  lp15@60562  1261  apply (auto simp add: neq_iff mult_strict_left_mono  haftmann@26193  1262  mult_strict_left_mono_neg)  lp15@60562  1263  apply (auto simp add: not_less  haftmann@26193  1264  not_le [symmetric, of "c*a"]  haftmann@26193  1265  not_le [symmetric, of a])  haftmann@26193  1266  apply (erule_tac [!] notE)  lp15@60562  1267  apply (auto simp add: less_imp_le mult_left_mono  haftmann@26193  1268  mult_left_mono_neg)  haftmann@26193  1269  done  haftmann@26193  1270 haftmann@26193  1271 text{*The conjunction of implication'' lemmas produce two cases when the  haftmann@26193  1272 comparison is a goal, but give four when the comparison is an assumption.*}  haftmann@26193  1273 haftmann@26193  1274 lemma mult_less_cancel_right:  haftmann@26193  1275  "a * c < b * c \ (0 \ c \ a < b) \ (c \ 0 \ b < a)"  haftmann@26193  1276  using mult_less_cancel_right_disj [of a c b] by auto  haftmann@26193  1277 haftmann@26193  1278 lemma mult_less_cancel_left:  haftmann@26193  1279  "c * a < c * b \ (0 \ c \ a < b) \ (c \ 0 \ b < a)"  haftmann@26193  1280  using mult_less_cancel_left_disj [of c a b] by auto  haftmann@26193  1281 haftmann@26193  1282 lemma mult_le_cancel_right:  haftmann@26193  1283  "a * c \ b * c \ (0 < c \ a \ b) \ (c < 0 \ b \ a)"  nipkow@29667  1284 by (simp add: not_less [symmetric] mult_less_cancel_right_disj)  haftmann@26193  1285 haftmann@26193  1286 lemma mult_le_cancel_left:  haftmann@26193  1287  "c * a \ c * b \ (0 < c \ a \ b) \ (c < 0 \ b \ a)"  nipkow@29667  1288 by (simp add: not_less [symmetric] mult_less_cancel_left_disj)  haftmann@26193  1289 nipkow@30649  1290 lemma mult_le_cancel_left_pos:  nipkow@30649  1291  "0 < c \ c * a \ c * b \ a \ b"  nipkow@30649  1292 by (auto simp: mult_le_cancel_left)  nipkow@30649  1293 nipkow@30649  1294 lemma mult_le_cancel_left_neg:  nipkow@30649  1295  "c < 0 \ c * a \ c * b \ b \ a"  nipkow@30649  1296 by (auto simp: mult_le_cancel_left)  nipkow@30649  1297 nipkow@30649  1298 lemma mult_less_cancel_left_pos:  nipkow@30649  1299  "0 < c \ c * a < c * b \ a < b"  nipkow@30649  1300 by (auto simp: mult_less_cancel_left)  nipkow@30649  1301 nipkow@30649  1302 lemma mult_less_cancel_left_neg:  nipkow@30649  1303  "c < 0 \ c * a < c * b \ b < a"  nipkow@30649  1304 by (auto simp: mult_less_cancel_left)  nipkow@30649  1305 haftmann@25917  1306 end  paulson@14265  1307 huffman@30692  1308 lemmas mult_sign_intros =  huffman@30692  1309  mult_nonneg_nonneg mult_nonneg_nonpos  huffman@30692  1310  mult_nonpos_nonneg mult_nonpos_nonpos  huffman@30692  1311  mult_pos_pos mult_pos_neg  huffman@30692  1312  mult_neg_pos mult_neg_neg  haftmann@25230  1313 haftmann@35028  1314 class ordered_comm_ring = comm_ring + ordered_comm_semiring  haftmann@25267  1315 begin  haftmann@25230  1316 haftmann@35028  1317 subclass ordered_ring ..  haftmann@35028  1318 subclass ordered_cancel_comm_semiring ..  haftmann@25230  1319 haftmann@25267  1320 end  haftmann@25230  1321 haftmann@59833  1322 class linordered_semidom = semidom + linordered_comm_semiring_strict +  haftmann@25230  1323  assumes zero_less_one [simp]: "0 < 1"  lp15@60562  1324  assumes le_add_diff_inverse2 [simp]: "b \ a \ a - b + b = a"  haftmann@25230  1325 begin  haftmann@25230  1326 lp15@60562  1327 text {* Addition is the inverse of subtraction. *}  lp15@60562  1328 lp15@60562  1329 lemma le_add_diff_inverse [simp]: "b \ a \ b + (a - b) = a"  lp15@60562  1330  by (frule le_add_diff_inverse2) (simp add: add.commute)  lp15@60562  1331 lp15@60562  1332 lemma add_diff_inverse: "~ a b + (a - b) = a"  lp15@60562  1333  by simp  lp15@60562  1334   haftmann@25230  1335 lemma pos_add_strict:  haftmann@25230  1336  shows "0 < a \ b < c \ b < a + c"  haftmann@36301  1337  using add_strict_mono [of 0 a b c] by simp  haftmann@25230  1338 haftmann@26193  1339 lemma zero_le_one [simp]: "0 \ 1"  lp15@60562  1340 by (rule zero_less_one [THEN less_imp_le])  haftmann@26193  1341 haftmann@26193  1342 lemma not_one_le_zero [simp]: "\ 1 \ 0"  lp15@60562  1343 by (simp add: not_le)  haftmann@26193  1344 haftmann@26193  1345 lemma not_one_less_zero [simp]: "\ 1 < 0"  lp15@60562  1346 by (simp add: not_less)  haftmann@26193  1347 haftmann@26193  1348 lemma less_1_mult:  haftmann@26193  1349  assumes "1 < m" and "1 < n"  haftmann@26193  1350  shows "1 < m * n"  haftmann@26193  1351  using assms mult_strict_mono [of 1 m 1 n]  lp15@60562  1352  by (simp add: less_trans [OF zero_less_one])  haftmann@26193  1353 hoelzl@59000  1354 lemma mult_left_le: "c \ 1 \ 0 \ a \ a * c \ a"  hoelzl@59000  1355  using mult_left_mono[of c 1 a] by simp  hoelzl@59000  1356 hoelzl@59000  1357 lemma mult_le_one: "a \ 1 \ 0 \ b \ b \ 1 \ a * b \ 1"  hoelzl@59000  1358  using mult_mono[of a 1 b 1] by simp  hoelzl@59000  1359 haftmann@25230  1360 end  haftmann@25230  1361 haftmann@35028  1362 class linordered_idom = comm_ring_1 +  haftmann@35028  1363  linordered_comm_semiring_strict + ordered_ab_group_add +  haftmann@25230  1364  abs_if + sgn_if  haftmann@25917  1365 begin  haftmann@25917  1366 hoelzl@36622  1367 subclass linordered_semiring_1_strict ..  haftmann@35043  1368 subclass linordered_ring_strict ..  haftmann@35028  1369 subclass ordered_comm_ring ..  huffman@27516  1370 subclass idom ..  haftmann@25917  1371 haftmann@35028  1372 subclass linordered_semidom  haftmann@28823  1373 proof  haftmann@26193  1374  have "0 \ 1 * 1" by (rule zero_le_square)  haftmann@26193  1375  thus "0 < 1" by (simp add: le_less)  lp15@60562  1376  show "\b a. b \ a \ a - b + b = a"  lp15@60562  1377  by simp  lp15@60562  1378 qed  haftmann@25917  1379 haftmann@35028  1380 lemma linorder_neqE_linordered_idom:  haftmann@26193  1381  assumes "x \ y" obtains "x < y" | "y < x"  haftmann@26193  1382  using assms by (rule neqE)  haftmann@26193  1383 haftmann@26274  1384 text {* These cancellation simprules also produce two cases when the comparison is a goal. *}  haftmann@26274  1385 haftmann@26274  1386 lemma mult_le_cancel_right1:  haftmann@26274  1387  "c \ b * c \ (0 < c \ 1 \ b) \ (c < 0 \ b \ 1)"  nipkow@29667  1388 by (insert mult_le_cancel_right [of 1 c b], simp)  haftmann@26274  1389 haftmann@26274  1390 lemma mult_le_cancel_right2:  haftmann@26274  1391  "a * c \ c \ (0 < c \ a \ 1) \ (c < 0 \ 1 \ a)"  nipkow@29667  1392 by (insert mult_le_cancel_right [of a c 1], simp)  haftmann@26274  1393 haftmann@26274  1394 lemma mult_le_cancel_left1:  haftmann@26274  1395  "c \ c * b \ (0 < c \ 1 \ b) \ (c < 0 \ b \ 1)"  nipkow@29667  1396 by (insert mult_le_cancel_left [of c 1 b], simp)  haftmann@26274  1397 haftmann@26274  1398 lemma mult_le_cancel_left2:  haftmann@26274  1399  "c * a \ c \ (0 < c \ a \ 1) \ (c < 0 \ 1 \ a)"  nipkow@29667  1400 by (insert mult_le_cancel_left [of c a 1], simp)  haftmann@26274  1401 haftmann@26274  1402 lemma mult_less_cancel_right1:  haftmann@26274  1403  "c < b * c \ (0 \ c \ 1 < b) \ (c \ 0 \ b < 1)"  nipkow@29667  1404 by (insert mult_less_cancel_right [of 1 c b], simp)  haftmann@26274  1405 haftmann@26274  1406 lemma mult_less_cancel_right2:  haftmann@26274  1407  "a * c < c \ (0 \ c \ a < 1) \ (c \ 0 \ 1 < a)"  nipkow@29667  1408 by (insert mult_less_cancel_right [of a c 1], simp)  haftmann@26274  1409 haftmann@26274  1410 lemma mult_less_cancel_left1:  haftmann@26274  1411  "c < c * b \ (0 \ c \ 1 < b) \ (c \ 0 \ b < 1)"  nipkow@29667  1412 by (insert mult_less_cancel_left [of c 1 b], simp)  haftmann@26274  1413 haftmann@26274  1414 lemma mult_less_cancel_left2:  haftmann@26274  1415  "c * a < c \ (0 \ c \ a < 1) \ (c \ 0 \ 1 < a)"  nipkow@29667  1416 by (insert mult_less_cancel_left [of c a 1], simp)  haftmann@26274  1417 haftmann@27651  1418 lemma sgn_sgn [simp]:  haftmann@27651  1419  "sgn (sgn a) = sgn a"  nipkow@29700  1420 unfolding sgn_if by simp  haftmann@27651  1421 haftmann@27651  1422 lemma sgn_0_0:  haftmann@27651  1423  "sgn a = 0 \ a = 0"  nipkow@29700  1424 unfolding sgn_if by simp  haftmann@27651  1425 haftmann@27651  1426 lemma sgn_1_pos:  haftmann@27651  1427  "sgn a = 1 \ a > 0"  huffman@35216  1428 unfolding sgn_if by simp  haftmann@27651  1429 haftmann@27651  1430 lemma sgn_1_neg:  haftmann@27651  1431  "sgn a = - 1 \ a < 0"  huffman@35216  1432 unfolding sgn_if by auto  haftmann@27651  1433 haftmann@29940  1434 lemma sgn_pos [simp]:  haftmann@29940  1435  "0 < a \ sgn a = 1"  haftmann@29940  1436 unfolding sgn_1_pos .  haftmann@29940  1437 haftmann@29940  1438 lemma sgn_neg [simp]:  haftmann@29940  1439  "a < 0 \ sgn a = - 1"  haftmann@29940  1440 unfolding sgn_1_neg .  haftmann@29940  1441 haftmann@27651  1442 lemma sgn_times:  haftmann@27651  1443  "sgn (a * b) = sgn a * sgn b"  nipkow@29667  1444 by (auto simp add: sgn_if zero_less_mult_iff)  haftmann@27651  1445 haftmann@36301  1446 lemma abs_sgn: "\k\ = k * sgn k"  nipkow@29700  1447 unfolding sgn_if abs_if by auto  nipkow@29700  1448 haftmann@29940  1449 lemma sgn_greater [simp]:  haftmann@29940  1450  "0 < sgn a \ 0 < a"  haftmann@29940  1451  unfolding sgn_if by auto  haftmann@29940  1452 haftmann@29940  1453 lemma sgn_less [simp]:  haftmann@29940  1454  "sgn a < 0 \ a < 0"  haftmann@29940  1455  unfolding sgn_if by auto  haftmann@29940  1456 haftmann@36301  1457 lemma abs_dvd_iff [simp]: "\m\ dvd k \ m dvd k"  huffman@29949  1458  by (simp add: abs_if)  huffman@29949  1459 haftmann@36301  1460 lemma dvd_abs_iff [simp]: "m dvd \k\ \ m dvd k"  huffman@29949  1461  by (simp add: abs_if)  haftmann@29653  1462 nipkow@33676  1463 lemma dvd_if_abs_eq:  haftmann@36301  1464  "\l\ = \k\ \ l dvd k"  nipkow@33676  1465 by(subst abs_dvd_iff[symmetric]) simp  nipkow@33676  1466 huffman@55912  1467 text {* The following lemmas can be proven in more general structures, but  lp15@60562  1468 are dangerous as simp rules in absence of @{thm neg_equal_zero},  haftmann@54489  1469 @{thm neg_less_pos}, @{thm neg_less_eq_nonneg}. *}  haftmann@54489  1470 haftmann@54489  1471 lemma equation_minus_iff_1 [simp, no_atp]:  haftmann@54489  1472  "1 = - a \ a = - 1"  haftmann@54489  1473  by (fact equation_minus_iff)  haftmann@54489  1474 haftmann@54489  1475 lemma minus_equation_iff_1 [simp, no_atp]:  haftmann@54489  1476  "- a = 1 \ a = - 1"  haftmann@54489  1477  by (subst minus_equation_iff, auto)  haftmann@54489  1478 haftmann@54489  1479 lemma le_minus_iff_1 [simp, no_atp]:  haftmann@54489  1480  "1 \ - b \ b \ - 1"  haftmann@54489  1481  by (fact le_minus_iff)  haftmann@54489  1482 haftmann@54489  1483 lemma minus_le_iff_1 [simp, no_atp]:  haftmann@54489  1484  "- a \ 1 \ - 1 \ a"  haftmann@54489  1485  by (fact minus_le_iff)  haftmann@54489  1486 haftmann@54489  1487 lemma less_minus_iff_1 [simp, no_atp]:  haftmann@54489  1488  "1 < - b \ b < - 1"  haftmann@54489  1489  by (fact less_minus_iff)  haftmann@54489  1490 haftmann@54489  1491 lemma minus_less_iff_1 [simp, no_atp]:  haftmann@54489  1492  "- a < 1 \ - 1 < a"  haftmann@54489  1493  by (fact minus_less_iff)  haftmann@54489  1494 haftmann@25917  1495 end  haftmann@25230  1496 haftmann@26274  1497 text {* Simprules for comparisons where common factors can be cancelled. *}  paulson@15234  1498 blanchet@54147  1499 lemmas mult_compare_simps =  paulson@15234  1500  mult_le_cancel_right mult_le_cancel_left  paulson@15234  1501  mult_le_cancel_right1 mult_le_cancel_right2  paulson@15234  1502  mult_le_cancel_left1 mult_le_cancel_left2  paulson@15234  1503  mult_less_cancel_right mult_less_cancel_left  paulson@15234  1504  mult_less_cancel_right1 mult_less_cancel_right2  paulson@15234  1505  mult_less_cancel_left1 mult_less_cancel_left2  paulson@15234  1506  mult_cancel_right mult_cancel_left  paulson@15234  1507  mult_cancel_right1 mult_cancel_right2  paulson@15234  1508  mult_cancel_left1 mult_cancel_left2  paulson@15234  1509 haftmann@36301  1510 text {* Reasoning about inequalities with division *}  avigad@16775  1511 haftmann@35028  1512 context linordered_semidom  haftmann@25193  1513 begin  haftmann@25193  1514 haftmann@25193  1515 lemma less_add_one: "a < a + 1"  paulson@14293  1516 proof -  haftmann@25193  1517  have "a + 0 < a + 1"  nipkow@23482  1518  by (blast intro: zero_less_one add_strict_left_mono)  paulson@14293  1519  thus ?thesis by simp  paulson@14293  1520 qed  paulson@14293  1521 haftmann@25193  1522 lemma zero_less_two: "0 < 1 + 1"  nipkow@29667  1523 by (blast intro: less_trans zero_less_one less_add_one)  haftmann@25193  1524 haftmann@25193  1525 end  paulson@14365  1526 haftmann@36301  1527 context linordered_idom  haftmann@36301  1528 begin  paulson@15234  1529 haftmann@36301  1530 lemma mult_right_le_one_le:  haftmann@36301  1531  "0 \ x \ 0 \ y \ y \ 1 \ x * y \ x"  haftmann@59833  1532  by (rule mult_left_le)  haftmann@36301  1533 haftmann@36301  1534 lemma mult_left_le_one_le:  haftmann@36301  1535  "0 \ x \ 0 \ y \ y \ 1 \ y * x \ x"  haftmann@36301  1536  by (auto simp add: mult_le_cancel_right2)  haftmann@36301  1537 haftmann@36301  1538 end  haftmann@36301  1539 haftmann@36301  1540 text {* Absolute Value *}  paulson@14293  1541 haftmann@35028  1542 context linordered_idom  haftmann@25304  1543 begin  haftmann@25304  1544 haftmann@36301  1545 lemma mult_sgn_abs:  haftmann@36301  1546  "sgn x * \x\ = x"  haftmann@25304  1547  unfolding abs_if sgn_if by auto  haftmann@25304  1548 haftmann@36301  1549 lemma abs_one [simp]:  haftmann@36301  1550  "\1\ = 1"  huffman@44921  1551  by (simp add: abs_if)  haftmann@36301  1552 haftmann@25304  1553 end  nipkow@24491  1554 haftmann@35028  1555 class ordered_ring_abs = ordered_ring + ordered_ab_group_add_abs +  haftmann@25304  1556  assumes abs_eq_mult:  haftmann@25304  1557  "(0 \ a \ a \ 0) \ (0 \ b \ b \ 0) \ \a * b\ = \a\ * \b\"  haftmann@25304  1558 haftmann@35028  1559 context linordered_idom  haftmann@30961  1560 begin  haftmann@30961  1561 haftmann@35028  1562 subclass ordered_ring_abs proof  huffman@35216  1563 qed (auto simp add: abs_if not_less mult_less_0_iff)  haftmann@30961  1564 haftmann@30961  1565 lemma abs_mult:  lp15@60562  1566  "\a * b\ = \a\ * \b\"  haftmann@30961  1567  by (rule abs_eq_mult) auto  haftmann@30961  1568 haftmann@30961  1569 lemma abs_mult_self:  haftmann@36301  1570  "\a\ * \a\ = a * a"  lp15@60562  1571  by (simp add: abs_if)  haftmann@30961  1572 paulson@14294  1573 lemma abs_mult_less:  haftmann@36301  1574  "\a\ < c \ \b\ < d \ \a\ * \b\ < c * d"  paulson@14294  1575 proof -  haftmann@36301  1576  assume ac: "\a\ < c"  haftmann@36301  1577  hence cpos: "0b\ < d"  lp15@60562  1579  thus ?thesis by (simp add: ac cpos mult_strict_mono)  paulson@14294  1580 qed  paulson@14293  1581 haftmann@36301  1582 lemma abs_less_iff:  lp15@60562  1583  "\a\ < b \ a < b \ - a < b"  haftmann@36301  1584  by (simp add: less_le abs_le_iff) (auto simp add: abs_if)  obua@14738  1585 haftmann@36301  1586 lemma abs_mult_pos:  haftmann@36301  1587  "0 \ x \ \y\ * x = \y * x\"  haftmann@36301  1588  by (simp add: abs_mult)  haftmann@36301  1589 hoelzl@51520  1590 lemma abs_diff_less_iff:  hoelzl@51520  1591  "\x - a\ < r \ a - r < x \ x < a + r"  hoelzl@51520  1592  by (auto simp add: diff_less_eq ac_simps abs_less_iff)  hoelzl@51520  1593 lp15@59865  1594 lemma abs_diff_le_iff:  lp15@59865  1595  "\x - a\ \ r \ a - r \ x \ x \ a + r"  lp15@59865  1596  by (auto simp add: diff_le_eq ac_simps abs_le_iff)  lp15@59865  1597 haftmann@36301  1598 end  avigad@16775  1599 haftmann@59557  1600 hide_fact (open) comm_mult_left_mono comm_mult_strict_left_mono distrib  haftmann@59557  1601 haftmann@52435  1602 code_identifier  haftmann@52435  1603  code_module Rings \ (SML) Arith and (OCaml) Arith and (Haskell) Arith  haftmann@33364  1604 paulson@14265  1605 end