1073 |
1073 |
1074 lemma pprt_0[simp]: "pprt 0 = 0" by (simp add: pprt_def) |
1074 lemma pprt_0[simp]: "pprt 0 = 0" by (simp add: pprt_def) |
1075 lemma nprt_0[simp]: "nprt 0 = 0" by (simp add: nprt_def) |
1075 lemma nprt_0[simp]: "nprt 0 = 0" by (simp add: nprt_def) |
1076 |
1076 |
1077 lemma pprt_eq_id [simp, noatp]: "0 \<le> x \<Longrightarrow> pprt x = x" |
1077 lemma pprt_eq_id [simp, noatp]: "0 \<le> x \<Longrightarrow> pprt x = x" |
1078 by (simp add: pprt_def le_iff_sup sup_ACI) |
1078 by (simp add: pprt_def le_iff_sup sup_aci) |
1079 |
1079 |
1080 lemma nprt_eq_id [simp, noatp]: "x \<le> 0 \<Longrightarrow> nprt x = x" |
1080 lemma nprt_eq_id [simp, noatp]: "x \<le> 0 \<Longrightarrow> nprt x = x" |
1081 by (simp add: nprt_def le_iff_inf inf_ACI) |
1081 by (simp add: nprt_def le_iff_inf inf_aci) |
1082 |
1082 |
1083 lemma pprt_eq_0 [simp, noatp]: "x \<le> 0 \<Longrightarrow> pprt x = 0" |
1083 lemma pprt_eq_0 [simp, noatp]: "x \<le> 0 \<Longrightarrow> pprt x = 0" |
1084 by (simp add: pprt_def le_iff_sup sup_ACI) |
1084 by (simp add: pprt_def le_iff_sup sup_aci) |
1085 |
1085 |
1086 lemma nprt_eq_0 [simp, noatp]: "0 \<le> x \<Longrightarrow> nprt x = 0" |
1086 lemma nprt_eq_0 [simp, noatp]: "0 \<le> x \<Longrightarrow> nprt x = 0" |
1087 by (simp add: nprt_def le_iff_inf inf_ACI) |
1087 by (simp add: nprt_def le_iff_inf inf_aci) |
1088 |
1088 |
1089 lemma sup_0_imp_0: "sup a (- a) = 0 \<Longrightarrow> a = 0" |
1089 lemma sup_0_imp_0: "sup a (- a) = 0 \<Longrightarrow> a = 0" |
1090 proof - |
1090 proof - |
1091 { |
1091 { |
1092 fix a::'a |
1092 fix a::'a |
1118 "0 \<le> a + a \<longleftrightarrow> 0 \<le> a" |
1118 "0 \<le> a + a \<longleftrightarrow> 0 \<le> a" |
1119 proof |
1119 proof |
1120 assume "0 <= a + a" |
1120 assume "0 <= a + a" |
1121 hence a:"inf (a+a) 0 = 0" by (simp add: le_iff_inf inf_commute) |
1121 hence a:"inf (a+a) 0 = 0" by (simp add: le_iff_inf inf_commute) |
1122 have "(inf a 0)+(inf a 0) = inf (inf (a+a) 0) a" (is "?l=_") |
1122 have "(inf a 0)+(inf a 0) = inf (inf (a+a) 0) a" (is "?l=_") |
1123 by (simp add: add_sup_inf_distribs inf_ACI) |
1123 by (simp add: add_sup_inf_distribs inf_aci) |
1124 hence "?l = 0 + inf a 0" by (simp add: a, simp add: inf_commute) |
1124 hence "?l = 0 + inf a 0" by (simp add: a, simp add: inf_commute) |
1125 hence "inf a 0 = 0" by (simp only: add_right_cancel) |
1125 hence "inf a 0 = 0" by (simp only: add_right_cancel) |
1126 then show "0 <= a" by (simp add: le_iff_inf inf_commute) |
1126 then show "0 <= a" by (simp add: le_iff_inf inf_commute) |
1127 next |
1127 next |
1128 assume a: "0 <= a" |
1128 assume a: "0 <= a" |
1204 |
1204 |
1205 lemma zero_le_iff_nprt_id: "a \<le> 0 \<longleftrightarrow> nprt a = a" |
1205 lemma zero_le_iff_nprt_id: "a \<le> 0 \<longleftrightarrow> nprt a = a" |
1206 by (simp add: le_iff_inf nprt_def inf_commute) |
1206 by (simp add: le_iff_inf nprt_def inf_commute) |
1207 |
1207 |
1208 lemma pprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> pprt a \<le> pprt b" |
1208 lemma pprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> pprt a \<le> pprt b" |
1209 by (simp add: le_iff_sup pprt_def sup_ACI sup_assoc [symmetric, of a]) |
1209 by (simp add: le_iff_sup pprt_def sup_aci sup_assoc [symmetric, of a]) |
1210 |
1210 |
1211 lemma nprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> nprt a \<le> nprt b" |
1211 lemma nprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> nprt a \<le> nprt b" |
1212 by (simp add: le_iff_inf nprt_def inf_ACI inf_assoc [symmetric, of a]) |
1212 by (simp add: le_iff_inf nprt_def inf_aci inf_assoc [symmetric, of a]) |
1213 |
1213 |
1214 end |
1214 end |
1215 |
1215 |
1216 lemmas add_sup_inf_distribs = add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left |
1216 lemmas add_sup_inf_distribs = add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left |
1217 |
1217 |
1228 show ?thesis by (rule add_mono [OF a b, simplified]) |
1228 show ?thesis by (rule add_mono [OF a b, simplified]) |
1229 qed |
1229 qed |
1230 then have "0 \<le> sup a (- a)" unfolding abs_lattice . |
1230 then have "0 \<le> sup a (- a)" unfolding abs_lattice . |
1231 then have "sup (sup a (- a)) 0 = sup a (- a)" by (rule sup_absorb1) |
1231 then have "sup (sup a (- a)) 0 = sup a (- a)" by (rule sup_absorb1) |
1232 then show ?thesis |
1232 then show ?thesis |
1233 by (simp add: add_sup_inf_distribs sup_ACI |
1233 by (simp add: add_sup_inf_distribs sup_aci |
1234 pprt_def nprt_def diff_minus abs_lattice) |
1234 pprt_def nprt_def diff_minus abs_lattice) |
1235 qed |
1235 qed |
1236 |
1236 |
1237 subclass pordered_ab_group_add_abs |
1237 subclass pordered_ab_group_add_abs |
1238 proof |
1238 proof |
1252 by (simp add: abs_lattice sup_commute) |
1252 by (simp add: abs_lattice sup_commute) |
1253 show "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b" by (fact abs_leI) |
1253 show "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b" by (fact abs_leI) |
1254 show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>" |
1254 show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>" |
1255 proof - |
1255 proof - |
1256 have g:"abs a + abs b = sup (a+b) (sup (-a-b) (sup (-a+b) (a + (-b))))" (is "_=sup ?m ?n") |
1256 have g:"abs a + abs b = sup (a+b) (sup (-a-b) (sup (-a+b) (a + (-b))))" (is "_=sup ?m ?n") |
1257 by (simp add: abs_lattice add_sup_inf_distribs sup_ACI diff_minus) |
1257 by (simp add: abs_lattice add_sup_inf_distribs sup_aci diff_minus) |
1258 have a:"a+b <= sup ?m ?n" by (simp) |
1258 have a:"a+b <= sup ?m ?n" by (simp) |
1259 have b:"-a-b <= ?n" by (simp) |
1259 have b:"-a-b <= ?n" by (simp) |
1260 have c:"?n <= sup ?m ?n" by (simp) |
1260 have c:"?n <= sup ?m ?n" by (simp) |
1261 from b c have d: "-a-b <= sup ?m ?n" by(rule order_trans) |
1261 from b c have d: "-a-b <= sup ?m ?n" by(rule order_trans) |
1262 have e:"-a-b = -(a+b)" by (simp add: diff_minus) |
1262 have e:"-a-b = -(a+b)" by (simp add: diff_minus) |