151 minus_mult_left [symmetric] minus_mult_right [symmetric]) |
151 minus_mult_left [symmetric] minus_mult_right [symmetric]) |
152 |
152 |
153 lemmas ring_distribs = |
153 lemmas ring_distribs = |
154 right_distrib left_distrib left_diff_distrib right_diff_distrib |
154 right_distrib left_distrib left_diff_distrib right_diff_distrib |
155 |
155 |
|
156 lemmas ring_simps = |
|
157 add_ac |
|
158 add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2 |
|
159 diff_eq_eq eq_diff_eq diff_minus [symmetric] uminus_add_conv_diff |
|
160 ring_distribs |
|
161 |
|
162 lemma eq_add_iff1: |
|
163 "a * e + c = b * e + d \<longleftrightarrow> (a - b) * e + c = d" |
|
164 by (simp add: ring_simps) |
|
165 |
|
166 lemma eq_add_iff2: |
|
167 "a * e + c = b * e + d \<longleftrightarrow> c = (b - a) * e + d" |
|
168 by (simp add: ring_simps) |
|
169 |
156 end |
170 end |
157 |
171 |
158 lemmas ring_distribs = |
172 lemmas ring_distribs = |
159 right_distrib left_distrib left_diff_distrib right_diff_distrib |
173 right_distrib left_distrib left_diff_distrib right_diff_distrib |
160 |
174 |
161 text{*This list of rewrites simplifies ring terms by multiplying |
|
162 everything out and bringing sums and products into a canonical form |
|
163 (by ordered rewriting). As a result it decides ring equalities but |
|
164 also helps with inequalities. *} |
|
165 lemmas ring_simps = group_simps ring_distribs |
|
166 |
|
167 class comm_ring = comm_semiring + ab_group_add |
175 class comm_ring = comm_semiring + ab_group_add |
168 |
176 |
169 subclass (in comm_ring) ring by unfold_locales |
177 subclass (in comm_ring) ring by unfold_locales |
170 subclass (in comm_ring) comm_semiring_0 by unfold_locales |
178 subclass (in comm_ring) comm_semiring_0 by unfold_locales |
171 |
179 |
224 fix a :: 'a |
244 fix a :: 'a |
225 assume "a \<noteq> 0" |
245 assume "a \<noteq> 0" |
226 thus "inverse a * a = 1" by (rule field_inverse) |
246 thus "inverse a * a = 1" by (rule field_inverse) |
227 thus "a * inverse a = 1" by (simp only: mult_commute) |
247 thus "a * inverse a = 1" by (simp only: mult_commute) |
228 qed |
248 qed |
|
249 |
229 subclass (in field) idom by unfold_locales |
250 subclass (in field) idom by unfold_locales |
|
251 |
|
252 context field |
|
253 begin |
|
254 |
|
255 lemma right_inverse_eq: "b \<noteq> 0 \<Longrightarrow> a / b = 1 \<longleftrightarrow> a = b" |
|
256 proof |
|
257 assume neq: "b \<noteq> 0" |
|
258 { |
|
259 hence "a = (a / b) * b" by (simp add: divide_inverse mult_ac) |
|
260 also assume "a / b = 1" |
|
261 finally show "a = b" by simp |
|
262 next |
|
263 assume "a = b" |
|
264 with neq show "a / b = 1" by (simp add: divide_inverse) |
|
265 } |
|
266 qed |
|
267 |
|
268 lemma nonzero_inverse_eq_divide: "a \<noteq> 0 \<Longrightarrow> inverse a = 1 / a" |
|
269 by (simp add: divide_inverse) |
|
270 |
|
271 lemma divide_self [simp]: "a \<noteq> 0 \<Longrightarrow> a / a = 1" |
|
272 by (simp add: divide_inverse) |
|
273 |
|
274 lemma divide_zero_left [simp]: "0 / a = 0" |
|
275 by (simp add: divide_inverse) |
|
276 |
|
277 lemma inverse_eq_divide: "inverse a = 1 / a" |
|
278 by (simp add: divide_inverse) |
|
279 |
|
280 lemma add_divide_distrib: "(a+b) / c = a/c + b/c" |
|
281 by (simp add: divide_inverse ring_distribs) |
|
282 |
|
283 end |
230 |
284 |
231 class division_by_zero = zero + inverse + |
285 class division_by_zero = zero + inverse + |
232 assumes inverse_zero [simp]: "inverse 0 = 0" |
286 assumes inverse_zero [simp]: "inverse 0 = 0" |
|
287 |
|
288 lemma divide_zero [simp]: |
|
289 "a / 0 = (0::'a::{field,division_by_zero})" |
|
290 by (simp add: divide_inverse) |
|
291 |
|
292 lemma divide_self_if [simp]: |
|
293 "a / (a::'a::{field,division_by_zero}) = (if a=0 then 0 else 1)" |
|
294 by (simp add: divide_self) |
233 |
295 |
234 class mult_mono = times + zero + ord + |
296 class mult_mono = times + zero + ord + |
235 assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b" |
297 assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b" |
236 assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c" |
298 assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c" |
237 |
299 |
238 class pordered_semiring = mult_mono + semiring_0 + pordered_ab_semigroup_add |
300 class pordered_semiring = mult_mono + semiring_0 + pordered_ab_semigroup_add |
|
301 begin |
|
302 |
|
303 lemma mult_mono: |
|
304 "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> c |
|
305 \<Longrightarrow> a * c \<le> b * d" |
|
306 apply (erule mult_right_mono [THEN order_trans], assumption) |
|
307 apply (erule mult_left_mono, assumption) |
|
308 done |
|
309 |
|
310 lemma mult_mono': |
|
311 "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> c |
|
312 \<Longrightarrow> a * c \<le> b * d" |
|
313 apply (rule mult_mono) |
|
314 apply (fast intro: order_trans)+ |
|
315 done |
|
316 |
|
317 end |
239 |
318 |
240 class pordered_cancel_semiring = mult_mono + pordered_ab_semigroup_add |
319 class pordered_cancel_semiring = mult_mono + pordered_ab_semigroup_add |
241 + semiring + comm_monoid_add + cancel_ab_semigroup_add |
320 + semiring + comm_monoid_add + cancel_ab_semigroup_add |
242 |
321 |
243 subclass (in pordered_cancel_semiring) semiring_0_cancel by unfold_locales |
322 subclass (in pordered_cancel_semiring) semiring_0_cancel by unfold_locales |
244 subclass (in pordered_cancel_semiring) pordered_semiring by unfold_locales |
323 subclass (in pordered_cancel_semiring) pordered_semiring by unfold_locales |
245 |
324 |
|
325 context pordered_cancel_semiring |
|
326 begin |
|
327 |
|
328 lemma mult_nonneg_nonneg: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b" |
|
329 by (drule mult_left_mono [of zero b], auto) |
|
330 |
|
331 lemma mult_nonneg_nonpos: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> a * b \<le> 0" |
|
332 by (drule mult_left_mono [of b zero], auto) |
|
333 |
|
334 lemma mult_nonneg_nonpos2: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> b * a \<le> 0" |
|
335 by (drule mult_right_mono [of b zero], auto) |
|
336 |
|
337 lemma split_mult_neg_le: "(0 \<le> a & b \<le> 0) | (a \<le> 0 & 0 \<le> b) \<Longrightarrow> a * b \<le> (0::_::pordered_cancel_semiring)" |
|
338 by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2) |
|
339 |
|
340 end |
|
341 |
246 class ordered_semiring = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add + mult_mono |
342 class ordered_semiring = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add + mult_mono |
|
343 |
|
344 subclass (in ordered_semiring) pordered_cancel_semiring by unfold_locales |
|
345 |
|
346 context ordered_semiring |
247 begin |
347 begin |
248 |
348 |
249 subclass pordered_cancel_semiring by unfold_locales |
349 lemma mult_left_less_imp_less: |
|
350 "c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b" |
|
351 by (force simp add: mult_left_mono not_le [symmetric]) |
|
352 |
|
353 lemma mult_right_less_imp_less: |
|
354 "a * c < b * c \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b" |
|
355 by (force simp add: mult_right_mono not_le [symmetric]) |
250 |
356 |
251 end |
357 end |
252 |
358 |
253 class ordered_semiring_strict = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add + |
359 class ordered_semiring_strict = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add + |
254 assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b" |
360 assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b" |
266 from A show "a * c \<le> b * c" |
372 from A show "a * c \<le> b * c" |
267 unfolding le_less |
373 unfolding le_less |
268 using mult_strict_right_mono by (cases "c = 0") auto |
374 using mult_strict_right_mono by (cases "c = 0") auto |
269 qed |
375 qed |
270 |
376 |
|
377 context ordered_semiring_strict |
|
378 begin |
|
379 |
|
380 lemma mult_left_le_imp_le: |
|
381 "c * a \<le> c * b \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b" |
|
382 by (force simp add: mult_strict_left_mono _not_less [symmetric]) |
|
383 |
|
384 lemma mult_right_le_imp_le: |
|
385 "a * c \<le> b * c \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b" |
|
386 by (force simp add: mult_strict_right_mono not_less [symmetric]) |
|
387 |
|
388 lemma mult_pos_pos: |
|
389 "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a * b" |
|
390 by (drule mult_strict_left_mono [of zero b], auto) |
|
391 |
|
392 lemma mult_pos_neg: |
|
393 "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> a * b < 0" |
|
394 by (drule mult_strict_left_mono [of b zero], auto) |
|
395 |
|
396 lemma mult_pos_neg2: |
|
397 "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> b * a < 0" |
|
398 by (drule mult_strict_right_mono [of b zero], auto) |
|
399 |
|
400 lemma zero_less_mult_pos: |
|
401 "0 < a * b \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b" |
|
402 apply (cases "b\<le>0") |
|
403 apply (auto simp add: le_less not_less) |
|
404 apply (drule_tac mult_pos_neg [of a b]) |
|
405 apply (auto dest: less_not_sym) |
|
406 done |
|
407 |
|
408 lemma zero_less_mult_pos2: |
|
409 "0 < b * a \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b" |
|
410 apply (cases "b\<le>0") |
|
411 apply (auto simp add: le_less not_less) |
|
412 apply (drule_tac mult_pos_neg2 [of a b]) |
|
413 apply (auto dest: less_not_sym) |
|
414 done |
|
415 |
|
416 end |
|
417 |
271 class mult_mono1 = times + zero + ord + |
418 class mult_mono1 = times + zero + ord + |
272 assumes mult_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b" |
419 assumes mult_mono1: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b" |
273 |
420 |
274 class pordered_comm_semiring = comm_semiring_0 |
421 class pordered_comm_semiring = comm_semiring_0 |
275 + pordered_ab_semigroup_add + mult_mono1 |
422 + pordered_ab_semigroup_add + mult_mono1 |
276 |
423 |
277 class pordered_cancel_comm_semiring = comm_semiring_0_cancel |
424 class pordered_cancel_comm_semiring = comm_semiring_0_cancel |
312 unfolding le_less |
459 unfolding le_less |
313 using mult_strict_mono by (cases "c = 0") auto |
460 using mult_strict_mono by (cases "c = 0") auto |
314 qed |
461 qed |
315 |
462 |
316 class pordered_ring = ring + pordered_cancel_semiring |
463 class pordered_ring = ring + pordered_cancel_semiring |
|
464 |
|
465 subclass (in pordered_ring) pordered_ab_group_add by unfold_locales |
|
466 |
|
467 context pordered_ring |
317 begin |
468 begin |
318 |
469 |
319 subclass pordered_ab_group_add by unfold_locales |
470 lemmas ring_simps = ring_simps group_simps |
|
471 |
|
472 lemma less_add_iff1: |
|
473 "a * e + c < b * e + d \<longleftrightarrow> (a - b) * e + c < d" |
|
474 by (simp add: ring_simps) |
|
475 |
|
476 lemma less_add_iff2: |
|
477 "a * e + c < b * e + d \<longleftrightarrow> c < (b - a) * e + d" |
|
478 by (simp add: ring_simps) |
|
479 |
|
480 lemma le_add_iff1: |
|
481 "a * e + c \<le> b * e + d \<longleftrightarrow> (a - b) * e + c \<le> d" |
|
482 by (simp add: ring_simps) |
|
483 |
|
484 lemma le_add_iff2: |
|
485 "a * e + c \<le> b * e + d \<longleftrightarrow> c \<le> (b - a) * e + d" |
|
486 by (simp add: ring_simps) |
|
487 |
|
488 lemma mult_left_mono_neg: |
|
489 "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> c * a \<le> c * b" |
|
490 apply (drule mult_left_mono [of _ _ "uminus c"]) |
|
491 apply (simp_all add: minus_mult_left [symmetric]) |
|
492 done |
|
493 |
|
494 lemma mult_right_mono_neg: |
|
495 "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> a * c \<le> b * c" |
|
496 apply (drule mult_right_mono [of _ _ "uminus c"]) |
|
497 apply (simp_all add: minus_mult_right [symmetric]) |
|
498 done |
|
499 |
|
500 lemma mult_nonpos_nonpos: |
|
501 "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> 0 \<le> a * b" |
|
502 by (drule mult_right_mono_neg [of a zero b]) auto |
|
503 |
|
504 lemma split_mult_pos_le: |
|
505 "(0 \<le> a \<and> 0 \<le> b) \<or> (a \<le> 0 \<and> b \<le> 0) \<Longrightarrow> 0 \<le> a * b" |
|
506 by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos) |
320 |
507 |
321 end |
508 end |
322 |
509 |
323 class lordered_ring = pordered_ring + lordered_ab_group_abs |
510 class lordered_ring = pordered_ring + lordered_ab_group_abs |
324 |
511 |
329 assumes abs_if: "\<bar>a\<bar> = (if a < 0 then (- a) else a)" |
516 assumes abs_if: "\<bar>a\<bar> = (if a < 0 then (- a) else a)" |
330 |
517 |
331 class sgn_if = sgn + zero + one + minus + ord + |
518 class sgn_if = sgn + zero + one + minus + ord + |
332 assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)" |
519 assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)" |
333 |
520 |
334 (* The "strict" suffix can be seen as describing the combination of ordered_ring and no_zero_divisors. |
521 class ordered_ring = ring + ordered_semiring |
335 Basically, ordered_ring + no_zero_divisors = ordered_ring_strict. |
522 + lordered_ab_group + abs_if |
336 *) |
523 -- {*FIXME: should inherit from ordered_ab_group_add rather than |
337 class ordered_ring = ring + ordered_semiring + lordered_ab_group + abs_if |
524 lordered_ab_group*} |
338 |
|
339 -- {*FIXME: continue localization here*} |
|
340 |
525 |
341 instance ordered_ring \<subseteq> lordered_ring |
526 instance ordered_ring \<subseteq> lordered_ring |
342 proof |
527 proof |
343 fix x :: 'a |
528 fix x :: 'a |
344 show "\<bar>x\<bar> = sup x (- x)" |
529 show "\<bar>x\<bar> = sup x (- x)" |
345 by (simp only: abs_if sup_eq_if) |
530 by (simp only: abs_if sup_eq_if) |
346 qed |
531 qed |
347 |
532 |
348 class ordered_ring_strict = |
533 (* The "strict" suffix can be seen as describing the combination of ordered_ring and no_zero_divisors. |
349 ring + ordered_semiring_strict + lordered_ab_group + abs_if |
534 Basically, ordered_ring + no_zero_divisors = ordered_ring_strict. |
350 |
535 *) |
351 instance ordered_ring_strict \<subseteq> ordered_ring .. |
536 class ordered_ring_strict = ring + ordered_semiring_strict |
|
537 + lordered_ab_group + abs_if |
|
538 -- {*FIXME: should inherit from ordered_ab_group_add rather than |
|
539 lordered_ab_group*} |
|
540 |
|
541 instance ordered_ring_strict \<subseteq> ordered_ring by intro_classes |
|
542 |
|
543 context ordered_ring_strict |
|
544 begin |
|
545 |
|
546 lemma mult_strict_left_mono_neg: |
|
547 "b < a \<Longrightarrow> c < 0 \<Longrightarrow> c * a < c * b" |
|
548 apply (drule mult_strict_left_mono [of _ _ "uminus c"]) |
|
549 apply (simp_all add: minus_mult_left [symmetric]) |
|
550 done |
|
551 |
|
552 lemma mult_strict_right_mono_neg: |
|
553 "b < a \<Longrightarrow> c < 0 \<Longrightarrow> a * c < b * c" |
|
554 apply (drule mult_strict_right_mono [of _ _ "uminus c"]) |
|
555 apply (simp_all add: minus_mult_right [symmetric]) |
|
556 done |
|
557 |
|
558 lemma mult_neg_neg: |
|
559 "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> 0 < a * b" |
|
560 by (drule mult_strict_right_mono_neg, auto) |
|
561 |
|
562 end |
|
563 |
|
564 lemma zero_less_mult_iff: |
|
565 fixes a :: "'a::ordered_ring_strict" |
|
566 shows "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0" |
|
567 apply (auto simp add: le_less not_less mult_pos_pos mult_neg_neg) |
|
568 apply (blast dest: zero_less_mult_pos) |
|
569 apply (blast dest: zero_less_mult_pos2) |
|
570 done |
|
571 |
|
572 instance ordered_ring_strict \<subseteq> ring_no_zero_divisors |
|
573 apply intro_classes |
|
574 apply (auto simp add: linorder_not_less order_le_less linorder_neq_iff) |
|
575 apply (force dest: mult_strict_right_mono_neg mult_strict_right_mono)+ |
|
576 done |
|
577 |
|
578 lemma zero_le_mult_iff: |
|
579 "((0::'a::ordered_ring_strict) \<le> a*b) = (0 \<le> a & 0 \<le> b | a \<le> 0 & b \<le> 0)" |
|
580 by (auto simp add: eq_commute [of 0] order_le_less linorder_not_less |
|
581 zero_less_mult_iff) |
|
582 |
|
583 lemma mult_less_0_iff: |
|
584 "(a*b < (0::'a::ordered_ring_strict)) = (0 < a & b < 0 | a < 0 & 0 < b)" |
|
585 apply (insert zero_less_mult_iff [of "-a" b]) |
|
586 apply (force simp add: minus_mult_left[symmetric]) |
|
587 done |
|
588 |
|
589 lemma mult_le_0_iff: |
|
590 "(a*b \<le> (0::'a::ordered_ring_strict)) = (0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> b)" |
|
591 apply (insert zero_le_mult_iff [of "-a" b]) |
|
592 apply (force simp add: minus_mult_left[symmetric]) |
|
593 done |
|
594 |
|
595 lemma zero_le_square[simp]: "(0::'a::ordered_ring_strict) \<le> a*a" |
|
596 by (simp add: zero_le_mult_iff linorder_linear) |
|
597 |
|
598 lemma not_square_less_zero[simp]: "\<not> (a * a < (0::'a::ordered_ring_strict))" |
|
599 by (simp add: not_less) |
|
600 |
|
601 text{*This list of rewrites simplifies ring terms by multiplying |
|
602 everything out and bringing sums and products into a canonical form |
|
603 (by ordered rewriting). As a result it decides ring equalities but |
|
604 also helps with inequalities. *} |
|
605 lemmas ring_simps = group_simps ring_distribs |
|
606 |
352 |
607 |
353 class pordered_comm_ring = comm_ring + pordered_comm_semiring |
608 class pordered_comm_ring = comm_ring + pordered_comm_semiring |
354 |
609 |
355 instance pordered_comm_ring \<subseteq> pordered_ring .. |
610 subclass (in pordered_comm_ring) pordered_ring by unfold_locales |
356 |
611 |
357 instance pordered_comm_ring \<subseteq> pordered_cancel_comm_semiring .. |
612 subclass (in pordered_comm_ring) pordered_cancel_comm_semiring by unfold_locales |
358 |
613 |
359 class ordered_semidom = comm_semiring_1_cancel + ordered_comm_semiring_strict + |
614 class ordered_semidom = comm_semiring_1_cancel + ordered_comm_semiring_strict + |
360 (*previously ordered_semiring*) |
615 (*previously ordered_semiring*) |
361 assumes zero_less_one [simp]: "0 < 1" |
616 assumes zero_less_one [simp]: "0 < 1" |
|
617 begin |
362 |
618 |
363 lemma pos_add_strict: |
619 lemma pos_add_strict: |
364 fixes a b c :: "'a\<Colon>ordered_semidom" |
|
365 shows "0 < a \<Longrightarrow> b < c \<Longrightarrow> b < a + c" |
620 shows "0 < a \<Longrightarrow> b < c \<Longrightarrow> b < a + c" |
366 using add_strict_mono [of 0 a b c] by simp |
621 using add_strict_mono [of zero a b c] by simp |
|
622 |
|
623 end |
367 |
624 |
368 class ordered_idom = |
625 class ordered_idom = |
369 comm_ring_1 + |
626 comm_ring_1 + |
370 ordered_comm_semiring_strict + |
627 ordered_comm_semiring_strict + |
371 lordered_ab_group + |
628 lordered_ab_group + |
381 lemma linorder_neqE_ordered_idom: |
638 lemma linorder_neqE_ordered_idom: |
382 fixes x y :: "'a :: ordered_idom" |
639 fixes x y :: "'a :: ordered_idom" |
383 assumes "x \<noteq> y" obtains "x < y" | "y < x" |
640 assumes "x \<noteq> y" obtains "x < y" | "y < x" |
384 using assms by (rule linorder_neqE) |
641 using assms by (rule linorder_neqE) |
385 |
642 |
386 lemma eq_add_iff1: |
643 -- {* FIXME continue localization here *} |
387 "(a*e + c = b*e + d) = ((a-b)*e + c = (d::'a::ring))" |
644 |
388 by (simp add: ring_simps) |
|
389 |
|
390 lemma eq_add_iff2: |
|
391 "(a*e + c = b*e + d) = (c = (b-a)*e + (d::'a::ring))" |
|
392 by (simp add: ring_simps) |
|
393 |
|
394 lemma less_add_iff1: |
|
395 "(a*e + c < b*e + d) = ((a-b)*e + c < (d::'a::pordered_ring))" |
|
396 by (simp add: ring_simps) |
|
397 |
|
398 lemma less_add_iff2: |
|
399 "(a*e + c < b*e + d) = (c < (b-a)*e + (d::'a::pordered_ring))" |
|
400 by (simp add: ring_simps) |
|
401 |
|
402 lemma le_add_iff1: |
|
403 "(a*e + c \<le> b*e + d) = ((a-b)*e + c \<le> (d::'a::pordered_ring))" |
|
404 by (simp add: ring_simps) |
|
405 |
|
406 lemma le_add_iff2: |
|
407 "(a*e + c \<le> b*e + d) = (c \<le> (b-a)*e + (d::'a::pordered_ring))" |
|
408 by (simp add: ring_simps) |
|
409 |
|
410 |
|
411 subsection {* Ordering Rules for Multiplication *} |
|
412 |
|
413 lemma mult_left_le_imp_le: |
|
414 "[|c*a \<le> c*b; 0 < c|] ==> a \<le> (b::'a::ordered_semiring_strict)" |
|
415 by (force simp add: mult_strict_left_mono linorder_not_less [symmetric]) |
|
416 |
|
417 lemma mult_right_le_imp_le: |
|
418 "[|a*c \<le> b*c; 0 < c|] ==> a \<le> (b::'a::ordered_semiring_strict)" |
|
419 by (force simp add: mult_strict_right_mono linorder_not_less [symmetric]) |
|
420 |
|
421 lemma mult_left_less_imp_less: |
|
422 "[|c*a < c*b; 0 \<le> c|] ==> a < (b::'a::ordered_semiring)" |
|
423 by (force simp add: mult_left_mono linorder_not_le [symmetric]) |
|
424 |
|
425 lemma mult_right_less_imp_less: |
|
426 "[|a*c < b*c; 0 \<le> c|] ==> a < (b::'a::ordered_semiring)" |
|
427 by (force simp add: mult_right_mono linorder_not_le [symmetric]) |
|
428 |
|
429 lemma mult_strict_left_mono_neg: |
|
430 "[|b < a; c < 0|] ==> c * a < c * (b::'a::ordered_ring_strict)" |
|
431 apply (drule mult_strict_left_mono [of _ _ "-c"]) |
|
432 apply (simp_all add: minus_mult_left [symmetric]) |
|
433 done |
|
434 |
|
435 lemma mult_left_mono_neg: |
|
436 "[|b \<le> a; c \<le> 0|] ==> c * a \<le> c * (b::'a::pordered_ring)" |
|
437 apply (drule mult_left_mono [of _ _ "-c"]) |
|
438 apply (simp_all add: minus_mult_left [symmetric]) |
|
439 done |
|
440 |
|
441 lemma mult_strict_right_mono_neg: |
|
442 "[|b < a; c < 0|] ==> a * c < b * (c::'a::ordered_ring_strict)" |
|
443 apply (drule mult_strict_right_mono [of _ _ "-c"]) |
|
444 apply (simp_all add: minus_mult_right [symmetric]) |
|
445 done |
|
446 |
|
447 lemma mult_right_mono_neg: |
|
448 "[|b \<le> a; c \<le> 0|] ==> a * c \<le> (b::'a::pordered_ring) * c" |
|
449 apply (drule mult_right_mono [of _ _ "-c"]) |
|
450 apply (simp) |
|
451 apply (simp_all add: minus_mult_right [symmetric]) |
|
452 done |
|
453 |
|
454 |
|
455 subsection{* Products of Signs *} |
|
456 |
|
457 lemma mult_pos_pos: "[| (0::'a::ordered_semiring_strict) < a; 0 < b |] ==> 0 < a*b" |
|
458 by (drule mult_strict_left_mono [of 0 b], auto) |
|
459 |
|
460 lemma mult_nonneg_nonneg: "[| (0::'a::pordered_cancel_semiring) \<le> a; 0 \<le> b |] ==> 0 \<le> a*b" |
|
461 by (drule mult_left_mono [of 0 b], auto) |
|
462 |
|
463 lemma mult_pos_neg: "[| (0::'a::ordered_semiring_strict) < a; b < 0 |] ==> a*b < 0" |
|
464 by (drule mult_strict_left_mono [of b 0], auto) |
|
465 |
|
466 lemma mult_nonneg_nonpos: "[| (0::'a::pordered_cancel_semiring) \<le> a; b \<le> 0 |] ==> a*b \<le> 0" |
|
467 by (drule mult_left_mono [of b 0], auto) |
|
468 |
|
469 lemma mult_pos_neg2: "[| (0::'a::ordered_semiring_strict) < a; b < 0 |] ==> b*a < 0" |
|
470 by (drule mult_strict_right_mono[of b 0], auto) |
|
471 |
|
472 lemma mult_nonneg_nonpos2: "[| (0::'a::pordered_cancel_semiring) \<le> a; b \<le> 0 |] ==> b*a \<le> 0" |
|
473 by (drule mult_right_mono[of b 0], auto) |
|
474 |
|
475 lemma mult_neg_neg: "[| a < (0::'a::ordered_ring_strict); b < 0 |] ==> 0 < a*b" |
|
476 by (drule mult_strict_right_mono_neg, auto) |
|
477 |
|
478 lemma mult_nonpos_nonpos: "[| a \<le> (0::'a::pordered_ring); b \<le> 0 |] ==> 0 \<le> a*b" |
|
479 by (drule mult_right_mono_neg[of a 0 b ], auto) |
|
480 |
|
481 lemma zero_less_mult_pos: |
|
482 "[| 0 < a*b; 0 < a|] ==> 0 < (b::'a::ordered_semiring_strict)" |
|
483 apply (cases "b\<le>0") |
|
484 apply (auto simp add: order_le_less linorder_not_less) |
|
485 apply (drule_tac mult_pos_neg [of a b]) |
|
486 apply (auto dest: order_less_not_sym) |
|
487 done |
|
488 |
|
489 lemma zero_less_mult_pos2: |
|
490 "[| 0 < b*a; 0 < a|] ==> 0 < (b::'a::ordered_semiring_strict)" |
|
491 apply (cases "b\<le>0") |
|
492 apply (auto simp add: order_le_less linorder_not_less) |
|
493 apply (drule_tac mult_pos_neg2 [of a b]) |
|
494 apply (auto dest: order_less_not_sym) |
|
495 done |
|
496 |
|
497 lemma zero_less_mult_iff: |
|
498 "((0::'a::ordered_ring_strict) < a*b) = (0 < a & 0 < b | a < 0 & b < 0)" |
|
499 apply (auto simp add: order_le_less linorder_not_less mult_pos_pos |
|
500 mult_neg_neg) |
|
501 apply (blast dest: zero_less_mult_pos) |
|
502 apply (blast dest: zero_less_mult_pos2) |
|
503 done |
|
504 |
|
505 lemma mult_eq_0_iff [simp]: |
|
506 fixes a b :: "'a::ring_no_zero_divisors" |
|
507 shows "(a * b = 0) = (a = 0 \<or> b = 0)" |
|
508 by (cases "a = 0 \<or> b = 0", auto dest: no_zero_divisors) |
|
509 |
|
510 instance ordered_ring_strict \<subseteq> ring_no_zero_divisors |
|
511 apply intro_classes |
|
512 apply (auto simp add: linorder_not_less order_le_less linorder_neq_iff) |
|
513 apply (force dest: mult_strict_right_mono_neg mult_strict_right_mono)+ |
|
514 done |
|
515 |
|
516 lemma zero_le_mult_iff: |
|
517 "((0::'a::ordered_ring_strict) \<le> a*b) = (0 \<le> a & 0 \<le> b | a \<le> 0 & b \<le> 0)" |
|
518 by (auto simp add: eq_commute [of 0] order_le_less linorder_not_less |
|
519 zero_less_mult_iff) |
|
520 |
|
521 lemma mult_less_0_iff: |
|
522 "(a*b < (0::'a::ordered_ring_strict)) = (0 < a & b < 0 | a < 0 & 0 < b)" |
|
523 apply (insert zero_less_mult_iff [of "-a" b]) |
|
524 apply (force simp add: minus_mult_left[symmetric]) |
|
525 done |
|
526 |
|
527 lemma mult_le_0_iff: |
|
528 "(a*b \<le> (0::'a::ordered_ring_strict)) = (0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> b)" |
|
529 apply (insert zero_le_mult_iff [of "-a" b]) |
|
530 apply (force simp add: minus_mult_left[symmetric]) |
|
531 done |
|
532 |
|
533 lemma split_mult_pos_le: "(0 \<le> a & 0 \<le> b) | (a \<le> 0 & b \<le> 0) \<Longrightarrow> 0 \<le> a * (b::_::pordered_ring)" |
|
534 by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos) |
|
535 |
|
536 lemma split_mult_neg_le: "(0 \<le> a & b \<le> 0) | (a \<le> 0 & 0 \<le> b) \<Longrightarrow> a * b \<le> (0::_::pordered_cancel_semiring)" |
|
537 by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2) |
|
538 |
|
539 lemma zero_le_square[simp]: "(0::'a::ordered_ring_strict) \<le> a*a" |
|
540 by (simp add: zero_le_mult_iff linorder_linear) |
|
541 |
|
542 lemma not_square_less_zero[simp]: "\<not> (a * a < (0::'a::ordered_ring_strict))" |
|
543 by (simp add: not_less) |
|
544 |
645 |
545 text{*Proving axiom @{text zero_less_one} makes all @{text ordered_semidom} |
646 text{*Proving axiom @{text zero_less_one} makes all @{text ordered_semidom} |
546 theorems available to members of @{term ordered_idom} *} |
647 theorems available to members of @{term ordered_idom} *} |
547 |
648 |
548 instance ordered_idom \<subseteq> ordered_semidom |
649 instance ordered_idom \<subseteq> ordered_semidom |
583 text{*This weaker variant has more natural premises*} |
684 text{*This weaker variant has more natural premises*} |
584 lemma mult_strict_mono': |
685 lemma mult_strict_mono': |
585 "[| a<b; c<d; 0 \<le> a; 0 \<le> c|] ==> a * c < b * (d::'a::ordered_semiring_strict)" |
686 "[| a<b; c<d; 0 \<le> a; 0 \<le> c|] ==> a * c < b * (d::'a::ordered_semiring_strict)" |
586 apply (rule mult_strict_mono) |
687 apply (rule mult_strict_mono) |
587 apply (blast intro: order_le_less_trans)+ |
688 apply (blast intro: order_le_less_trans)+ |
588 done |
|
589 |
|
590 lemma mult_mono: |
|
591 "[|a \<le> b; c \<le> d; 0 \<le> b; 0 \<le> c|] |
|
592 ==> a * c \<le> b * (d::'a::pordered_semiring)" |
|
593 apply (erule mult_right_mono [THEN order_trans], assumption) |
|
594 apply (erule mult_left_mono, assumption) |
|
595 done |
|
596 |
|
597 lemma mult_mono': |
|
598 "[|a \<le> b; c \<le> d; 0 \<le> a; 0 \<le> c|] |
|
599 ==> a * c \<le> b * (d::'a::pordered_semiring)" |
|
600 apply (rule mult_mono) |
|
601 apply (fast intro: order_trans)+ |
|
602 done |
689 done |
603 |
690 |
604 lemma less_1_mult: "[| 1 < m; 1 < n |] ==> 1 < m*(n::'a::ordered_semidom)" |
691 lemma less_1_mult: "[| 1 < m; 1 < n |] ==> 1 < m*(n::'a::ordered_semidom)" |
605 apply (insert mult_strict_mono [of 1 m 1 n]) |
692 apply (insert mult_strict_mono [of 1 m 1 n]) |
606 apply (simp add: order_less_trans [OF zero_less_one]) |
693 apply (simp add: order_less_trans [OF zero_less_one]) |
802 mult_less_cancel_left1 mult_less_cancel_left2 |
889 mult_less_cancel_left1 mult_less_cancel_left2 |
803 mult_cancel_right mult_cancel_left |
890 mult_cancel_right mult_cancel_left |
804 mult_cancel_right1 mult_cancel_right2 |
891 mult_cancel_right1 mult_cancel_right2 |
805 mult_cancel_left1 mult_cancel_left2 |
892 mult_cancel_left1 mult_cancel_left2 |
806 |
893 |
807 |
|
808 subsection {* Fields *} |
|
809 |
|
810 lemma right_inverse_eq: "b \<noteq> 0 ==> (a / b = 1) = (a = (b::'a::field))" |
|
811 proof |
|
812 assume neq: "b \<noteq> 0" |
|
813 { |
|
814 hence "a = (a / b) * b" by (simp add: divide_inverse mult_ac) |
|
815 also assume "a / b = 1" |
|
816 finally show "a = b" by simp |
|
817 next |
|
818 assume "a = b" |
|
819 with neq show "a / b = 1" by (simp add: divide_inverse) |
|
820 } |
|
821 qed |
|
822 |
|
823 lemma nonzero_inverse_eq_divide: "a \<noteq> 0 ==> inverse (a::'a::field) = 1/a" |
|
824 by (simp add: divide_inverse) |
|
825 |
|
826 lemma divide_self[simp]: "a \<noteq> 0 ==> a / (a::'a::field) = 1" |
|
827 by (simp add: divide_inverse) |
|
828 |
|
829 lemma divide_zero [simp]: "a / 0 = (0::'a::{field,division_by_zero})" |
|
830 by (simp add: divide_inverse) |
|
831 |
|
832 lemma divide_self_if [simp]: |
|
833 "a / (a::'a::{field,division_by_zero}) = (if a=0 then 0 else 1)" |
|
834 by (simp add: divide_self) |
|
835 |
|
836 lemma divide_zero_left [simp]: "0/a = (0::'a::field)" |
|
837 by (simp add: divide_inverse) |
|
838 |
|
839 lemma inverse_eq_divide: "inverse (a::'a::field) = 1/a" |
|
840 by (simp add: divide_inverse) |
|
841 |
|
842 lemma add_divide_distrib: "(a+b)/(c::'a::field) = a/c + b/c" |
|
843 by (simp add: divide_inverse ring_distribs) |
|
844 |
894 |
845 (* what ordering?? this is a straight instance of mult_eq_0_iff |
895 (* what ordering?? this is a straight instance of mult_eq_0_iff |
846 text{*Compared with @{text mult_eq_0_iff}, this version removes the requirement |
896 text{*Compared with @{text mult_eq_0_iff}, this version removes the requirement |
847 of an ordering.*} |
897 of an ordering.*} |
848 lemma field_mult_eq_0_iff [simp]: |
898 lemma field_mult_eq_0_iff [simp]: |