763 with A have "- a \<le> 0" by auto |
782 with A have "- a \<le> 0" by auto |
764 with B show ?thesis by (auto intro: order_trans) |
783 with B show ?thesis by (auto intro: order_trans) |
765 qed |
784 qed |
766 qed |
785 qed |
767 |
786 |
768 lemma neg_equal_zero: |
787 lemma neg_equal_zero [simp]: |
769 "- a = a \<longleftrightarrow> a = 0" |
788 "- a = a \<longleftrightarrow> a = 0" |
770 unfolding equal_neg_zero [symmetric] by auto |
789 by (auto dest: sym) |
|
790 |
|
791 lemma double_zero [simp]: |
|
792 "a + a = 0 \<longleftrightarrow> a = 0" |
|
793 proof |
|
794 assume assm: "a + a = 0" |
|
795 then have a: "- a = a" by (rule minus_unique) |
|
796 then show "a = 0" by (simp add: neg_equal_zero) |
|
797 qed simp |
|
798 |
|
799 lemma double_zero_sym [simp]: |
|
800 "0 = a + a \<longleftrightarrow> a = 0" |
|
801 by (rule, drule sym) simp_all |
|
802 |
|
803 lemma zero_less_double_add_iff_zero_less_single_add [simp]: |
|
804 "0 < a + a \<longleftrightarrow> 0 < a" |
|
805 proof |
|
806 assume "0 < a + a" |
|
807 then have "0 - a < a" by (simp only: diff_less_eq) |
|
808 then have "- a < a" by simp |
|
809 then show "0 < a" by (simp add: neg_less_nonneg) |
|
810 next |
|
811 assume "0 < a" |
|
812 with this have "0 + 0 < a + a" |
|
813 by (rule add_strict_mono) |
|
814 then show "0 < a + a" by simp |
|
815 qed |
|
816 |
|
817 lemma zero_le_double_add_iff_zero_le_single_add [simp]: |
|
818 "0 \<le> a + a \<longleftrightarrow> 0 \<le> a" |
|
819 by (auto simp add: le_less) |
|
820 |
|
821 lemma double_add_less_zero_iff_single_add_less_zero [simp]: |
|
822 "a + a < 0 \<longleftrightarrow> a < 0" |
|
823 proof - |
|
824 have "\<not> a + a < 0 \<longleftrightarrow> \<not> a < 0" |
|
825 by (simp add: not_less) |
|
826 then show ?thesis by simp |
|
827 qed |
|
828 |
|
829 lemma double_add_le_zero_iff_single_add_le_zero [simp]: |
|
830 "a + a \<le> 0 \<longleftrightarrow> a \<le> 0" |
|
831 proof - |
|
832 have "\<not> a + a \<le> 0 \<longleftrightarrow> \<not> a \<le> 0" |
|
833 by (simp add: not_le) |
|
834 then show ?thesis by simp |
|
835 qed |
|
836 |
|
837 lemma le_minus_self_iff: |
|
838 "a \<le> - a \<longleftrightarrow> a \<le> 0" |
|
839 proof - |
|
840 from add_le_cancel_left [of "- a" "a + a" 0] |
|
841 have "a \<le> - a \<longleftrightarrow> a + a \<le> 0" |
|
842 by (simp add: add_assoc [symmetric]) |
|
843 thus ?thesis by simp |
|
844 qed |
|
845 |
|
846 lemma minus_le_self_iff: |
|
847 "- a \<le> a \<longleftrightarrow> 0 \<le> a" |
|
848 proof - |
|
849 from add_le_cancel_left [of "- a" 0 "a + a"] |
|
850 have "- a \<le> a \<longleftrightarrow> 0 \<le> a + a" |
|
851 by (simp add: add_assoc [symmetric]) |
|
852 thus ?thesis by simp |
|
853 qed |
|
854 |
|
855 lemma minus_max_eq_min: |
|
856 "- max x y = min (-x) (-y)" |
|
857 by (auto simp add: max_def min_def) |
|
858 |
|
859 lemma minus_min_eq_max: |
|
860 "- min x y = max (-x) (-y)" |
|
861 by (auto simp add: max_def min_def) |
771 |
862 |
772 end |
863 end |
773 |
864 |
774 -- {* FIXME localize the following *} |
865 -- {* FIXME localize the following *} |
775 |
866 |
939 finally show "?L \<le> ?R" . |
1030 finally show "?L \<le> ?R" . |
940 qed |
1031 qed |
941 |
1032 |
942 end |
1033 end |
943 |
1034 |
944 |
|
945 subsection {* Lattice Ordered (Abelian) Groups *} |
|
946 |
|
947 class semilattice_inf_ab_group_add = ordered_ab_group_add + semilattice_inf |
|
948 begin |
|
949 |
|
950 lemma add_inf_distrib_left: |
|
951 "a + inf b c = inf (a + b) (a + c)" |
|
952 apply (rule antisym) |
|
953 apply (simp_all add: le_infI) |
|
954 apply (rule add_le_imp_le_left [of "uminus a"]) |
|
955 apply (simp only: add_assoc [symmetric], simp) |
|
956 apply rule |
|
957 apply (rule add_le_imp_le_left[of "a"], simp only: add_assoc[symmetric], simp)+ |
|
958 done |
|
959 |
|
960 lemma add_inf_distrib_right: |
|
961 "inf a b + c = inf (a + c) (b + c)" |
|
962 proof - |
|
963 have "c + inf a b = inf (c+a) (c+b)" by (simp add: add_inf_distrib_left) |
|
964 thus ?thesis by (simp add: add_commute) |
|
965 qed |
|
966 |
|
967 end |
|
968 |
|
969 class semilattice_sup_ab_group_add = ordered_ab_group_add + semilattice_sup |
|
970 begin |
|
971 |
|
972 lemma add_sup_distrib_left: |
|
973 "a + sup b c = sup (a + b) (a + c)" |
|
974 apply (rule antisym) |
|
975 apply (rule add_le_imp_le_left [of "uminus a"]) |
|
976 apply (simp only: add_assoc[symmetric], simp) |
|
977 apply rule |
|
978 apply (rule add_le_imp_le_left [of "a"], simp only: add_assoc[symmetric], simp)+ |
|
979 apply (rule le_supI) |
|
980 apply (simp_all) |
|
981 done |
|
982 |
|
983 lemma add_sup_distrib_right: |
|
984 "sup a b + c = sup (a+c) (b+c)" |
|
985 proof - |
|
986 have "c + sup a b = sup (c+a) (c+b)" by (simp add: add_sup_distrib_left) |
|
987 thus ?thesis by (simp add: add_commute) |
|
988 qed |
|
989 |
|
990 end |
|
991 |
|
992 class lattice_ab_group_add = ordered_ab_group_add + lattice |
|
993 begin |
|
994 |
|
995 subclass semilattice_inf_ab_group_add .. |
|
996 subclass semilattice_sup_ab_group_add .. |
|
997 |
|
998 lemmas add_sup_inf_distribs = add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left |
|
999 |
|
1000 lemma inf_eq_neg_sup: "inf a b = - sup (-a) (-b)" |
|
1001 proof (rule inf_unique) |
|
1002 fix a b :: 'a |
|
1003 show "- sup (-a) (-b) \<le> a" |
|
1004 by (rule add_le_imp_le_right [of _ "sup (uminus a) (uminus b)"]) |
|
1005 (simp, simp add: add_sup_distrib_left) |
|
1006 next |
|
1007 fix a b :: 'a |
|
1008 show "- sup (-a) (-b) \<le> b" |
|
1009 by (rule add_le_imp_le_right [of _ "sup (uminus a) (uminus b)"]) |
|
1010 (simp, simp add: add_sup_distrib_left) |
|
1011 next |
|
1012 fix a b c :: 'a |
|
1013 assume "a \<le> b" "a \<le> c" |
|
1014 then show "a \<le> - sup (-b) (-c)" by (subst neg_le_iff_le [symmetric]) |
|
1015 (simp add: le_supI) |
|
1016 qed |
|
1017 |
|
1018 lemma sup_eq_neg_inf: "sup a b = - inf (-a) (-b)" |
|
1019 proof (rule sup_unique) |
|
1020 fix a b :: 'a |
|
1021 show "a \<le> - inf (-a) (-b)" |
|
1022 by (rule add_le_imp_le_right [of _ "inf (uminus a) (uminus b)"]) |
|
1023 (simp, simp add: add_inf_distrib_left) |
|
1024 next |
|
1025 fix a b :: 'a |
|
1026 show "b \<le> - inf (-a) (-b)" |
|
1027 by (rule add_le_imp_le_right [of _ "inf (uminus a) (uminus b)"]) |
|
1028 (simp, simp add: add_inf_distrib_left) |
|
1029 next |
|
1030 fix a b c :: 'a |
|
1031 assume "a \<le> c" "b \<le> c" |
|
1032 then show "- inf (-a) (-b) \<le> c" by (subst neg_le_iff_le [symmetric]) |
|
1033 (simp add: le_infI) |
|
1034 qed |
|
1035 |
|
1036 lemma neg_inf_eq_sup: "- inf a b = sup (-a) (-b)" |
|
1037 by (simp add: inf_eq_neg_sup) |
|
1038 |
|
1039 lemma neg_sup_eq_inf: "- sup a b = inf (-a) (-b)" |
|
1040 by (simp add: sup_eq_neg_inf) |
|
1041 |
|
1042 lemma add_eq_inf_sup: "a + b = sup a b + inf a b" |
|
1043 proof - |
|
1044 have "0 = - inf 0 (a-b) + inf (a-b) 0" by (simp add: inf_commute) |
|
1045 hence "0 = sup 0 (b-a) + inf (a-b) 0" by (simp add: inf_eq_neg_sup) |
|
1046 hence "0 = (-a + sup a b) + (inf a b + (-b))" |
|
1047 by (simp add: add_sup_distrib_left add_inf_distrib_right) |
|
1048 (simp add: algebra_simps) |
|
1049 thus ?thesis by (simp add: algebra_simps) |
|
1050 qed |
|
1051 |
|
1052 subsection {* Positive Part, Negative Part, Absolute Value *} |
|
1053 |
|
1054 definition |
|
1055 nprt :: "'a \<Rightarrow> 'a" where |
|
1056 "nprt x = inf x 0" |
|
1057 |
|
1058 definition |
|
1059 pprt :: "'a \<Rightarrow> 'a" where |
|
1060 "pprt x = sup x 0" |
|
1061 |
|
1062 lemma pprt_neg: "pprt (- x) = - nprt x" |
|
1063 proof - |
|
1064 have "sup (- x) 0 = sup (- x) (- 0)" unfolding minus_zero .. |
|
1065 also have "\<dots> = - inf x 0" unfolding neg_inf_eq_sup .. |
|
1066 finally have "sup (- x) 0 = - inf x 0" . |
|
1067 then show ?thesis unfolding pprt_def nprt_def . |
|
1068 qed |
|
1069 |
|
1070 lemma nprt_neg: "nprt (- x) = - pprt x" |
|
1071 proof - |
|
1072 from pprt_neg have "pprt (- (- x)) = - nprt (- x)" . |
|
1073 then have "pprt x = - nprt (- x)" by simp |
|
1074 then show ?thesis by simp |
|
1075 qed |
|
1076 |
|
1077 lemma prts: "a = pprt a + nprt a" |
|
1078 by (simp add: pprt_def nprt_def add_eq_inf_sup[symmetric]) |
|
1079 |
|
1080 lemma zero_le_pprt[simp]: "0 \<le> pprt a" |
|
1081 by (simp add: pprt_def) |
|
1082 |
|
1083 lemma nprt_le_zero[simp]: "nprt a \<le> 0" |
|
1084 by (simp add: nprt_def) |
|
1085 |
|
1086 lemma le_eq_neg: "a \<le> - b \<longleftrightarrow> a + b \<le> 0" (is "?l = ?r") |
|
1087 proof - |
|
1088 have a: "?l \<longrightarrow> ?r" |
|
1089 apply (auto) |
|
1090 apply (rule add_le_imp_le_right[of _ "uminus b" _]) |
|
1091 apply (simp add: add_assoc) |
|
1092 done |
|
1093 have b: "?r \<longrightarrow> ?l" |
|
1094 apply (auto) |
|
1095 apply (rule add_le_imp_le_right[of _ "b" _]) |
|
1096 apply (simp) |
|
1097 done |
|
1098 from a b show ?thesis by blast |
|
1099 qed |
|
1100 |
|
1101 lemma pprt_0[simp]: "pprt 0 = 0" by (simp add: pprt_def) |
|
1102 lemma nprt_0[simp]: "nprt 0 = 0" by (simp add: nprt_def) |
|
1103 |
|
1104 lemma pprt_eq_id [simp, noatp]: "0 \<le> x \<Longrightarrow> pprt x = x" |
|
1105 by (simp add: pprt_def sup_aci sup_absorb1) |
|
1106 |
|
1107 lemma nprt_eq_id [simp, noatp]: "x \<le> 0 \<Longrightarrow> nprt x = x" |
|
1108 by (simp add: nprt_def inf_aci inf_absorb1) |
|
1109 |
|
1110 lemma pprt_eq_0 [simp, noatp]: "x \<le> 0 \<Longrightarrow> pprt x = 0" |
|
1111 by (simp add: pprt_def sup_aci sup_absorb2) |
|
1112 |
|
1113 lemma nprt_eq_0 [simp, noatp]: "0 \<le> x \<Longrightarrow> nprt x = 0" |
|
1114 by (simp add: nprt_def inf_aci inf_absorb2) |
|
1115 |
|
1116 lemma sup_0_imp_0: "sup a (- a) = 0 \<Longrightarrow> a = 0" |
|
1117 proof - |
|
1118 { |
|
1119 fix a::'a |
|
1120 assume hyp: "sup a (-a) = 0" |
|
1121 hence "sup a (-a) + a = a" by (simp) |
|
1122 hence "sup (a+a) 0 = a" by (simp add: add_sup_distrib_right) |
|
1123 hence "sup (a+a) 0 <= a" by (simp) |
|
1124 hence "0 <= a" by (blast intro: order_trans inf_sup_ord) |
|
1125 } |
|
1126 note p = this |
|
1127 assume hyp:"sup a (-a) = 0" |
|
1128 hence hyp2:"sup (-a) (-(-a)) = 0" by (simp add: sup_commute) |
|
1129 from p[OF hyp] p[OF hyp2] show "a = 0" by simp |
|
1130 qed |
|
1131 |
|
1132 lemma inf_0_imp_0: "inf a (-a) = 0 \<Longrightarrow> a = 0" |
|
1133 apply (simp add: inf_eq_neg_sup) |
|
1134 apply (simp add: sup_commute) |
|
1135 apply (erule sup_0_imp_0) |
|
1136 done |
|
1137 |
|
1138 lemma inf_0_eq_0 [simp, noatp]: "inf a (- a) = 0 \<longleftrightarrow> a = 0" |
|
1139 by (rule, erule inf_0_imp_0) simp |
|
1140 |
|
1141 lemma sup_0_eq_0 [simp, noatp]: "sup a (- a) = 0 \<longleftrightarrow> a = 0" |
|
1142 by (rule, erule sup_0_imp_0) simp |
|
1143 |
|
1144 lemma zero_le_double_add_iff_zero_le_single_add [simp]: |
|
1145 "0 \<le> a + a \<longleftrightarrow> 0 \<le> a" |
|
1146 proof |
|
1147 assume "0 <= a + a" |
|
1148 hence a:"inf (a+a) 0 = 0" by (simp add: inf_commute inf_absorb1) |
|
1149 have "(inf a 0)+(inf a 0) = inf (inf (a+a) 0) a" (is "?l=_") |
|
1150 by (simp add: add_sup_inf_distribs inf_aci) |
|
1151 hence "?l = 0 + inf a 0" by (simp add: a, simp add: inf_commute) |
|
1152 hence "inf a 0 = 0" by (simp only: add_right_cancel) |
|
1153 then show "0 <= a" unfolding le_iff_inf by (simp add: inf_commute) |
|
1154 next |
|
1155 assume a: "0 <= a" |
|
1156 show "0 <= a + a" by (simp add: add_mono[OF a a, simplified]) |
|
1157 qed |
|
1158 |
|
1159 lemma double_zero: "a + a = 0 \<longleftrightarrow> a = 0" |
|
1160 proof |
|
1161 assume assm: "a + a = 0" |
|
1162 then have "a + a + - a = - a" by simp |
|
1163 then have "a + (a + - a) = - a" by (simp only: add_assoc) |
|
1164 then have a: "- a = a" by simp |
|
1165 show "a = 0" apply (rule antisym) |
|
1166 apply (unfold neg_le_iff_le [symmetric, of a]) |
|
1167 unfolding a apply simp |
|
1168 unfolding zero_le_double_add_iff_zero_le_single_add [symmetric, of a] |
|
1169 unfolding assm unfolding le_less apply simp_all done |
|
1170 next |
|
1171 assume "a = 0" then show "a + a = 0" by simp |
|
1172 qed |
|
1173 |
|
1174 lemma zero_less_double_add_iff_zero_less_single_add: |
|
1175 "0 < a + a \<longleftrightarrow> 0 < a" |
|
1176 proof (cases "a = 0") |
|
1177 case True then show ?thesis by auto |
|
1178 next |
|
1179 case False then show ?thesis (*FIXME tune proof*) |
|
1180 unfolding less_le apply simp apply rule |
|
1181 apply clarify |
|
1182 apply rule |
|
1183 apply assumption |
|
1184 apply (rule notI) |
|
1185 unfolding double_zero [symmetric, of a] apply simp |
|
1186 done |
|
1187 qed |
|
1188 |
|
1189 lemma double_add_le_zero_iff_single_add_le_zero [simp]: |
|
1190 "a + a \<le> 0 \<longleftrightarrow> a \<le> 0" |
|
1191 proof - |
|
1192 have "a + a \<le> 0 \<longleftrightarrow> 0 \<le> - (a + a)" by (subst le_minus_iff, simp) |
|
1193 moreover have "\<dots> \<longleftrightarrow> a \<le> 0" by (simp add: zero_le_double_add_iff_zero_le_single_add) |
|
1194 ultimately show ?thesis by blast |
|
1195 qed |
|
1196 |
|
1197 lemma double_add_less_zero_iff_single_less_zero [simp]: |
|
1198 "a + a < 0 \<longleftrightarrow> a < 0" |
|
1199 proof - |
|
1200 have "a + a < 0 \<longleftrightarrow> 0 < - (a + a)" by (subst less_minus_iff, simp) |
|
1201 moreover have "\<dots> \<longleftrightarrow> a < 0" by (simp add: zero_less_double_add_iff_zero_less_single_add) |
|
1202 ultimately show ?thesis by blast |
|
1203 qed |
|
1204 |
|
1205 declare neg_inf_eq_sup [simp] neg_sup_eq_inf [simp] |
|
1206 |
|
1207 lemma le_minus_self_iff: "a \<le> - a \<longleftrightarrow> a \<le> 0" |
|
1208 proof - |
|
1209 from add_le_cancel_left [of "uminus a" "plus a a" zero] |
|
1210 have "(a <= -a) = (a+a <= 0)" |
|
1211 by (simp add: add_assoc[symmetric]) |
|
1212 thus ?thesis by simp |
|
1213 qed |
|
1214 |
|
1215 lemma minus_le_self_iff: "- a \<le> a \<longleftrightarrow> 0 \<le> a" |
|
1216 proof - |
|
1217 from add_le_cancel_left [of "uminus a" zero "plus a a"] |
|
1218 have "(-a <= a) = (0 <= a+a)" |
|
1219 by (simp add: add_assoc[symmetric]) |
|
1220 thus ?thesis by simp |
|
1221 qed |
|
1222 |
|
1223 lemma zero_le_iff_zero_nprt: "0 \<le> a \<longleftrightarrow> nprt a = 0" |
|
1224 unfolding le_iff_inf by (simp add: nprt_def inf_commute) |
|
1225 |
|
1226 lemma le_zero_iff_zero_pprt: "a \<le> 0 \<longleftrightarrow> pprt a = 0" |
|
1227 unfolding le_iff_sup by (simp add: pprt_def sup_commute) |
|
1228 |
|
1229 lemma le_zero_iff_pprt_id: "0 \<le> a \<longleftrightarrow> pprt a = a" |
|
1230 unfolding le_iff_sup by (simp add: pprt_def sup_commute) |
|
1231 |
|
1232 lemma zero_le_iff_nprt_id: "a \<le> 0 \<longleftrightarrow> nprt a = a" |
|
1233 unfolding le_iff_inf by (simp add: nprt_def inf_commute) |
|
1234 |
|
1235 lemma pprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> pprt a \<le> pprt b" |
|
1236 unfolding le_iff_sup by (simp add: pprt_def sup_aci sup_assoc [symmetric, of a]) |
|
1237 |
|
1238 lemma nprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> nprt a \<le> nprt b" |
|
1239 unfolding le_iff_inf by (simp add: nprt_def inf_aci inf_assoc [symmetric, of a]) |
|
1240 |
|
1241 end |
|
1242 |
|
1243 lemmas add_sup_inf_distribs = add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left |
|
1244 |
|
1245 |
|
1246 class lattice_ab_group_add_abs = lattice_ab_group_add + abs + |
|
1247 assumes abs_lattice: "\<bar>a\<bar> = sup a (- a)" |
|
1248 begin |
|
1249 |
|
1250 lemma abs_prts: "\<bar>a\<bar> = pprt a - nprt a" |
|
1251 proof - |
|
1252 have "0 \<le> \<bar>a\<bar>" |
|
1253 proof - |
|
1254 have a: "a \<le> \<bar>a\<bar>" and b: "- a \<le> \<bar>a\<bar>" by (auto simp add: abs_lattice) |
|
1255 show ?thesis by (rule add_mono [OF a b, simplified]) |
|
1256 qed |
|
1257 then have "0 \<le> sup a (- a)" unfolding abs_lattice . |
|
1258 then have "sup (sup a (- a)) 0 = sup a (- a)" by (rule sup_absorb1) |
|
1259 then show ?thesis |
|
1260 by (simp add: add_sup_inf_distribs sup_aci |
|
1261 pprt_def nprt_def diff_minus abs_lattice) |
|
1262 qed |
|
1263 |
|
1264 subclass ordered_ab_group_add_abs |
|
1265 proof |
|
1266 have abs_ge_zero [simp]: "\<And>a. 0 \<le> \<bar>a\<bar>" |
|
1267 proof - |
|
1268 fix a b |
|
1269 have a: "a \<le> \<bar>a\<bar>" and b: "- a \<le> \<bar>a\<bar>" by (auto simp add: abs_lattice) |
|
1270 show "0 \<le> \<bar>a\<bar>" by (rule add_mono [OF a b, simplified]) |
|
1271 qed |
|
1272 have abs_leI: "\<And>a b. a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b" |
|
1273 by (simp add: abs_lattice le_supI) |
|
1274 fix a b |
|
1275 show "0 \<le> \<bar>a\<bar>" by simp |
|
1276 show "a \<le> \<bar>a\<bar>" |
|
1277 by (auto simp add: abs_lattice) |
|
1278 show "\<bar>-a\<bar> = \<bar>a\<bar>" |
|
1279 by (simp add: abs_lattice sup_commute) |
|
1280 show "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b" by (fact abs_leI) |
|
1281 show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>" |
|
1282 proof - |
|
1283 have g:"abs a + abs b = sup (a+b) (sup (-a-b) (sup (-a+b) (a + (-b))))" (is "_=sup ?m ?n") |
|
1284 by (simp add: abs_lattice add_sup_inf_distribs sup_aci diff_minus) |
|
1285 have a:"a+b <= sup ?m ?n" by (simp) |
|
1286 have b:"-a-b <= ?n" by (simp) |
|
1287 have c:"?n <= sup ?m ?n" by (simp) |
|
1288 from b c have d: "-a-b <= sup ?m ?n" by(rule order_trans) |
|
1289 have e:"-a-b = -(a+b)" by (simp add: diff_minus) |
|
1290 from a d e have "abs(a+b) <= sup ?m ?n" |
|
1291 by (drule_tac abs_leI, auto) |
|
1292 with g[symmetric] show ?thesis by simp |
|
1293 qed |
|
1294 qed |
|
1295 |
|
1296 end |
|
1297 |
|
1298 lemma sup_eq_if: |
|
1299 fixes a :: "'a\<Colon>{lattice_ab_group_add, linorder}" |
|
1300 shows "sup a (- a) = (if a < 0 then - a else a)" |
|
1301 proof - |
|
1302 note add_le_cancel_right [of a a "- a", symmetric, simplified] |
|
1303 moreover note add_le_cancel_right [of "-a" a a, symmetric, simplified] |
|
1304 then show ?thesis by (auto simp: sup_max min_max.sup_absorb1 min_max.sup_absorb2) |
|
1305 qed |
|
1306 |
|
1307 lemma abs_if_lattice: |
|
1308 fixes a :: "'a\<Colon>{lattice_ab_group_add_abs, linorder}" |
|
1309 shows "\<bar>a\<bar> = (if a < 0 then - a else a)" |
|
1310 by auto |
|
1311 |
|
1312 |
|
1313 text {* Needed for abelian cancellation simprocs: *} |
1035 text {* Needed for abelian cancellation simprocs: *} |
1314 |
1036 |
1315 lemma add_cancel_21: "((x::'a::ab_group_add) + (y + z) = y + u) = (x + z = u)" |
1037 lemma add_cancel_21: "((x::'a::ab_group_add) + (y + z) = y + u) = (x + z = u)" |
1316 apply (subst add_left_commute) |
1038 apply (subst add_left_commute) |
1317 apply (subst add_left_cancel) |
1039 apply (subst add_left_cancel) |