392 "min x y + z = min (x + z) (y + z)" |
392 "min x y + z = min (x + z) (y + z)" |
393 unfolding min_def by auto |
393 unfolding min_def by auto |
394 |
394 |
395 end |
395 end |
396 |
396 |
|
397 subsection {* Support for reasoning about signs *} |
|
398 |
|
399 class pordered_comm_monoid_add = |
|
400 pordered_cancel_ab_semigroup_add + comm_monoid_add |
|
401 begin |
|
402 |
|
403 lemma add_pos_nonneg: |
|
404 assumes "0 < a" and "0 \<le> b" |
|
405 shows "0 < a + b" |
|
406 proof - |
|
407 have "0 + 0 < a + b" |
|
408 using assms by (rule add_less_le_mono) |
|
409 then show ?thesis by simp |
|
410 qed |
|
411 |
|
412 lemma add_pos_pos: |
|
413 assumes "0 < a" and "0 < b" |
|
414 shows "0 < a + b" |
|
415 by (rule add_pos_nonneg) (insert assms, auto) |
|
416 |
|
417 lemma add_nonneg_pos: |
|
418 assumes "0 \<le> a" and "0 < b" |
|
419 shows "0 < a + b" |
|
420 proof - |
|
421 have "0 + 0 < a + b" |
|
422 using assms by (rule add_le_less_mono) |
|
423 then show ?thesis by simp |
|
424 qed |
|
425 |
|
426 lemma add_nonneg_nonneg: |
|
427 assumes "0 \<le> a" and "0 \<le> b" |
|
428 shows "0 \<le> a + b" |
|
429 proof - |
|
430 have "0 + 0 \<le> a + b" |
|
431 using assms by (rule add_mono) |
|
432 then show ?thesis by simp |
|
433 qed |
|
434 |
|
435 lemma add_neg_nonpos: |
|
436 assumes "a < 0" and "b \<le> 0" |
|
437 shows "a + b < 0" |
|
438 proof - |
|
439 have "a + b < 0 + 0" |
|
440 using assms by (rule add_less_le_mono) |
|
441 then show ?thesis by simp |
|
442 qed |
|
443 |
|
444 lemma add_neg_neg: |
|
445 assumes "a < 0" and "b < 0" |
|
446 shows "a + b < 0" |
|
447 by (rule add_neg_nonpos) (insert assms, auto) |
|
448 |
|
449 lemma add_nonpos_neg: |
|
450 assumes "a \<le> 0" and "b < 0" |
|
451 shows "a + b < 0" |
|
452 proof - |
|
453 have "a + b < 0 + 0" |
|
454 using assms by (rule add_le_less_mono) |
|
455 then show ?thesis by simp |
|
456 qed |
|
457 |
|
458 lemma add_nonpos_nonpos: |
|
459 assumes "a \<le> 0" and "b \<le> 0" |
|
460 shows "a + b \<le> 0" |
|
461 proof - |
|
462 have "a + b \<le> 0 + 0" |
|
463 using assms by (rule add_mono) |
|
464 then show ?thesis by simp |
|
465 qed |
|
466 |
|
467 end |
|
468 |
397 class pordered_ab_group_add = |
469 class pordered_ab_group_add = |
398 ab_group_add + pordered_ab_semigroup_add |
470 ab_group_add + pordered_ab_semigroup_add |
399 begin |
471 begin |
400 |
472 |
401 subclass pordered_cancel_ab_semigroup_add |
473 subclass pordered_cancel_ab_semigroup_add |
582 begin |
657 begin |
583 |
658 |
584 subclass ordered_cancel_ab_semigroup_add |
659 subclass ordered_cancel_ab_semigroup_add |
585 by unfold_locales |
660 by unfold_locales |
586 |
661 |
|
662 lemma neg_less_eq_nonneg: |
|
663 "- a \<le> a \<longleftrightarrow> 0 \<le> a" |
|
664 proof |
|
665 assume A: "- a \<le> a" show "0 \<le> a" |
|
666 proof (rule classical) |
|
667 assume "\<not> 0 \<le> a" |
|
668 then have "a < 0" by auto |
|
669 with A have "- a < 0" by (rule le_less_trans) |
|
670 then show ?thesis by auto |
|
671 qed |
|
672 next |
|
673 assume A: "0 \<le> a" show "- a \<le> a" |
|
674 proof (rule order_trans) |
|
675 show "- a \<le> 0" using A by (simp add: minus_le_iff) |
|
676 next |
|
677 show "0 \<le> a" using A . |
|
678 qed |
|
679 qed |
|
680 |
|
681 lemma less_eq_neg_nonpos: |
|
682 "a \<le> - a \<longleftrightarrow> a \<le> 0" |
|
683 proof |
|
684 assume A: "a \<le> - a" show "a \<le> 0" |
|
685 proof (rule classical) |
|
686 assume "\<not> a \<le> 0" |
|
687 then have "0 < a" by auto |
|
688 then have "0 < - a" using A by (rule less_le_trans) |
|
689 then show ?thesis by auto |
|
690 qed |
|
691 next |
|
692 assume A: "a \<le> 0" show "a \<le> - a" |
|
693 proof (rule order_trans) |
|
694 show "0 \<le> - a" using A by (simp add: minus_le_iff) |
|
695 next |
|
696 show "a \<le> 0" using A . |
|
697 qed |
|
698 qed |
|
699 |
|
700 lemma equal_neg_zero: |
|
701 "a = - a \<longleftrightarrow> a = 0" |
|
702 proof |
|
703 assume "a = 0" then show "a = - a" by simp |
|
704 next |
|
705 assume A: "a = - a" show "a = 0" |
|
706 proof (cases "0 \<le> a") |
|
707 case True with A have "0 \<le> - a" by auto |
|
708 with le_minus_iff have "a \<le> 0" by simp |
|
709 with True show ?thesis by (auto intro: order_trans) |
|
710 next |
|
711 case False then have B: "a \<le> 0" by auto |
|
712 with A have "- a \<le> 0" by auto |
|
713 with B show ?thesis by (auto intro: order_trans) |
|
714 qed |
|
715 qed |
|
716 |
|
717 lemma neg_equal_zero: |
|
718 "- a = a \<longleftrightarrow> a = 0" |
|
719 unfolding equal_neg_zero [symmetric] by auto |
|
720 |
587 end |
721 end |
588 |
722 |
589 -- {* FIXME localize the following *} |
723 -- {* FIXME localize the following *} |
590 |
724 |
591 lemma add_increasing: |
725 lemma add_increasing: |
607 fixes c :: "'a::{pordered_ab_semigroup_add_imp_le, comm_monoid_add}" |
741 fixes c :: "'a::{pordered_ab_semigroup_add_imp_le, comm_monoid_add}" |
608 shows "[|0\<le>a; b<c|] ==> b < a + c" |
742 shows "[|0\<le>a; b<c|] ==> b < a + c" |
609 by (insert add_le_less_mono [of 0 a b c], simp) |
743 by (insert add_le_less_mono [of 0 a b c], simp) |
610 |
744 |
611 |
745 |
612 subsection {* Support for reasoning about signs *} |
746 class pordered_ab_group_add_abs = pordered_ab_group_add + abs + |
613 |
747 assumes abs_ge_zero [simp]: "\<bar>a\<bar> \<ge> 0" |
614 lemma add_pos_pos: "0 < |
748 and abs_ge_self: "a \<le> \<bar>a\<bar>" |
615 (x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add}) |
749 and abs_of_nonneg [simp]: "0 \<le> a \<Longrightarrow> \<bar>a\<bar> = a" |
616 ==> 0 < y ==> 0 < x + y" |
750 and abs_leI: "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b" |
617 apply (subgoal_tac "0 + 0 < x + y") |
751 and abs_eq_0 [simp]: "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0" |
618 apply simp |
752 and abs_minus_cancel [simp]: "\<bar>-a\<bar> = \<bar>a\<bar>" |
619 apply (erule add_less_le_mono) |
753 and abs_idempotent [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>" |
620 apply (erule order_less_imp_le) |
754 and abs_triangle_ineq: "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>" |
|
755 begin |
|
756 |
|
757 lemma abs_zero [simp]: "\<bar>0\<bar> = 0" |
|
758 by simp |
|
759 |
|
760 lemma abs_0_eq [simp, noatp]: "0 = \<bar>a\<bar> \<longleftrightarrow> a = 0" |
|
761 proof - |
|
762 have "0 = \<bar>a\<bar> \<longleftrightarrow> \<bar>a\<bar> = 0" by (simp only: eq_ac) |
|
763 thus ?thesis by simp |
|
764 qed |
|
765 |
|
766 lemma abs_le_zero_iff [simp]: "\<bar>a\<bar> \<le> 0 \<longleftrightarrow> a = 0" |
|
767 proof |
|
768 assume "\<bar>a\<bar> \<le> 0" |
|
769 then have "\<bar>a\<bar> = 0" by (rule antisym) simp |
|
770 thus "a = 0" by simp |
|
771 next |
|
772 assume "a = 0" |
|
773 thus "\<bar>a\<bar> \<le> 0" by simp |
|
774 qed |
|
775 |
|
776 lemma zero_less_abs_iff [simp]: "0 < \<bar>a\<bar> \<longleftrightarrow> a \<noteq> 0" |
|
777 by (simp add: less_le) |
|
778 |
|
779 lemma abs_not_less_zero [simp]: "\<not> \<bar>a\<bar> < 0" |
|
780 proof - |
|
781 have a: "\<And>x y. x \<le> y \<Longrightarrow> \<not> y < x" by auto |
|
782 show ?thesis by (simp add: a) |
|
783 qed |
|
784 |
|
785 lemma abs_ge_minus_self: "- a \<le> \<bar>a\<bar>" |
|
786 proof - |
|
787 have "- a \<le> \<bar>-a\<bar>" by (rule abs_ge_self) |
|
788 then show ?thesis by simp |
|
789 qed |
|
790 |
|
791 lemma abs_minus_commute: |
|
792 "\<bar>a - b\<bar> = \<bar>b - a\<bar>" |
|
793 proof - |
|
794 have "\<bar>a - b\<bar> = \<bar>- (a - b)\<bar>" by (simp only: abs_minus_cancel) |
|
795 also have "... = \<bar>b - a\<bar>" by simp |
|
796 finally show ?thesis . |
|
797 qed |
|
798 |
|
799 lemma abs_of_pos: "0 < a \<Longrightarrow> \<bar>a\<bar> = a" |
|
800 by (rule abs_of_nonneg, rule less_imp_le) |
|
801 |
|
802 lemma abs_of_nonpos [simp]: |
|
803 assumes "a \<le> 0" |
|
804 shows "\<bar>a\<bar> = - a" |
|
805 proof - |
|
806 let ?b = "- a" |
|
807 have "- ?b \<le> 0 \<Longrightarrow> \<bar>- ?b\<bar> = - (- ?b)" |
|
808 unfolding abs_minus_cancel [of "?b"] |
|
809 unfolding neg_le_0_iff_le [of "?b"] |
|
810 unfolding minus_minus by (erule abs_of_nonneg) |
|
811 then show ?thesis using assms by auto |
|
812 qed |
|
813 |
|
814 lemma abs_of_neg: "a < 0 \<Longrightarrow> \<bar>a\<bar> = - a" |
|
815 by (rule abs_of_nonpos, rule less_imp_le) |
|
816 |
|
817 lemma abs_le_D1: "\<bar>a\<bar> \<le> b \<Longrightarrow> a \<le> b" |
|
818 by (insert abs_ge_self, blast intro: order_trans) |
|
819 |
|
820 lemma abs_le_D2: "\<bar>a\<bar> \<le> b \<Longrightarrow> - a \<le> b" |
|
821 by (insert abs_le_D1 [of "uminus a"], simp) |
|
822 |
|
823 lemma abs_le_iff: "\<bar>a\<bar> \<le> b \<longleftrightarrow> a \<le> b \<and> - a \<le> b" |
|
824 by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2) |
|
825 |
|
826 lemma abs_triangle_ineq2: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>a - b\<bar>" |
|
827 apply (simp add: compare_rls) |
|
828 apply (subgoal_tac "abs a = abs (plus (minus a b) b)") |
|
829 apply (erule ssubst) |
|
830 apply (rule abs_triangle_ineq) |
|
831 apply (rule arg_cong) back |
|
832 apply (simp add: compare_rls) |
621 done |
833 done |
622 |
834 |
623 lemma add_pos_nonneg: "0 < |
835 lemma abs_triangle_ineq3: "\<bar>\<bar>a\<bar> - \<bar>b\<bar>\<bar> \<le> \<bar>a - b\<bar>" |
624 (x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add}) |
836 apply (subst abs_le_iff) |
625 ==> 0 <= y ==> 0 < x + y" |
837 apply auto |
626 apply (subgoal_tac "0 + 0 < x + y") |
838 apply (rule abs_triangle_ineq2) |
627 apply simp |
839 apply (subst abs_minus_commute) |
628 apply (erule add_less_le_mono, assumption) |
840 apply (rule abs_triangle_ineq2) |
629 done |
841 done |
630 |
842 |
631 lemma add_nonneg_pos: "0 <= |
843 lemma abs_triangle_ineq4: "\<bar>a - b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>" |
632 (x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add}) |
844 proof - |
633 ==> 0 < y ==> 0 < x + y" |
845 have "abs(a - b) = abs(a + - b)" |
634 apply (subgoal_tac "0 + 0 < x + y") |
846 by (subst diff_minus, rule refl) |
635 apply simp |
847 also have "... <= abs a + abs (- b)" |
636 apply (erule add_le_less_mono, assumption) |
848 by (rule abs_triangle_ineq) |
637 done |
849 finally show ?thesis |
638 |
850 by simp |
639 lemma add_nonneg_nonneg: "0 <= |
851 qed |
640 (x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add}) |
852 |
641 ==> 0 <= y ==> 0 <= x + y" |
853 lemma abs_diff_triangle_ineq: "\<bar>a + b - (c + d)\<bar> \<le> \<bar>a - c\<bar> + \<bar>b - d\<bar>" |
642 apply (subgoal_tac "0 + 0 <= x + y") |
854 proof - |
643 apply simp |
855 have "\<bar>a + b - (c+d)\<bar> = \<bar>(a-c) + (b-d)\<bar>" by (simp add: diff_minus add_ac) |
644 apply (erule add_mono, assumption) |
856 also have "... \<le> \<bar>a-c\<bar> + \<bar>b-d\<bar>" by (rule abs_triangle_ineq) |
645 done |
857 finally show ?thesis . |
646 |
858 qed |
647 lemma add_neg_neg: "(x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add}) |
859 |
648 < 0 ==> y < 0 ==> x + y < 0" |
860 lemma abs_add_abs [simp]: |
649 apply (subgoal_tac "x + y < 0 + 0") |
861 "\<bar>\<bar>a\<bar> + \<bar>b\<bar>\<bar> = \<bar>a\<bar> + \<bar>b\<bar>" (is "?L = ?R") |
650 apply simp |
862 proof (rule antisym) |
651 apply (erule add_less_le_mono) |
863 show "?L \<ge> ?R" by(rule abs_ge_self) |
652 apply (erule order_less_imp_le) |
864 next |
653 done |
865 have "?L \<le> \<bar>\<bar>a\<bar>\<bar> + \<bar>\<bar>b\<bar>\<bar>" by(rule abs_triangle_ineq) |
654 |
866 also have "\<dots> = ?R" by simp |
655 lemma add_neg_nonpos: |
867 finally show "?L \<le> ?R" . |
656 "(x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add}) < 0 |
868 qed |
657 ==> y <= 0 ==> x + y < 0" |
869 |
658 apply (subgoal_tac "x + y < 0 + 0") |
870 end |
659 apply simp |
|
660 apply (erule add_less_le_mono, assumption) |
|
661 done |
|
662 |
|
663 lemma add_nonpos_neg: |
|
664 "(x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add}) <= 0 |
|
665 ==> y < 0 ==> x + y < 0" |
|
666 apply (subgoal_tac "x + y < 0 + 0") |
|
667 apply simp |
|
668 apply (erule add_le_less_mono, assumption) |
|
669 done |
|
670 |
|
671 lemma add_nonpos_nonpos: |
|
672 "(x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add}) <= 0 |
|
673 ==> y <= 0 ==> x + y <= 0" |
|
674 apply (subgoal_tac "x + y <= 0 + 0") |
|
675 apply simp |
|
676 apply (erule add_mono, assumption) |
|
677 done |
|
678 |
871 |
679 |
872 |
680 subsection {* Lattice Ordered (Abelian) Groups *} |
873 subsection {* Lattice Ordered (Abelian) Groups *} |
681 |
874 |
682 class lordered_ab_group_meet = pordered_ab_group_add + lower_semilattice |
875 class lordered_ab_group_add_meet = pordered_ab_group_add + lower_semilattice |
683 begin |
876 begin |
684 |
877 |
685 lemma add_inf_distrib_left: |
878 lemma add_inf_distrib_left: |
686 "a + inf b c = inf (a + b) (a + c)" |
879 "a + inf b c = inf (a + b) (a + c)" |
687 apply (rule antisym) |
880 apply (rule antisym) |
980 end |
1173 end |
981 |
1174 |
982 lemmas add_sup_inf_distribs = add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left |
1175 lemmas add_sup_inf_distribs = add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left |
983 |
1176 |
984 |
1177 |
985 class pordered_ab_group_add_abs = pordered_ab_group_add + abs + |
1178 class lordered_ab_group_add_abs = lordered_ab_group_add + abs + |
986 assumes abs_ge_zero [simp]: "\<bar>a\<bar> \<ge> 0" |
|
987 and abs_ge_self: "a \<le> \<bar>a\<bar>" |
|
988 and abs_of_nonneg [simp]: "0 \<le> a \<Longrightarrow> \<bar>a\<bar> = a" |
|
989 and abs_leI: "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b" |
|
990 and abs_eq_0 [simp]: "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0" |
|
991 and abs_minus_cancel [simp]: "\<bar>-a\<bar> = \<bar>a\<bar>" |
|
992 and abs_idempotent [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>" |
|
993 and abs_triangle_ineq: "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>" |
|
994 begin |
|
995 |
|
996 lemma abs_zero [simp]: "\<bar>0\<bar> = 0" |
|
997 by simp |
|
998 |
|
999 lemma abs_0_eq [simp, noatp]: "0 = \<bar>a\<bar> \<longleftrightarrow> a = 0" |
|
1000 proof - |
|
1001 have "0 = \<bar>a\<bar> \<longleftrightarrow> \<bar>a\<bar> = 0" by (simp only: eq_ac) |
|
1002 thus ?thesis by simp |
|
1003 qed |
|
1004 |
|
1005 lemma abs_le_zero_iff [simp]: "\<bar>a\<bar> \<le> 0 \<longleftrightarrow> a = 0" |
|
1006 proof |
|
1007 assume "\<bar>a\<bar> \<le> 0" |
|
1008 then have "\<bar>a\<bar> = 0" by (rule antisym) simp |
|
1009 thus "a = 0" by simp |
|
1010 next |
|
1011 assume "a = 0" |
|
1012 thus "\<bar>a\<bar> \<le> 0" by simp |
|
1013 qed |
|
1014 |
|
1015 lemma zero_less_abs_iff [simp]: "0 < \<bar>a\<bar> \<longleftrightarrow> a \<noteq> 0" |
|
1016 by (simp add: less_le) |
|
1017 |
|
1018 lemma abs_not_less_zero [simp]: "\<not> \<bar>a\<bar> < 0" |
|
1019 proof - |
|
1020 have a: "\<And>x y. x \<le> y \<Longrightarrow> \<not> y < x" by auto |
|
1021 show ?thesis by (simp add: a) |
|
1022 qed |
|
1023 |
|
1024 lemma abs_ge_minus_self: "- a \<le> \<bar>a\<bar>" |
|
1025 proof - |
|
1026 have "- a \<le> \<bar>-a\<bar>" by (rule abs_ge_self) |
|
1027 then show ?thesis by simp |
|
1028 qed |
|
1029 |
|
1030 lemma abs_minus_commute: |
|
1031 "\<bar>a - b\<bar> = \<bar>b - a\<bar>" |
|
1032 proof - |
|
1033 have "\<bar>a - b\<bar> = \<bar>- (a - b)\<bar>" by (simp only: abs_minus_cancel) |
|
1034 also have "... = \<bar>b - a\<bar>" by simp |
|
1035 finally show ?thesis . |
|
1036 qed |
|
1037 |
|
1038 lemma abs_of_pos: "0 < a \<Longrightarrow> \<bar>a\<bar> = a" |
|
1039 by (rule abs_of_nonneg, rule less_imp_le) |
|
1040 |
|
1041 lemma abs_of_nonpos [simp]: |
|
1042 assumes "a \<le> 0" |
|
1043 shows "\<bar>a\<bar> = - a" |
|
1044 proof - |
|
1045 let ?b = "- a" |
|
1046 have "- ?b \<le> 0 \<Longrightarrow> \<bar>- ?b\<bar> = - (- ?b)" |
|
1047 unfolding abs_minus_cancel [of "?b"] |
|
1048 unfolding neg_le_0_iff_le [of "?b"] |
|
1049 unfolding minus_minus by (erule abs_of_nonneg) |
|
1050 then show ?thesis using assms by auto |
|
1051 qed |
|
1052 |
|
1053 lemma abs_of_neg: "a < 0 \<Longrightarrow> \<bar>a\<bar> = - a" |
|
1054 by (rule abs_of_nonpos, rule less_imp_le) |
|
1055 |
|
1056 lemma abs_le_D1: "\<bar>a\<bar> \<le> b \<Longrightarrow> a \<le> b" |
|
1057 by (insert abs_ge_self, blast intro: order_trans) |
|
1058 |
|
1059 lemma abs_le_D2: "\<bar>a\<bar> \<le> b \<Longrightarrow> - a \<le> b" |
|
1060 by (insert abs_le_D1 [of "uminus a"], simp) |
|
1061 |
|
1062 lemma abs_le_iff: "\<bar>a\<bar> \<le> b \<longleftrightarrow> a \<le> b \<and> - a \<le> b" |
|
1063 by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2) |
|
1064 |
|
1065 lemma abs_triangle_ineq2: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>a - b\<bar>" |
|
1066 apply (simp add: compare_rls) |
|
1067 apply (subgoal_tac "abs a = abs (plus (minus a b) b)") |
|
1068 apply (erule ssubst) |
|
1069 apply (rule abs_triangle_ineq) |
|
1070 apply (rule arg_cong) back |
|
1071 apply (simp add: compare_rls) |
|
1072 done |
|
1073 |
|
1074 lemma abs_triangle_ineq3: "\<bar>\<bar>a\<bar> - \<bar>b\<bar>\<bar> \<le> \<bar>a - b\<bar>" |
|
1075 apply (subst abs_le_iff) |
|
1076 apply auto |
|
1077 apply (rule abs_triangle_ineq2) |
|
1078 apply (subst abs_minus_commute) |
|
1079 apply (rule abs_triangle_ineq2) |
|
1080 done |
|
1081 |
|
1082 lemma abs_triangle_ineq4: "\<bar>a - b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>" |
|
1083 proof - |
|
1084 have "abs(a - b) = abs(a + - b)" |
|
1085 by (subst diff_minus, rule refl) |
|
1086 also have "... <= abs a + abs (- b)" |
|
1087 by (rule abs_triangle_ineq) |
|
1088 finally show ?thesis |
|
1089 by simp |
|
1090 qed |
|
1091 |
|
1092 lemma abs_diff_triangle_ineq: "\<bar>a + b - (c + d)\<bar> \<le> \<bar>a - c\<bar> + \<bar>b - d\<bar>" |
|
1093 proof - |
|
1094 have "\<bar>a + b - (c+d)\<bar> = \<bar>(a-c) + (b-d)\<bar>" by (simp add: diff_minus add_ac) |
|
1095 also have "... \<le> \<bar>a-c\<bar> + \<bar>b-d\<bar>" by (rule abs_triangle_ineq) |
|
1096 finally show ?thesis . |
|
1097 qed |
|
1098 |
|
1099 lemma abs_add_abs [simp]: |
|
1100 "\<bar>\<bar>a\<bar> + \<bar>b\<bar>\<bar> = \<bar>a\<bar> + \<bar>b\<bar>" (is "?L = ?R") |
|
1101 proof (rule antisym) |
|
1102 show "?L \<ge> ?R" by(rule abs_ge_self) |
|
1103 next |
|
1104 have "?L \<le> \<bar>\<bar>a\<bar>\<bar> + \<bar>\<bar>b\<bar>\<bar>" by(rule abs_triangle_ineq) |
|
1105 also have "\<dots> = ?R" by simp |
|
1106 finally show "?L \<le> ?R" . |
|
1107 qed |
|
1108 |
|
1109 end |
|
1110 |
|
1111 |
|
1112 class lordered_ab_group_abs = lordered_ab_group + abs + |
|
1113 assumes abs_lattice: "\<bar>a\<bar> = sup a (- a)" |
1179 assumes abs_lattice: "\<bar>a\<bar> = sup a (- a)" |
1114 begin |
1180 begin |
1115 |
1181 |
1116 lemma abs_prts: "\<bar>a\<bar> = pprt a - nprt a" |
1182 lemma abs_prts: "\<bar>a\<bar> = pprt a - nprt a" |
1117 proof - |
1183 proof - |