672 |
672 |
673 |
673 |
674 subsection {* Lattice Ordered (Abelian) Groups *} |
674 subsection {* Lattice Ordered (Abelian) Groups *} |
675 |
675 |
676 class lordered_ab_group_meet = pordered_ab_group_add + lower_semilattice |
676 class lordered_ab_group_meet = pordered_ab_group_add + lower_semilattice |
677 |
677 begin |
678 class lordered_ab_group_join = pordered_ab_group_add + upper_semilattice |
678 |
679 |
679 lemma add_inf_distrib_left: |
680 class lordered_ab_group = pordered_ab_group_add + lattice |
680 "a + inf b c = inf (a + b) (a + c)" |
681 |
681 apply (rule antisym) |
682 instance lordered_ab_group \<subseteq> lordered_ab_group_meet by default |
|
683 instance lordered_ab_group \<subseteq> lordered_ab_group_join by default |
|
684 |
|
685 lemma add_inf_distrib_left: "a + inf b c = inf (a + b) (a + (c::'a::{pordered_ab_group_add, lower_semilattice}))" |
|
686 apply (rule order_antisym) |
|
687 apply (simp_all add: le_infI) |
682 apply (simp_all add: le_infI) |
688 apply (rule add_le_imp_le_left [of "-a"]) |
683 apply (rule add_le_imp_le_left [of "uminus a"]) |
689 apply (simp only: add_assoc[symmetric], simp) |
684 apply (simp only: add_assoc [symmetric], simp) |
690 apply rule |
685 apply rule |
691 apply (rule add_le_imp_le_left[of "a"], simp only: add_assoc[symmetric], simp)+ |
686 apply (rule add_le_imp_le_left[of "a"], simp only: add_assoc[symmetric], simp)+ |
692 done |
687 done |
693 |
688 |
694 lemma add_sup_distrib_left: "a + sup b c = sup (a + b) (a+ (c::'a::{pordered_ab_group_add, upper_semilattice}))" |
689 lemma add_inf_distrib_right: |
695 apply (rule order_antisym) |
690 "inf a b + c = inf (a + c) (b + c)" |
696 apply (rule add_le_imp_le_left [of "-a"]) |
691 proof - |
|
692 have "c + inf a b = inf (c+a) (c+b)" by (simp add: add_inf_distrib_left) |
|
693 thus ?thesis by (simp add: add_commute) |
|
694 qed |
|
695 |
|
696 end |
|
697 |
|
698 class lordered_ab_group_join = pordered_ab_group_add + upper_semilattice |
|
699 begin |
|
700 |
|
701 lemma add_sup_distrib_left: |
|
702 "a + sup b c = sup (a + b) (a + c)" |
|
703 apply (rule antisym) |
|
704 apply (rule add_le_imp_le_left [of "uminus a"]) |
697 apply (simp only: add_assoc[symmetric], simp) |
705 apply (simp only: add_assoc[symmetric], simp) |
698 apply rule |
706 apply rule |
699 apply (rule add_le_imp_le_left [of "a"], simp only: add_assoc[symmetric], simp)+ |
707 apply (rule add_le_imp_le_left [of "a"], simp only: add_assoc[symmetric], simp)+ |
700 apply (rule le_supI) |
708 apply (rule le_supI) |
701 apply (simp_all) |
709 apply (simp_all) |
702 done |
710 done |
703 |
711 |
704 lemma add_inf_distrib_right: "inf a b + (c::'a::lordered_ab_group) = inf (a+c) (b+c)" |
712 lemma add_sup_distrib_right: |
705 proof - |
713 "sup a b + c = sup (a+c) (b+c)" |
706 have "c + inf a b = inf (c+a) (c+b)" by (simp add: add_inf_distrib_left) |
|
707 thus ?thesis by (simp add: add_commute) |
|
708 qed |
|
709 |
|
710 lemma add_sup_distrib_right: "sup a b + (c::'a::lordered_ab_group) = sup (a+c) (b+c)" |
|
711 proof - |
714 proof - |
712 have "c + sup a b = sup (c+a) (c+b)" by (simp add: add_sup_distrib_left) |
715 have "c + sup a b = sup (c+a) (c+b)" by (simp add: add_sup_distrib_left) |
713 thus ?thesis by (simp add: add_commute) |
716 thus ?thesis by (simp add: add_commute) |
714 qed |
717 qed |
715 |
718 |
|
719 end |
|
720 |
|
721 class lordered_ab_group = pordered_ab_group_add + lattice |
|
722 begin |
|
723 |
|
724 subclass lordered_ab_group_meet by unfold_locales |
|
725 subclass lordered_ab_group_join by unfold_locales |
|
726 |
|
727 end |
|
728 |
|
729 context lordered_ab_group |
|
730 begin |
|
731 |
716 lemmas add_sup_inf_distribs = add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left |
732 lemmas add_sup_inf_distribs = add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left |
717 |
733 |
718 lemma inf_eq_neg_sup: "inf a (b\<Colon>'a\<Colon>lordered_ab_group) = - sup (-a) (-b)" |
734 lemma inf_eq_neg_sup: "inf a b = - sup (-a) (-b)" |
719 proof (rule inf_unique) |
735 proof (rule inf_unique) |
720 fix a b :: 'a |
736 fix a b :: 'a |
721 show "- sup (-a) (-b) \<le> a" by (rule add_le_imp_le_right [of _ "sup (-a) (-b)"]) |
737 show "- sup (-a) (-b) \<le> a" |
722 (simp, simp add: add_sup_distrib_left) |
738 by (rule add_le_imp_le_right [of _ "sup (uminus a) (uminus b)"]) |
|
739 (simp, simp add: add_sup_distrib_left) |
723 next |
740 next |
724 fix a b :: 'a |
741 fix a b :: 'a |
725 show "- sup (-a) (-b) \<le> b" by (rule add_le_imp_le_right [of _ "sup (-a) (-b)"]) |
742 show "- sup (-a) (-b) \<le> b" |
726 (simp, simp add: add_sup_distrib_left) |
743 by (rule add_le_imp_le_right [of _ "sup (uminus a) (uminus b)"]) |
|
744 (simp, simp add: add_sup_distrib_left) |
727 next |
745 next |
728 fix a b c :: 'a |
746 fix a b c :: 'a |
729 assume "a \<le> b" "a \<le> c" |
747 assume "a \<le> b" "a \<le> c" |
730 then show "a \<le> - sup (-b) (-c)" by (subst neg_le_iff_le [symmetric]) |
748 then show "a \<le> - sup (-b) (-c)" by (subst neg_le_iff_le [symmetric]) |
731 (simp add: le_supI) |
749 (simp add: le_supI) |
732 qed |
750 qed |
733 |
751 |
734 lemma sup_eq_neg_inf: "sup a (b\<Colon>'a\<Colon>lordered_ab_group) = - inf (-a) (-b)" |
752 lemma sup_eq_neg_inf: "sup a b = - inf (-a) (-b)" |
735 proof (rule sup_unique) |
753 proof (rule sup_unique) |
736 fix a b :: 'a |
754 fix a b :: 'a |
737 show "a \<le> - inf (-a) (-b)" by (rule add_le_imp_le_right [of _ "inf (-a) (-b)"]) |
755 show "a \<le> - inf (-a) (-b)" |
738 (simp, simp add: add_inf_distrib_left) |
756 by (rule add_le_imp_le_right [of _ "inf (uminus a) (uminus b)"]) |
|
757 (simp, simp add: add_inf_distrib_left) |
739 next |
758 next |
740 fix a b :: 'a |
759 fix a b :: 'a |
741 show "b \<le> - inf (-a) (-b)" by (rule add_le_imp_le_right [of _ "inf (-a) (-b)"]) |
760 show "b \<le> - inf (-a) (-b)" |
742 (simp, simp add: add_inf_distrib_left) |
761 by (rule add_le_imp_le_right [of _ "inf (uminus a) (uminus b)"]) |
|
762 (simp, simp add: add_inf_distrib_left) |
743 next |
763 next |
744 fix a b c :: 'a |
764 fix a b c :: 'a |
745 assume "a \<le> c" "b \<le> c" |
765 assume "a \<le> c" "b \<le> c" |
746 then show "- inf (-a) (-b) \<le> c" by (subst neg_le_iff_le [symmetric]) |
766 then show "- inf (-a) (-b) \<le> c" by (subst neg_le_iff_le [symmetric]) |
747 (simp add: le_infI) |
767 (simp add: le_infI) |
748 qed |
768 qed |
749 |
769 |
750 lemma add_eq_inf_sup: "a + b = sup a b + inf a (b\<Colon>'a\<Colon>lordered_ab_group)" |
770 lemma add_eq_inf_sup: "a + b = sup a b + inf a b" |
751 proof - |
771 proof - |
752 have "0 = - inf 0 (a-b) + inf (a-b) 0" by (simp add: inf_commute) |
772 have "0 = - inf 0 (a-b) + inf (a-b) 0" by (simp add: inf_commute) |
753 hence "0 = sup 0 (b-a) + inf (a-b) 0" by (simp add: inf_eq_neg_sup) |
773 hence "0 = sup 0 (b-a) + inf (a-b) 0" by (simp add: inf_eq_neg_sup) |
754 hence "0 = (-a + sup a b) + (inf a b + (-b))" |
774 hence "0 = (-a + sup a b) + (inf a b + (-b))" |
755 apply (simp add: add_sup_distrib_left add_inf_distrib_right) |
775 apply (simp add: add_sup_distrib_left add_inf_distrib_right) |
756 by (simp add: diff_minus add_commute) |
776 by (simp add: diff_minus add_commute) |
757 thus ?thesis |
777 thus ?thesis |
758 apply (simp add: compare_rls) |
778 apply (simp add: compare_rls) |
759 apply (subst add_left_cancel[symmetric, of "a+b" "sup a b + inf a b" "-a"]) |
779 apply (subst add_left_cancel [symmetric, of "plus a b" "plus (sup a b) (inf a b)" "uminus a"]) |
760 apply (simp only: add_assoc, simp add: add_assoc[symmetric]) |
780 apply (simp only: add_assoc, simp add: add_assoc[symmetric]) |
761 done |
781 done |
762 qed |
782 qed |
763 |
783 |
764 subsection {* Positive Part, Negative Part, Absolute Value *} |
784 subsection {* Positive Part, Negative Part, Absolute Value *} |
765 |
785 |
766 definition |
786 definition |
767 nprt :: "'a \<Rightarrow> ('a::lordered_ab_group)" where |
787 nprt :: "'a \<Rightarrow> 'a" where |
768 "nprt x = inf x 0" |
788 "nprt x = inf x 0" |
769 |
789 |
770 definition |
790 definition |
771 pprt :: "'a \<Rightarrow> ('a::lordered_ab_group)" where |
791 pprt :: "'a \<Rightarrow> 'a" where |
772 "pprt x = sup x 0" |
792 "pprt x = sup x 0" |
773 |
793 |
774 lemma prts: "a = pprt a + nprt a" |
794 lemma prts: "a = pprt a + nprt a" |
775 by (simp add: pprt_def nprt_def add_eq_inf_sup[symmetric]) |
795 by (simp add: pprt_def nprt_def add_eq_inf_sup[symmetric]) |
776 |
796 |
777 lemma zero_le_pprt[simp]: "0 \<le> pprt a" |
797 lemma zero_le_pprt[simp]: "0 \<le> pprt a" |
778 by (simp add: pprt_def) |
798 by (simp add: pprt_def) |
779 |
799 |
780 lemma nprt_le_zero[simp]: "nprt a \<le> 0" |
800 lemma nprt_le_zero[simp]: "nprt a \<le> 0" |
781 by (simp add: nprt_def) |
801 by (simp add: nprt_def) |
782 |
802 |
783 lemma le_eq_neg: "(a \<le> -b) = (a + b \<le> (0::_::lordered_ab_group))" (is "?l = ?r") |
803 lemma le_eq_neg: "a \<le> - b \<longleftrightarrow> a + b \<le> 0" (is "?l = ?r") |
784 proof - |
804 proof - |
785 have a: "?l \<longrightarrow> ?r" |
805 have a: "?l \<longrightarrow> ?r" |
786 apply (auto) |
806 apply (auto) |
787 apply (rule add_le_imp_le_right[of _ "-b" _]) |
807 apply (rule add_le_imp_le_right[of _ "uminus b" _]) |
788 apply (simp add: add_assoc) |
808 apply (simp add: add_assoc) |
789 done |
809 done |
790 have b: "?r \<longrightarrow> ?l" |
810 have b: "?r \<longrightarrow> ?l" |
791 apply (auto) |
811 apply (auto) |
792 apply (rule add_le_imp_le_right[of _ "b" _]) |
812 apply (rule add_le_imp_le_right[of _ "b" _]) |
824 assume hyp:"sup a (-a) = 0" |
844 assume hyp:"sup a (-a) = 0" |
825 hence hyp2:"sup (-a) (-(-a)) = 0" by (simp add: sup_commute) |
845 hence hyp2:"sup (-a) (-(-a)) = 0" by (simp add: sup_commute) |
826 from p[OF hyp] p[OF hyp2] show "a = 0" by simp |
846 from p[OF hyp] p[OF hyp2] show "a = 0" by simp |
827 qed |
847 qed |
828 |
848 |
829 lemma inf_0_imp_0: "inf a (-a) = 0 \<Longrightarrow> a = (0::'a::lordered_ab_group)" |
849 lemma inf_0_imp_0: "inf a (-a) = 0 \<Longrightarrow> a = 0" |
830 apply (simp add: inf_eq_neg_sup) |
850 apply (simp add: inf_eq_neg_sup) |
831 apply (simp add: sup_commute) |
851 apply (simp add: sup_commute) |
832 apply (erule sup_0_imp_0) |
852 apply (erule sup_0_imp_0) |
833 done |
853 done |
834 |
854 |
835 lemma inf_0_eq_0[simp,noatp]: "(inf a (-a) = 0) = (a = (0::'a::lordered_ab_group))" |
855 lemma inf_0_eq_0 [simp, noatp]: "inf a (- a) = 0 \<longleftrightarrow> a = 0" |
836 by (auto, erule inf_0_imp_0) |
856 by (rule, erule inf_0_imp_0) simp |
837 |
857 |
838 lemma sup_0_eq_0[simp,noatp]: "(sup a (-a) = 0) = (a = (0::'a::lordered_ab_group))" |
858 lemma sup_0_eq_0 [simp, noatp]: "sup a (- a) = 0 \<longleftrightarrow> a = 0" |
839 by (auto, erule sup_0_imp_0) |
859 by (rule, erule sup_0_imp_0) simp |
840 |
860 |
841 lemma zero_le_double_add_iff_zero_le_single_add[simp]: "(0 \<le> a + a) = (0 \<le> (a::'a::lordered_ab_group))" |
861 lemma zero_le_double_add_iff_zero_le_single_add [simp]: |
|
862 "0 \<le> a + a \<longleftrightarrow> 0 \<le> a" |
842 proof |
863 proof |
843 assume "0 <= a + a" |
864 assume "0 <= a + a" |
844 hence a:"inf (a+a) 0 = 0" by (simp add: le_iff_inf inf_commute) |
865 hence a:"inf (a+a) 0 = 0" by (simp add: le_iff_inf inf_commute) |
845 have "(inf a 0)+(inf a 0) = inf (inf (a+a) 0) a" (is "?l=_") by (simp add: add_sup_inf_distribs inf_aci) |
866 have "(inf a 0)+(inf a 0) = inf (inf (a+a) 0) a" (is "?l=_") |
|
867 by (simp add: add_sup_inf_distribs inf_ACI) |
846 hence "?l = 0 + inf a 0" by (simp add: a, simp add: inf_commute) |
868 hence "?l = 0 + inf a 0" by (simp add: a, simp add: inf_commute) |
847 hence "inf a 0 = 0" by (simp only: add_right_cancel) |
869 hence "inf a 0 = 0" by (simp only: add_right_cancel) |
848 then show "0 <= a" by (simp add: le_iff_inf inf_commute) |
870 then show "0 <= a" by (simp add: le_iff_inf inf_commute) |
849 next |
871 next |
850 assume a: "0 <= a" |
872 assume a: "0 <= a" |
851 show "0 <= a + a" by (simp add: add_mono[OF a a, simplified]) |
873 show "0 <= a + a" by (simp add: add_mono[OF a a, simplified]) |
852 qed |
874 qed |
853 |
875 |
854 lemma double_add_le_zero_iff_single_add_le_zero[simp]: "(a + a <= 0) = ((a::'a::lordered_ab_group) <= 0)" |
876 lemma double_zero: "a + a = 0 \<longleftrightarrow> a = 0" |
855 proof - |
877 proof |
856 have "(a + a <= 0) = (0 <= -(a+a))" by (subst le_minus_iff, simp) |
878 assume assm: "a + a = 0" |
857 moreover have "\<dots> = (a <= 0)" by (simp add: zero_le_double_add_iff_zero_le_single_add) |
879 then have "a + a + - a = - a" by simp |
|
880 then have "a + (a + - a) = - a" by (simp only: add_assoc) |
|
881 then have a: "- a = a" by simp (*FIXME tune proof*) |
|
882 show "a = 0" apply rule |
|
883 apply (unfold neg_le_iff_le [symmetric, of a]) |
|
884 unfolding a apply simp |
|
885 unfolding zero_le_double_add_iff_zero_le_single_add [symmetric, of a] |
|
886 unfolding assm unfolding le_less apply simp_all done |
|
887 next |
|
888 assume "a = 0" then show "a + a = 0" by simp |
|
889 qed |
|
890 |
|
891 lemma zero_less_double_add_iff_zero_less_single_add: |
|
892 "0 < a + a \<longleftrightarrow> 0 < a" |
|
893 proof (cases "a = 0") |
|
894 case True then show ?thesis by auto |
|
895 next |
|
896 case False then show ?thesis (*FIXME tune proof*) |
|
897 unfolding less_le apply simp apply rule |
|
898 apply clarify |
|
899 apply rule |
|
900 apply assumption |
|
901 apply (rule notI) |
|
902 unfolding double_zero [symmetric, of a] apply simp |
|
903 done |
|
904 qed |
|
905 |
|
906 lemma double_add_le_zero_iff_single_add_le_zero [simp]: |
|
907 "a + a \<le> 0 \<longleftrightarrow> a \<le> 0" |
|
908 proof - |
|
909 have "a + a \<le> 0 \<longleftrightarrow> 0 \<le> - (a + a)" by (subst le_minus_iff, simp) |
|
910 moreover have "\<dots> \<longleftrightarrow> a \<le> 0" by (simp add: zero_le_double_add_iff_zero_le_single_add) |
858 ultimately show ?thesis by blast |
911 ultimately show ?thesis by blast |
859 qed |
912 qed |
860 |
913 |
861 lemma double_add_less_zero_iff_single_less_zero[simp]: "(a+a<0) = ((a::'a::{pordered_ab_group_add,linorder}) < 0)" (is ?s) |
914 lemma double_add_less_zero_iff_single_less_zero [simp]: |
862 proof cases |
915 "a + a < 0 \<longleftrightarrow> a < 0" |
863 assume a: "a < 0" |
916 proof - |
864 thus ?s by (simp add: add_strict_mono[OF a a, simplified]) |
917 have "a + a < 0 \<longleftrightarrow> 0 < - (a + a)" by (subst less_minus_iff, simp) |
865 next |
918 moreover have "\<dots> \<longleftrightarrow> a < 0" by (simp add: zero_less_double_add_iff_zero_less_single_add) |
866 assume "~(a < 0)" |
919 ultimately show ?thesis by blast |
867 hence a:"0 <= a" by (simp) |
920 qed |
868 hence "0 <= a+a" by (simp add: add_mono[OF a a, simplified]) |
921 |
869 hence "~(a+a < 0)" by simp |
922 end |
870 with a show ?thesis by simp |
923 |
871 qed |
924 lemmas add_sup_inf_distribs = add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left |
872 |
925 |
873 class lordered_ab_group_abs = lordered_ab_group + abs + |
926 class lordered_ab_group_abs = lordered_ab_group + abs + |
874 assumes abs_lattice: "abs x = sup x (uminus x)" |
927 assumes abs_lattice: "\<bar>x\<bar> = sup x (- x)" |
875 |
928 begin |
876 lemma abs_zero[simp]: "abs 0 = (0::'a::lordered_ab_group_abs)" |
929 |
877 by (simp add: abs_lattice) |
930 lemma abs_zero [simp]: "\<bar>0\<bar> = 0" |
878 |
931 by (simp add: abs_lattice) |
879 lemma abs_eq_0[simp]: "(abs a = 0) = (a = (0::'a::lordered_ab_group_abs))" |
932 |
880 by (simp add: abs_lattice) |
933 lemma abs_eq_0 [simp]: "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0" |
881 |
934 by (simp add: abs_lattice) |
882 lemma abs_0_eq[simp]: "(0 = abs a) = (a = (0::'a::lordered_ab_group_abs))" |
935 |
|
936 lemma abs_0_eq [simp, noatp]: "0 = \<bar>a\<bar> \<longleftrightarrow> a = 0" |
883 proof - |
937 proof - |
884 have "(0 = abs a) = (abs a = 0)" by (simp only: eq_ac) |
938 have "(0 = abs a) = (abs a = 0)" by (simp only: eq_ac) |
885 thus ?thesis by simp |
939 thus ?thesis by simp |
886 qed |
940 qed |
887 |
941 |
888 declare abs_0_eq [noatp] (*essentially the same as the other one*) |
942 lemma neg_inf_eq_sup [simp]: "- inf a b = sup (-a) (-b)" |
889 |
943 by (simp add: inf_eq_neg_sup) |
890 lemma neg_inf_eq_sup[simp]: "- inf a (b::_::lordered_ab_group) = sup (-a) (-b)" |
944 |
891 by (simp add: inf_eq_neg_sup) |
945 lemma neg_sup_eq_inf [simp]: "- sup a b = inf (-a) (-b)" |
892 |
946 by (simp del: neg_inf_eq_sup add: sup_eq_neg_inf) |
893 lemma neg_sup_eq_inf[simp]: "- sup a (b::_::lordered_ab_group) = inf (-a) (-b)" |
947 |
894 by (simp del: neg_inf_eq_sup add: sup_eq_neg_inf) |
948 lemma abs_ge_zero [simp]: "0 \<le> \<bar>a\<bar>" |
895 |
949 proof - |
896 lemma sup_eq_if: "sup a (-a) = (if a < 0 then -a else (a::'a::{lordered_ab_group, linorder}))" |
950 have a: "a \<le> \<bar>a\<bar>" and b: "- a \<le> \<bar>a\<bar>" by (auto simp add: abs_lattice) |
897 proof - |
951 show ?thesis by (rule add_mono [OF a b, simplified]) |
898 note b = add_le_cancel_right[of a a "-a",symmetric,simplified] |
|
899 have c: "a + a = 0 \<Longrightarrow> -a = a" by (rule add_right_imp_eq[of _ a], simp) |
|
900 show ?thesis by (auto simp add: max_def b linorder_not_less sup_max) |
|
901 qed |
|
902 |
|
903 lemma abs_if_lattice: "\<bar>a\<bar> = (if a < 0 then -a else (a::'a::{lordered_ab_group_abs, linorder}))" |
|
904 proof - |
|
905 show ?thesis by (simp add: abs_lattice sup_eq_if) |
|
906 qed |
|
907 |
|
908 lemma abs_ge_zero[simp]: "0 \<le> abs (a::'a::lordered_ab_group_abs)" |
|
909 proof - |
|
910 have a:"a <= abs a" and b:"-a <= abs a" by (auto simp add: abs_lattice) |
|
911 show ?thesis by (rule add_mono[OF a b, simplified]) |
|
912 qed |
952 qed |
913 |
953 |
914 lemma abs_le_zero_iff [simp]: "(abs a \<le> (0::'a::lordered_ab_group_abs)) = (a = 0)" |
954 lemma abs_le_zero_iff [simp]: "\<bar>a\<bar> \<le> 0 \<longleftrightarrow> a = 0" |
915 proof |
955 proof |
916 assume "abs a <= 0" |
956 assume "\<bar>a\<bar> \<le> 0" |
917 hence "abs a = 0" by (auto dest: order_antisym) |
957 then have "\<bar>a\<bar> = 0" by (rule antisym) simp |
918 thus "a = 0" by simp |
958 thus "a = 0" by simp |
919 next |
959 next |
920 assume "a = 0" |
960 assume "a = 0" |
921 thus "abs a <= 0" by simp |
961 thus "\<bar>a\<bar> \<le> 0" by simp |
922 qed |
962 qed |
923 |
963 |
924 lemma zero_less_abs_iff [simp]: "(0 < abs a) = (a \<noteq> (0::'a::lordered_ab_group_abs))" |
964 lemma zero_less_abs_iff [simp]: "0 < \<bar>a\<bar> \<longleftrightarrow> a \<noteq> 0" |
925 by (simp add: order_less_le) |
965 by (simp add: less_le) |
926 |
966 |
927 lemma abs_not_less_zero [simp]: "~ abs a < (0::'a::lordered_ab_group_abs)" |
967 lemma abs_not_less_zero [simp]: "\<not> \<bar>a\<bar> < 0" |
928 proof - |
968 proof - |
929 have a:"!! x (y::_::order). x <= y \<Longrightarrow> ~(y < x)" by auto |
969 have a: "\<And>x y. x \<le> y \<Longrightarrow> \<not> y < x" by auto |
930 show ?thesis by (simp add: a) |
970 show ?thesis by (simp add: a) |
931 qed |
971 qed |
932 |
972 |
933 lemma abs_ge_self: "a \<le> abs (a::'a::lordered_ab_group_abs)" |
973 lemma abs_ge_self: "a \<le> \<bar>a\<bar>" |
934 by (simp add: abs_lattice) |
974 by (auto simp add: abs_lattice) |
935 |
975 |
936 lemma abs_ge_minus_self: "-a \<le> abs (a::'a::lordered_ab_group_abs)" |
976 lemma abs_ge_minus_self: "- a \<le> \<bar>a\<bar>" |
937 by (simp add: abs_lattice) |
977 by (auto simp add: abs_lattice) |
938 |
978 |
939 lemma abs_prts: "abs (a::_::lordered_ab_group_abs) = pprt a - nprt a" |
979 lemma abs_minus_cancel [simp]: "\<bar>-a\<bar> = \<bar>a\<bar>" |
940 apply (simp add: pprt_def nprt_def diff_minus) |
980 by (simp add: abs_lattice sup_commute) |
941 apply (simp add: add_sup_inf_distribs sup_aci abs_lattice[symmetric]) |
981 |
942 apply (subst sup_absorb2, auto) |
982 lemma abs_idempotent [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>" |
943 done |
983 apply (simp add: abs_lattice [of "abs a"]) |
944 |
|
945 lemma abs_minus_cancel [simp]: "abs (-a) = abs(a::'a::lordered_ab_group_abs)" |
|
946 by (simp add: abs_lattice sup_commute) |
|
947 |
|
948 lemma abs_idempotent [simp]: "abs (abs a) = abs (a::'a::lordered_ab_group_abs)" |
|
949 apply (simp add: abs_lattice[of "abs a"]) |
|
950 apply (subst sup_absorb1) |
984 apply (subst sup_absorb1) |
951 apply (rule order_trans[of _ 0]) |
985 apply (rule order_trans [of _ zero]) |
952 by auto |
986 by auto |
953 |
987 |
954 lemma abs_minus_commute: |
988 lemma abs_minus_commute: |
955 fixes a :: "'a::lordered_ab_group_abs" |
989 "\<bar>a - b\<bar> = \<bar>b - a\<bar>" |
956 shows "abs (a-b) = abs(b-a)" |
990 proof - |
957 proof - |
991 have "\<bar>a - b\<bar> = \<bar>- (a - b)\<bar>" by (simp only: abs_minus_cancel) |
958 have "abs (a-b) = abs (- (a-b))" by (simp only: abs_minus_cancel) |
992 also have "... = \<bar>b - a\<bar>" by simp |
959 also have "... = abs(b-a)" by simp |
|
960 finally show ?thesis . |
993 finally show ?thesis . |
961 qed |
994 qed |
962 |
995 |
963 lemma zero_le_iff_zero_nprt: "(0 \<le> a) = (nprt a = 0)" |
996 lemma abs_prts: "\<bar>a\<bar> = pprt a - nprt a" |
|
997 proof - |
|
998 have "0 \<le> \<bar>a\<bar>" by simp |
|
999 then have "0 \<le> sup a (- a)" unfolding abs_lattice . |
|
1000 then have "sup (sup a (- a)) 0 = sup a (- a)" by (rule sup_absorb1) |
|
1001 then show ?thesis |
|
1002 by (simp add: add_sup_inf_distribs sup_ACI |
|
1003 pprt_def nprt_def diff_minus abs_lattice) |
|
1004 qed |
|
1005 |
|
1006 lemma zero_le_iff_zero_nprt: "0 \<le> a \<longleftrightarrow> nprt a = 0" |
|
1007 by (simp add: le_iff_inf nprt_def inf_commute) |
|
1008 |
|
1009 lemma le_zero_iff_zero_pprt: "a \<le> 0 \<longleftrightarrow> pprt a = 0" |
|
1010 by (simp add: le_iff_sup pprt_def sup_commute) |
|
1011 |
|
1012 lemma le_zero_iff_pprt_id: "0 \<le> a \<longleftrightarrow> pprt a = a" |
|
1013 by (simp add: le_iff_sup pprt_def sup_commute) |
|
1014 |
|
1015 lemma zero_le_iff_nprt_id: "a \<le> 0 \<longleftrightarrow> nprt a = a" |
964 by (simp add: le_iff_inf nprt_def inf_commute) |
1016 by (simp add: le_iff_inf nprt_def inf_commute) |
965 |
1017 |
966 lemma le_zero_iff_zero_pprt: "(a \<le> 0) = (pprt a = 0)" |
1018 lemma pprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> pprt a \<le> pprt b" |
967 by (simp add: le_iff_sup pprt_def sup_commute) |
1019 by (simp add: le_iff_sup pprt_def sup_ACI sup_assoc [symmetric, of a]) |
968 |
1020 |
969 lemma le_zero_iff_pprt_id: "(0 \<le> a) = (pprt a = a)" |
1021 lemma nprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> nprt a \<le> nprt b" |
970 by (simp add: le_iff_sup pprt_def sup_commute) |
1022 by (simp add: le_iff_inf nprt_def inf_ACI inf_assoc [symmetric, of a]) |
971 |
1023 |
972 lemma zero_le_iff_nprt_id: "(a \<le> 0) = (nprt a = a)" |
1024 lemma pprt_neg: "pprt (- x) = - nprt x" |
973 by (simp add: le_iff_inf nprt_def inf_commute) |
|
974 |
|
975 lemma pprt_mono[simp,noatp]: "(a::_::lordered_ab_group) <= b \<Longrightarrow> pprt a <= pprt b" |
|
976 by (simp add: le_iff_sup pprt_def sup_aci) |
|
977 |
|
978 lemma nprt_mono[simp,noatp]: "(a::_::lordered_ab_group) <= b \<Longrightarrow> nprt a <= nprt b" |
|
979 by (simp add: le_iff_inf nprt_def inf_aci) |
|
980 |
|
981 lemma pprt_neg: "pprt (-x) = - nprt x" |
|
982 by (simp add: pprt_def nprt_def) |
1025 by (simp add: pprt_def nprt_def) |
983 |
1026 |
984 lemma nprt_neg: "nprt (-x) = - pprt x" |
1027 lemma nprt_neg: "nprt (- x) = - pprt x" |
985 by (simp add: pprt_def nprt_def) |
1028 by (simp add: pprt_def nprt_def) |
986 |
1029 |
987 lemma abs_of_nonneg [simp]: "0 \<le> a \<Longrightarrow> abs a = (a::'a::lordered_ab_group_abs)" |
1030 lemma abs_of_nonneg [simp]: "0 \<le> a \<Longrightarrow> \<bar>a\<bar> = a" |
988 by (simp add: iffD1[OF zero_le_iff_zero_nprt] iffD1[OF le_zero_iff_pprt_id] abs_prts) |
1031 by (simp add: iffD1 [OF zero_le_iff_zero_nprt] |
989 |
1032 iffD1[OF le_zero_iff_pprt_id] abs_prts) |
990 lemma abs_of_pos: "0 < (x::'a::lordered_ab_group_abs) ==> abs x = x"; |
1033 |
991 by (rule abs_of_nonneg, rule order_less_imp_le); |
1034 lemma abs_of_pos: "0 < x \<Longrightarrow> \<bar>x\<bar> = x" |
992 |
1035 by (rule abs_of_nonneg, rule less_imp_le) |
993 lemma abs_of_nonpos [simp]: "a \<le> 0 \<Longrightarrow> abs a = -(a::'a::lordered_ab_group_abs)" |
1036 |
994 by (simp add: iffD1[OF le_zero_iff_zero_pprt] iffD1[OF zero_le_iff_nprt_id] abs_prts) |
1037 lemma abs_of_nonpos [simp]: "a \<le> 0 \<Longrightarrow> \<bar>a\<bar> = - a" |
995 |
1038 by (simp add: iffD1 [OF le_zero_iff_zero_pprt] |
996 lemma abs_of_neg: "(x::'a::lordered_ab_group_abs) < 0 ==> |
1039 iffD1 [OF zero_le_iff_nprt_id] abs_prts) |
997 abs x = - x" |
1040 |
998 by (rule abs_of_nonpos, rule order_less_imp_le) |
1041 lemma abs_of_neg: "x < 0 \<Longrightarrow> \<bar>x\<bar> = - x" |
999 |
1042 by (rule abs_of_nonpos, rule less_imp_le) |
1000 lemma abs_leI: "[|a \<le> b; -a \<le> b|] ==> abs a \<le> (b::'a::lordered_ab_group_abs)" |
1043 |
1001 by (simp add: abs_lattice le_supI) |
1044 lemma abs_leI: "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b" |
1002 |
1045 by (simp add: abs_lattice le_supI) |
1003 lemma le_minus_self_iff: "(a \<le> -a) = (a \<le> (0::'a::lordered_ab_group))" |
1046 |
1004 proof - |
1047 lemma le_minus_self_iff: "a \<le> - a \<longleftrightarrow> a \<le> 0" |
1005 from add_le_cancel_left[of "-a" "a+a" "0"] have "(a <= -a) = (a+a <= 0)" |
1048 proof - |
|
1049 from add_le_cancel_left [of "uminus a" "plus a a" zero] |
|
1050 have "(a <= -a) = (a+a <= 0)" |
1006 by (simp add: add_assoc[symmetric]) |
1051 by (simp add: add_assoc[symmetric]) |
1007 thus ?thesis by simp |
1052 thus ?thesis by simp |
1008 qed |
1053 qed |
1009 |
1054 |
1010 lemma minus_le_self_iff: "(-a \<le> a) = (0 \<le> (a::'a::lordered_ab_group))" |
1055 lemma minus_le_self_iff: "- a \<le> a \<longleftrightarrow> 0 \<le> a" |
1011 proof - |
1056 proof - |
1012 from add_le_cancel_left[of "-a" "0" "a+a"] have "(-a <= a) = (0 <= a+a)" |
1057 from add_le_cancel_left [of "uminus a" zero "plus a a"] |
|
1058 have "(-a <= a) = (0 <= a+a)" |
1013 by (simp add: add_assoc[symmetric]) |
1059 by (simp add: add_assoc[symmetric]) |
1014 thus ?thesis by simp |
1060 thus ?thesis by simp |
1015 qed |
1061 qed |
1016 |
1062 |
1017 lemma abs_le_D1: "abs a \<le> b ==> a \<le> (b::'a::lordered_ab_group_abs)" |
1063 lemma abs_le_D1: "\<bar>a\<bar> \<le> b \<Longrightarrow> a \<le> b" |
1018 by (insert abs_ge_self, blast intro: order_trans) |
1064 by (insert abs_ge_self, blast intro: order_trans) |
1019 |
1065 |
1020 lemma abs_le_D2: "abs a \<le> b ==> -a \<le> (b::'a::lordered_ab_group_abs)" |
1066 lemma abs_le_D2: "\<bar>a\<bar> \<le> b \<Longrightarrow> - a \<le> b" |
1021 by (insert abs_le_D1 [of "-a"], simp) |
1067 by (insert abs_le_D1 [of "uminus a"], simp) |
1022 |
1068 |
1023 lemma abs_le_iff: "(abs a \<le> b) = (a \<le> b & -a \<le> (b::'a::lordered_ab_group_abs))" |
1069 lemma abs_le_iff: "\<bar>a\<bar> \<le> b \<longleftrightarrow> a \<le> b \<and> - a \<le> b" |
1024 by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2) |
1070 by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2) |
1025 |
1071 |
1026 lemma abs_triangle_ineq: "abs(a+b) \<le> abs a + abs(b::'a::lordered_ab_group_abs)" |
1072 lemma abs_triangle_ineq: "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>" |
1027 proof - |
1073 proof - |
1028 have g:"abs a + abs b = sup (a+b) (sup (-a-b) (sup (-a+b) (a + (-b))))" (is "_=sup ?m ?n") |
1074 have g:"abs a + abs b = sup (a+b) (sup (-a-b) (sup (-a+b) (a + (-b))))" (is "_=sup ?m ?n") |
1029 by (simp add: abs_lattice add_sup_inf_distribs sup_aci diff_minus) |
1075 by (simp add: abs_lattice add_sup_inf_distribs sup_ACI diff_minus) |
1030 have a:"a+b <= sup ?m ?n" by (simp) |
1076 have a:"a+b <= sup ?m ?n" by (simp) |
1031 have b:"-a-b <= ?n" by (simp) |
1077 have b:"-a-b <= ?n" by (simp) |
1032 have c:"?n <= sup ?m ?n" by (simp) |
1078 have c:"?n <= sup ?m ?n" by (simp) |
1033 from b c have d: "-a-b <= sup ?m ?n" by(rule order_trans) |
1079 from b c have d: "-a-b <= sup ?m ?n" by(rule order_trans) |
1034 have e:"-a-b = -(a+b)" by (simp add: diff_minus) |
1080 have e:"-a-b = -(a+b)" by (simp add: diff_minus) |
1035 from a d e have "abs(a+b) <= sup ?m ?n" |
1081 from a d e have "abs(a+b) <= sup ?m ?n" |
1036 by (drule_tac abs_leI, auto) |
1082 by (drule_tac abs_leI, auto) |
1037 with g[symmetric] show ?thesis by simp |
1083 with g[symmetric] show ?thesis by simp |
1038 qed |
1084 qed |
1039 |
1085 |
1040 lemma abs_triangle_ineq2: "abs (a::'a::lordered_ab_group_abs) - |
1086 lemma abs_triangle_ineq2: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>a - b\<bar>" |
1041 abs b <= abs (a - b)" |
|
1042 apply (simp add: compare_rls) |
1087 apply (simp add: compare_rls) |
1043 apply (subgoal_tac "abs a = abs (a - b + b)") |
1088 apply (subgoal_tac "abs a = abs (plus (minus a b) b)") |
1044 apply (erule ssubst) |
1089 apply (erule ssubst) |
1045 apply (rule abs_triangle_ineq) |
1090 apply (rule abs_triangle_ineq) |
1046 apply (rule arg_cong);back; |
1091 apply (rule arg_cong) back |
1047 apply (simp add: compare_rls) |
1092 apply (simp add: compare_rls) |
1048 done |
1093 done |
1049 |
1094 |
1050 lemma abs_triangle_ineq3: |
1095 lemma abs_triangle_ineq3: "\<bar>\<bar>a\<bar> - \<bar>b\<bar>\<bar> \<le> \<bar>a - b\<bar>" |
1051 "abs(abs (a::'a::lordered_ab_group_abs) - abs b) <= abs (a - b)" |
|
1052 apply (subst abs_le_iff) |
1096 apply (subst abs_le_iff) |
1053 apply auto |
1097 apply auto |
1054 apply (rule abs_triangle_ineq2) |
1098 apply (rule abs_triangle_ineq2) |
1055 apply (subst abs_minus_commute) |
1099 apply (subst abs_minus_commute) |
1056 apply (rule abs_triangle_ineq2) |
1100 apply (rule abs_triangle_ineq2) |
1057 done |
1101 done |
1058 |
1102 |
1059 lemma abs_triangle_ineq4: "abs ((a::'a::lordered_ab_group_abs) - b) <= |
1103 lemma abs_triangle_ineq4: "\<bar>a - b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>" |
1060 abs a + abs b" |
1104 proof - |
1061 proof -; |
|
1062 have "abs(a - b) = abs(a + - b)" |
1105 have "abs(a - b) = abs(a + - b)" |
1063 by (subst diff_minus, rule refl) |
1106 by (subst diff_minus, rule refl) |
1064 also have "... <= abs a + abs (- b)" |
1107 also have "... <= abs a + abs (- b)" |
1065 by (rule abs_triangle_ineq) |
1108 by (rule abs_triangle_ineq) |
1066 finally show ?thesis |
1109 finally show ?thesis |
1067 by simp |
1110 by simp |
1068 qed |
1111 qed |
1069 |
1112 |
1070 lemma abs_diff_triangle_ineq: |
1113 lemma abs_diff_triangle_ineq: "\<bar>a + b - (c + d)\<bar> \<le> \<bar>a - c\<bar> + \<bar>b - d\<bar>" |
1071 "\<bar>(a::'a::lordered_ab_group_abs) + b - (c+d)\<bar> \<le> \<bar>a-c\<bar> + \<bar>b-d\<bar>" |
|
1072 proof - |
1114 proof - |
1073 have "\<bar>a + b - (c+d)\<bar> = \<bar>(a-c) + (b-d)\<bar>" by (simp add: diff_minus add_ac) |
1115 have "\<bar>a + b - (c+d)\<bar> = \<bar>(a-c) + (b-d)\<bar>" by (simp add: diff_minus add_ac) |
1074 also have "... \<le> \<bar>a-c\<bar> + \<bar>b-d\<bar>" by (rule abs_triangle_ineq) |
1116 also have "... \<le> \<bar>a-c\<bar> + \<bar>b-d\<bar>" by (rule abs_triangle_ineq) |
1075 finally show ?thesis . |
1117 finally show ?thesis . |
1076 qed |
1118 qed |
1077 |
1119 |
1078 lemma abs_add_abs[simp]: |
1120 lemma abs_add_abs[simp]: |
1079 fixes a:: "'a::{lordered_ab_group_abs}" |
1121 "\<bar>\<bar>a\<bar> + \<bar>b\<bar>\<bar> = \<bar>a\<bar> + \<bar>b\<bar>" (is "?L = ?R") |
1080 shows "abs(abs a + abs b) = abs a + abs b" (is "?L = ?R") |
1122 proof (rule antisym) |
1081 proof (rule order_antisym) |
|
1082 show "?L \<ge> ?R" by(rule abs_ge_self) |
1123 show "?L \<ge> ?R" by(rule abs_ge_self) |
1083 next |
1124 next |
1084 have "?L \<le> \<bar>\<bar>a\<bar>\<bar> + \<bar>\<bar>b\<bar>\<bar>" by(rule abs_triangle_ineq) |
1125 have "?L \<le> \<bar>\<bar>a\<bar>\<bar> + \<bar>\<bar>b\<bar>\<bar>" by(rule abs_triangle_ineq) |
1085 also have "\<dots> = ?R" by simp |
1126 also have "\<dots> = ?R" by simp |
1086 finally show "?L \<le> ?R" . |
1127 finally show "?L \<le> ?R" . |
1087 qed |
1128 qed |
1088 |
1129 |
|
1130 end |
|
1131 |
|
1132 lemma sup_eq_if: |
|
1133 fixes a :: "'a\<Colon>{lordered_ab_group, linorder}" |
|
1134 shows "sup a (- a) = (if a < 0 then - a else a)" |
|
1135 proof - |
|
1136 note add_le_cancel_right [of a a "- a", symmetric, simplified] |
|
1137 moreover note add_le_cancel_right [of "-a" a a, symmetric, simplified] |
|
1138 then show ?thesis by (auto simp: sup_max max_def) |
|
1139 qed |
|
1140 |
|
1141 lemma abs_if_lattice: |
|
1142 fixes a :: "'a\<Colon>{lordered_ab_group_abs, linorder}" |
|
1143 shows "\<bar>a\<bar> = (if a < 0 then - a else a)" |
|
1144 by auto |
|
1145 |
|
1146 |
1089 text {* Needed for abelian cancellation simprocs: *} |
1147 text {* Needed for abelian cancellation simprocs: *} |
1090 |
1148 |
1091 lemma add_cancel_21: "((x::'a::ab_group_add) + (y + z) = y + u) = (x + z = u)" |
1149 lemma add_cancel_21: "((x::'a::ab_group_add) + (y + z) = y + u) = (x + z = u)" |
1092 apply (subst add_left_commute) |
1150 apply (subst add_left_commute) |
1093 apply (subst add_left_cancel) |
1151 apply (subst add_left_cancel) |