1.1 --- a/src/HOL/OrderedGroup.thy Mon Feb 08 15:49:01 2010 -0800
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,1446 +0,0 @@
1.4 -(* Title: HOL/OrderedGroup.thy
1.5 - Author: Gertrud Bauer, Steven Obua, Lawrence C Paulson, Markus Wenzel, Jeremy Avigad
1.6 -*)
1.7 -
1.8 -header {* Ordered Groups *}
1.9 -
1.10 -theory OrderedGroup
1.11 -imports Lattices
1.12 -uses "~~/src/Provers/Arith/abel_cancel.ML"
1.13 -begin
1.14 -
1.15 -text {*
1.16 - The theory of partially ordered groups is taken from the books:
1.17 - \begin{itemize}
1.18 - \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979
1.19 - \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963
1.20 - \end{itemize}
1.21 - Most of the used notions can also be looked up in
1.22 - \begin{itemize}
1.23 - \item \url{http://www.mathworld.com} by Eric Weisstein et. al.
1.24 - \item \emph{Algebra I} by van der Waerden, Springer.
1.25 - \end{itemize}
1.26 -*}
1.27 -
1.28 -ML {*
1.29 -structure Algebra_Simps = Named_Thms(
1.30 - val name = "algebra_simps"
1.31 - val description = "algebra simplification rules"
1.32 -)
1.33 -*}
1.34 -
1.35 -setup Algebra_Simps.setup
1.36 -
1.37 -text{* The rewrites accumulated in @{text algebra_simps} deal with the
1.38 -classical algebraic structures of groups, rings and family. They simplify
1.39 -terms by multiplying everything out (in case of a ring) and bringing sums and
1.40 -products into a canonical form (by ordered rewriting). As a result it decides
1.41 -group and ring equalities but also helps with inequalities.
1.42 -
1.43 -Of course it also works for fields, but it knows nothing about multiplicative
1.44 -inverses or division. This is catered for by @{text field_simps}. *}
1.45 -
1.46 -subsection {* Semigroups and Monoids *}
1.47 -
1.48 -class semigroup_add = plus +
1.49 - assumes add_assoc [algebra_simps]: "(a + b) + c = a + (b + c)"
1.50 -
1.51 -sublocale semigroup_add < plus!: semigroup plus proof
1.52 -qed (fact add_assoc)
1.53 -
1.54 -class ab_semigroup_add = semigroup_add +
1.55 - assumes add_commute [algebra_simps]: "a + b = b + a"
1.56 -
1.57 -sublocale ab_semigroup_add < plus!: abel_semigroup plus proof
1.58 -qed (fact add_commute)
1.59 -
1.60 -context ab_semigroup_add
1.61 -begin
1.62 -
1.63 -lemmas add_left_commute [algebra_simps] = plus.left_commute
1.64 -
1.65 -theorems add_ac = add_assoc add_commute add_left_commute
1.66 -
1.67 -end
1.68 -
1.69 -theorems add_ac = add_assoc add_commute add_left_commute
1.70 -
1.71 -class semigroup_mult = times +
1.72 - assumes mult_assoc [algebra_simps]: "(a * b) * c = a * (b * c)"
1.73 -
1.74 -sublocale semigroup_mult < times!: semigroup times proof
1.75 -qed (fact mult_assoc)
1.76 -
1.77 -class ab_semigroup_mult = semigroup_mult +
1.78 - assumes mult_commute [algebra_simps]: "a * b = b * a"
1.79 -
1.80 -sublocale ab_semigroup_mult < times!: abel_semigroup times proof
1.81 -qed (fact mult_commute)
1.82 -
1.83 -context ab_semigroup_mult
1.84 -begin
1.85 -
1.86 -lemmas mult_left_commute [algebra_simps] = times.left_commute
1.87 -
1.88 -theorems mult_ac = mult_assoc mult_commute mult_left_commute
1.89 -
1.90 -end
1.91 -
1.92 -theorems mult_ac = mult_assoc mult_commute mult_left_commute
1.93 -
1.94 -class ab_semigroup_idem_mult = ab_semigroup_mult +
1.95 - assumes mult_idem: "x * x = x"
1.96 -
1.97 -sublocale ab_semigroup_idem_mult < times!: semilattice times proof
1.98 -qed (fact mult_idem)
1.99 -
1.100 -context ab_semigroup_idem_mult
1.101 -begin
1.102 -
1.103 -lemmas mult_left_idem = times.left_idem
1.104 -
1.105 -end
1.106 -
1.107 -class monoid_add = zero + semigroup_add +
1.108 - assumes add_0_left [simp]: "0 + a = a"
1.109 - and add_0_right [simp]: "a + 0 = a"
1.110 -
1.111 -lemma zero_reorient: "0 = x \<longleftrightarrow> x = 0"
1.112 -by (rule eq_commute)
1.113 -
1.114 -class comm_monoid_add = zero + ab_semigroup_add +
1.115 - assumes add_0: "0 + a = a"
1.116 -begin
1.117 -
1.118 -subclass monoid_add
1.119 - proof qed (insert add_0, simp_all add: add_commute)
1.120 -
1.121 -end
1.122 -
1.123 -class monoid_mult = one + semigroup_mult +
1.124 - assumes mult_1_left [simp]: "1 * a = a"
1.125 - assumes mult_1_right [simp]: "a * 1 = a"
1.126 -
1.127 -lemma one_reorient: "1 = x \<longleftrightarrow> x = 1"
1.128 -by (rule eq_commute)
1.129 -
1.130 -class comm_monoid_mult = one + ab_semigroup_mult +
1.131 - assumes mult_1: "1 * a = a"
1.132 -begin
1.133 -
1.134 -subclass monoid_mult
1.135 - proof qed (insert mult_1, simp_all add: mult_commute)
1.136 -
1.137 -end
1.138 -
1.139 -class cancel_semigroup_add = semigroup_add +
1.140 - assumes add_left_imp_eq: "a + b = a + c \<Longrightarrow> b = c"
1.141 - assumes add_right_imp_eq: "b + a = c + a \<Longrightarrow> b = c"
1.142 -begin
1.143 -
1.144 -lemma add_left_cancel [simp]:
1.145 - "a + b = a + c \<longleftrightarrow> b = c"
1.146 -by (blast dest: add_left_imp_eq)
1.147 -
1.148 -lemma add_right_cancel [simp]:
1.149 - "b + a = c + a \<longleftrightarrow> b = c"
1.150 -by (blast dest: add_right_imp_eq)
1.151 -
1.152 -end
1.153 -
1.154 -class cancel_ab_semigroup_add = ab_semigroup_add +
1.155 - assumes add_imp_eq: "a + b = a + c \<Longrightarrow> b = c"
1.156 -begin
1.157 -
1.158 -subclass cancel_semigroup_add
1.159 -proof
1.160 - fix a b c :: 'a
1.161 - assume "a + b = a + c"
1.162 - then show "b = c" by (rule add_imp_eq)
1.163 -next
1.164 - fix a b c :: 'a
1.165 - assume "b + a = c + a"
1.166 - then have "a + b = a + c" by (simp only: add_commute)
1.167 - then show "b = c" by (rule add_imp_eq)
1.168 -qed
1.169 -
1.170 -end
1.171 -
1.172 -class cancel_comm_monoid_add = cancel_ab_semigroup_add + comm_monoid_add
1.173 -
1.174 -
1.175 -subsection {* Groups *}
1.176 -
1.177 -class group_add = minus + uminus + monoid_add +
1.178 - assumes left_minus [simp]: "- a + a = 0"
1.179 - assumes diff_minus: "a - b = a + (- b)"
1.180 -begin
1.181 -
1.182 -lemma minus_unique:
1.183 - assumes "a + b = 0" shows "- a = b"
1.184 -proof -
1.185 - have "- a = - a + (a + b)" using assms by simp
1.186 - also have "\<dots> = b" by (simp add: add_assoc [symmetric])
1.187 - finally show ?thesis .
1.188 -qed
1.189 -
1.190 -lemmas equals_zero_I = minus_unique (* legacy name *)
1.191 -
1.192 -lemma minus_zero [simp]: "- 0 = 0"
1.193 -proof -
1.194 - have "0 + 0 = 0" by (rule add_0_right)
1.195 - thus "- 0 = 0" by (rule minus_unique)
1.196 -qed
1.197 -
1.198 -lemma minus_minus [simp]: "- (- a) = a"
1.199 -proof -
1.200 - have "- a + a = 0" by (rule left_minus)
1.201 - thus "- (- a) = a" by (rule minus_unique)
1.202 -qed
1.203 -
1.204 -lemma right_minus [simp]: "a + - a = 0"
1.205 -proof -
1.206 - have "a + - a = - (- a) + - a" by simp
1.207 - also have "\<dots> = 0" by (rule left_minus)
1.208 - finally show ?thesis .
1.209 -qed
1.210 -
1.211 -lemma minus_add_cancel: "- a + (a + b) = b"
1.212 -by (simp add: add_assoc [symmetric])
1.213 -
1.214 -lemma add_minus_cancel: "a + (- a + b) = b"
1.215 -by (simp add: add_assoc [symmetric])
1.216 -
1.217 -lemma minus_add: "- (a + b) = - b + - a"
1.218 -proof -
1.219 - have "(a + b) + (- b + - a) = 0"
1.220 - by (simp add: add_assoc add_minus_cancel)
1.221 - thus "- (a + b) = - b + - a"
1.222 - by (rule minus_unique)
1.223 -qed
1.224 -
1.225 -lemma right_minus_eq: "a - b = 0 \<longleftrightarrow> a = b"
1.226 -proof
1.227 - assume "a - b = 0"
1.228 - have "a = (a - b) + b" by (simp add:diff_minus add_assoc)
1.229 - also have "\<dots> = b" using `a - b = 0` by simp
1.230 - finally show "a = b" .
1.231 -next
1.232 - assume "a = b" thus "a - b = 0" by (simp add: diff_minus)
1.233 -qed
1.234 -
1.235 -lemma diff_self [simp]: "a - a = 0"
1.236 -by (simp add: diff_minus)
1.237 -
1.238 -lemma diff_0 [simp]: "0 - a = - a"
1.239 -by (simp add: diff_minus)
1.240 -
1.241 -lemma diff_0_right [simp]: "a - 0 = a"
1.242 -by (simp add: diff_minus)
1.243 -
1.244 -lemma diff_minus_eq_add [simp]: "a - - b = a + b"
1.245 -by (simp add: diff_minus)
1.246 -
1.247 -lemma neg_equal_iff_equal [simp]:
1.248 - "- a = - b \<longleftrightarrow> a = b"
1.249 -proof
1.250 - assume "- a = - b"
1.251 - hence "- (- a) = - (- b)" by simp
1.252 - thus "a = b" by simp
1.253 -next
1.254 - assume "a = b"
1.255 - thus "- a = - b" by simp
1.256 -qed
1.257 -
1.258 -lemma neg_equal_0_iff_equal [simp]:
1.259 - "- a = 0 \<longleftrightarrow> a = 0"
1.260 -by (subst neg_equal_iff_equal [symmetric], simp)
1.261 -
1.262 -lemma neg_0_equal_iff_equal [simp]:
1.263 - "0 = - a \<longleftrightarrow> 0 = a"
1.264 -by (subst neg_equal_iff_equal [symmetric], simp)
1.265 -
1.266 -text{*The next two equations can make the simplifier loop!*}
1.267 -
1.268 -lemma equation_minus_iff:
1.269 - "a = - b \<longleftrightarrow> b = - a"
1.270 -proof -
1.271 - have "- (- a) = - b \<longleftrightarrow> - a = b" by (rule neg_equal_iff_equal)
1.272 - thus ?thesis by (simp add: eq_commute)
1.273 -qed
1.274 -
1.275 -lemma minus_equation_iff:
1.276 - "- a = b \<longleftrightarrow> - b = a"
1.277 -proof -
1.278 - have "- a = - (- b) \<longleftrightarrow> a = -b" by (rule neg_equal_iff_equal)
1.279 - thus ?thesis by (simp add: eq_commute)
1.280 -qed
1.281 -
1.282 -lemma diff_add_cancel: "a - b + b = a"
1.283 -by (simp add: diff_minus add_assoc)
1.284 -
1.285 -lemma add_diff_cancel: "a + b - b = a"
1.286 -by (simp add: diff_minus add_assoc)
1.287 -
1.288 -declare diff_minus[symmetric, algebra_simps]
1.289 -
1.290 -lemma eq_neg_iff_add_eq_0: "a = - b \<longleftrightarrow> a + b = 0"
1.291 -proof
1.292 - assume "a = - b" then show "a + b = 0" by simp
1.293 -next
1.294 - assume "a + b = 0"
1.295 - moreover have "a + (b + - b) = (a + b) + - b"
1.296 - by (simp only: add_assoc)
1.297 - ultimately show "a = - b" by simp
1.298 -qed
1.299 -
1.300 -end
1.301 -
1.302 -class ab_group_add = minus + uminus + comm_monoid_add +
1.303 - assumes ab_left_minus: "- a + a = 0"
1.304 - assumes ab_diff_minus: "a - b = a + (- b)"
1.305 -begin
1.306 -
1.307 -subclass group_add
1.308 - proof qed (simp_all add: ab_left_minus ab_diff_minus)
1.309 -
1.310 -subclass cancel_comm_monoid_add
1.311 -proof
1.312 - fix a b c :: 'a
1.313 - assume "a + b = a + c"
1.314 - then have "- a + a + b = - a + a + c"
1.315 - unfolding add_assoc by simp
1.316 - then show "b = c" by simp
1.317 -qed
1.318 -
1.319 -lemma uminus_add_conv_diff[algebra_simps]:
1.320 - "- a + b = b - a"
1.321 -by (simp add:diff_minus add_commute)
1.322 -
1.323 -lemma minus_add_distrib [simp]:
1.324 - "- (a + b) = - a + - b"
1.325 -by (rule minus_unique) (simp add: add_ac)
1.326 -
1.327 -lemma minus_diff_eq [simp]:
1.328 - "- (a - b) = b - a"
1.329 -by (simp add: diff_minus add_commute)
1.330 -
1.331 -lemma add_diff_eq[algebra_simps]: "a + (b - c) = (a + b) - c"
1.332 -by (simp add: diff_minus add_ac)
1.333 -
1.334 -lemma diff_add_eq[algebra_simps]: "(a - b) + c = (a + c) - b"
1.335 -by (simp add: diff_minus add_ac)
1.336 -
1.337 -lemma diff_eq_eq[algebra_simps]: "a - b = c \<longleftrightarrow> a = c + b"
1.338 -by (auto simp add: diff_minus add_assoc)
1.339 -
1.340 -lemma eq_diff_eq[algebra_simps]: "a = c - b \<longleftrightarrow> a + b = c"
1.341 -by (auto simp add: diff_minus add_assoc)
1.342 -
1.343 -lemma diff_diff_eq[algebra_simps]: "(a - b) - c = a - (b + c)"
1.344 -by (simp add: diff_minus add_ac)
1.345 -
1.346 -lemma diff_diff_eq2[algebra_simps]: "a - (b - c) = (a + c) - b"
1.347 -by (simp add: diff_minus add_ac)
1.348 -
1.349 -lemma eq_iff_diff_eq_0: "a = b \<longleftrightarrow> a - b = 0"
1.350 -by (simp add: algebra_simps)
1.351 -
1.352 -lemma diff_eq_0_iff_eq [simp, noatp]: "a - b = 0 \<longleftrightarrow> a = b"
1.353 -by (simp add: algebra_simps)
1.354 -
1.355 -end
1.356 -
1.357 -subsection {* (Partially) Ordered Groups *}
1.358 -
1.359 -class pordered_ab_semigroup_add = order + ab_semigroup_add +
1.360 - assumes add_left_mono: "a \<le> b \<Longrightarrow> c + a \<le> c + b"
1.361 -begin
1.362 -
1.363 -lemma add_right_mono:
1.364 - "a \<le> b \<Longrightarrow> a + c \<le> b + c"
1.365 -by (simp add: add_commute [of _ c] add_left_mono)
1.366 -
1.367 -text {* non-strict, in both arguments *}
1.368 -lemma add_mono:
1.369 - "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c \<le> b + d"
1.370 - apply (erule add_right_mono [THEN order_trans])
1.371 - apply (simp add: add_commute add_left_mono)
1.372 - done
1.373 -
1.374 -end
1.375 -
1.376 -class pordered_cancel_ab_semigroup_add =
1.377 - pordered_ab_semigroup_add + cancel_ab_semigroup_add
1.378 -begin
1.379 -
1.380 -lemma add_strict_left_mono:
1.381 - "a < b \<Longrightarrow> c + a < c + b"
1.382 -by (auto simp add: less_le add_left_mono)
1.383 -
1.384 -lemma add_strict_right_mono:
1.385 - "a < b \<Longrightarrow> a + c < b + c"
1.386 -by (simp add: add_commute [of _ c] add_strict_left_mono)
1.387 -
1.388 -text{*Strict monotonicity in both arguments*}
1.389 -lemma add_strict_mono:
1.390 - "a < b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
1.391 -apply (erule add_strict_right_mono [THEN less_trans])
1.392 -apply (erule add_strict_left_mono)
1.393 -done
1.394 -
1.395 -lemma add_less_le_mono:
1.396 - "a < b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c < b + d"
1.397 -apply (erule add_strict_right_mono [THEN less_le_trans])
1.398 -apply (erule add_left_mono)
1.399 -done
1.400 -
1.401 -lemma add_le_less_mono:
1.402 - "a \<le> b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
1.403 -apply (erule add_right_mono [THEN le_less_trans])
1.404 -apply (erule add_strict_left_mono)
1.405 -done
1.406 -
1.407 -end
1.408 -
1.409 -class pordered_ab_semigroup_add_imp_le =
1.410 - pordered_cancel_ab_semigroup_add +
1.411 - assumes add_le_imp_le_left: "c + a \<le> c + b \<Longrightarrow> a \<le> b"
1.412 -begin
1.413 -
1.414 -lemma add_less_imp_less_left:
1.415 - assumes less: "c + a < c + b" shows "a < b"
1.416 -proof -
1.417 - from less have le: "c + a <= c + b" by (simp add: order_le_less)
1.418 - have "a <= b"
1.419 - apply (insert le)
1.420 - apply (drule add_le_imp_le_left)
1.421 - by (insert le, drule add_le_imp_le_left, assumption)
1.422 - moreover have "a \<noteq> b"
1.423 - proof (rule ccontr)
1.424 - assume "~(a \<noteq> b)"
1.425 - then have "a = b" by simp
1.426 - then have "c + a = c + b" by simp
1.427 - with less show "False"by simp
1.428 - qed
1.429 - ultimately show "a < b" by (simp add: order_le_less)
1.430 -qed
1.431 -
1.432 -lemma add_less_imp_less_right:
1.433 - "a + c < b + c \<Longrightarrow> a < b"
1.434 -apply (rule add_less_imp_less_left [of c])
1.435 -apply (simp add: add_commute)
1.436 -done
1.437 -
1.438 -lemma add_less_cancel_left [simp]:
1.439 - "c + a < c + b \<longleftrightarrow> a < b"
1.440 -by (blast intro: add_less_imp_less_left add_strict_left_mono)
1.441 -
1.442 -lemma add_less_cancel_right [simp]:
1.443 - "a + c < b + c \<longleftrightarrow> a < b"
1.444 -by (blast intro: add_less_imp_less_right add_strict_right_mono)
1.445 -
1.446 -lemma add_le_cancel_left [simp]:
1.447 - "c + a \<le> c + b \<longleftrightarrow> a \<le> b"
1.448 -by (auto, drule add_le_imp_le_left, simp_all add: add_left_mono)
1.449 -
1.450 -lemma add_le_cancel_right [simp]:
1.451 - "a + c \<le> b + c \<longleftrightarrow> a \<le> b"
1.452 -by (simp add: add_commute [of a c] add_commute [of b c])
1.453 -
1.454 -lemma add_le_imp_le_right:
1.455 - "a + c \<le> b + c \<Longrightarrow> a \<le> b"
1.456 -by simp
1.457 -
1.458 -lemma max_add_distrib_left:
1.459 - "max x y + z = max (x + z) (y + z)"
1.460 - unfolding max_def by auto
1.461 -
1.462 -lemma min_add_distrib_left:
1.463 - "min x y + z = min (x + z) (y + z)"
1.464 - unfolding min_def by auto
1.465 -
1.466 -end
1.467 -
1.468 -subsection {* Support for reasoning about signs *}
1.469 -
1.470 -class pordered_comm_monoid_add =
1.471 - pordered_cancel_ab_semigroup_add + comm_monoid_add
1.472 -begin
1.473 -
1.474 -lemma add_pos_nonneg:
1.475 - assumes "0 < a" and "0 \<le> b" shows "0 < a + b"
1.476 -proof -
1.477 - have "0 + 0 < a + b"
1.478 - using assms by (rule add_less_le_mono)
1.479 - then show ?thesis by simp
1.480 -qed
1.481 -
1.482 -lemma add_pos_pos:
1.483 - assumes "0 < a" and "0 < b" shows "0 < a + b"
1.484 -by (rule add_pos_nonneg) (insert assms, auto)
1.485 -
1.486 -lemma add_nonneg_pos:
1.487 - assumes "0 \<le> a" and "0 < b" shows "0 < a + b"
1.488 -proof -
1.489 - have "0 + 0 < a + b"
1.490 - using assms by (rule add_le_less_mono)
1.491 - then show ?thesis by simp
1.492 -qed
1.493 -
1.494 -lemma add_nonneg_nonneg:
1.495 - assumes "0 \<le> a" and "0 \<le> b" shows "0 \<le> a + b"
1.496 -proof -
1.497 - have "0 + 0 \<le> a + b"
1.498 - using assms by (rule add_mono)
1.499 - then show ?thesis by simp
1.500 -qed
1.501 -
1.502 -lemma add_neg_nonpos:
1.503 - assumes "a < 0" and "b \<le> 0" shows "a + b < 0"
1.504 -proof -
1.505 - have "a + b < 0 + 0"
1.506 - using assms by (rule add_less_le_mono)
1.507 - then show ?thesis by simp
1.508 -qed
1.509 -
1.510 -lemma add_neg_neg:
1.511 - assumes "a < 0" and "b < 0" shows "a + b < 0"
1.512 -by (rule add_neg_nonpos) (insert assms, auto)
1.513 -
1.514 -lemma add_nonpos_neg:
1.515 - assumes "a \<le> 0" and "b < 0" shows "a + b < 0"
1.516 -proof -
1.517 - have "a + b < 0 + 0"
1.518 - using assms by (rule add_le_less_mono)
1.519 - then show ?thesis by simp
1.520 -qed
1.521 -
1.522 -lemma add_nonpos_nonpos:
1.523 - assumes "a \<le> 0" and "b \<le> 0" shows "a + b \<le> 0"
1.524 -proof -
1.525 - have "a + b \<le> 0 + 0"
1.526 - using assms by (rule add_mono)
1.527 - then show ?thesis by simp
1.528 -qed
1.529 -
1.530 -lemmas add_sign_intros =
1.531 - add_pos_nonneg add_pos_pos add_nonneg_pos add_nonneg_nonneg
1.532 - add_neg_nonpos add_neg_neg add_nonpos_neg add_nonpos_nonpos
1.533 -
1.534 -lemma add_nonneg_eq_0_iff:
1.535 - assumes x: "0 \<le> x" and y: "0 \<le> y"
1.536 - shows "x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
1.537 -proof (intro iffI conjI)
1.538 - have "x = x + 0" by simp
1.539 - also have "x + 0 \<le> x + y" using y by (rule add_left_mono)
1.540 - also assume "x + y = 0"
1.541 - also have "0 \<le> x" using x .
1.542 - finally show "x = 0" .
1.543 -next
1.544 - have "y = 0 + y" by simp
1.545 - also have "0 + y \<le> x + y" using x by (rule add_right_mono)
1.546 - also assume "x + y = 0"
1.547 - also have "0 \<le> y" using y .
1.548 - finally show "y = 0" .
1.549 -next
1.550 - assume "x = 0 \<and> y = 0"
1.551 - then show "x + y = 0" by simp
1.552 -qed
1.553 -
1.554 -end
1.555 -
1.556 -class pordered_ab_group_add =
1.557 - ab_group_add + pordered_ab_semigroup_add
1.558 -begin
1.559 -
1.560 -subclass pordered_cancel_ab_semigroup_add ..
1.561 -
1.562 -subclass pordered_ab_semigroup_add_imp_le
1.563 -proof
1.564 - fix a b c :: 'a
1.565 - assume "c + a \<le> c + b"
1.566 - hence "(-c) + (c + a) \<le> (-c) + (c + b)" by (rule add_left_mono)
1.567 - hence "((-c) + c) + a \<le> ((-c) + c) + b" by (simp only: add_assoc)
1.568 - thus "a \<le> b" by simp
1.569 -qed
1.570 -
1.571 -subclass pordered_comm_monoid_add ..
1.572 -
1.573 -lemma max_diff_distrib_left:
1.574 - shows "max x y - z = max (x - z) (y - z)"
1.575 -by (simp add: diff_minus, rule max_add_distrib_left)
1.576 -
1.577 -lemma min_diff_distrib_left:
1.578 - shows "min x y - z = min (x - z) (y - z)"
1.579 -by (simp add: diff_minus, rule min_add_distrib_left)
1.580 -
1.581 -lemma le_imp_neg_le:
1.582 - assumes "a \<le> b" shows "-b \<le> -a"
1.583 -proof -
1.584 - have "-a+a \<le> -a+b" using `a \<le> b` by (rule add_left_mono)
1.585 - hence "0 \<le> -a+b" by simp
1.586 - hence "0 + (-b) \<le> (-a + b) + (-b)" by (rule add_right_mono)
1.587 - thus ?thesis by (simp add: add_assoc)
1.588 -qed
1.589 -
1.590 -lemma neg_le_iff_le [simp]: "- b \<le> - a \<longleftrightarrow> a \<le> b"
1.591 -proof
1.592 - assume "- b \<le> - a"
1.593 - hence "- (- a) \<le> - (- b)" by (rule le_imp_neg_le)
1.594 - thus "a\<le>b" by simp
1.595 -next
1.596 - assume "a\<le>b"
1.597 - thus "-b \<le> -a" by (rule le_imp_neg_le)
1.598 -qed
1.599 -
1.600 -lemma neg_le_0_iff_le [simp]: "- a \<le> 0 \<longleftrightarrow> 0 \<le> a"
1.601 -by (subst neg_le_iff_le [symmetric], simp)
1.602 -
1.603 -lemma neg_0_le_iff_le [simp]: "0 \<le> - a \<longleftrightarrow> a \<le> 0"
1.604 -by (subst neg_le_iff_le [symmetric], simp)
1.605 -
1.606 -lemma neg_less_iff_less [simp]: "- b < - a \<longleftrightarrow> a < b"
1.607 -by (force simp add: less_le)
1.608 -
1.609 -lemma neg_less_0_iff_less [simp]: "- a < 0 \<longleftrightarrow> 0 < a"
1.610 -by (subst neg_less_iff_less [symmetric], simp)
1.611 -
1.612 -lemma neg_0_less_iff_less [simp]: "0 < - a \<longleftrightarrow> a < 0"
1.613 -by (subst neg_less_iff_less [symmetric], simp)
1.614 -
1.615 -text{*The next several equations can make the simplifier loop!*}
1.616 -
1.617 -lemma less_minus_iff: "a < - b \<longleftrightarrow> b < - a"
1.618 -proof -
1.619 - have "(- (-a) < - b) = (b < - a)" by (rule neg_less_iff_less)
1.620 - thus ?thesis by simp
1.621 -qed
1.622 -
1.623 -lemma minus_less_iff: "- a < b \<longleftrightarrow> - b < a"
1.624 -proof -
1.625 - have "(- a < - (-b)) = (- b < a)" by (rule neg_less_iff_less)
1.626 - thus ?thesis by simp
1.627 -qed
1.628 -
1.629 -lemma le_minus_iff: "a \<le> - b \<longleftrightarrow> b \<le> - a"
1.630 -proof -
1.631 - have mm: "!! a (b::'a). (-(-a)) < -b \<Longrightarrow> -(-b) < -a" by (simp only: minus_less_iff)
1.632 - have "(- (- a) <= -b) = (b <= - a)"
1.633 - apply (auto simp only: le_less)
1.634 - apply (drule mm)
1.635 - apply (simp_all)
1.636 - apply (drule mm[simplified], assumption)
1.637 - done
1.638 - then show ?thesis by simp
1.639 -qed
1.640 -
1.641 -lemma minus_le_iff: "- a \<le> b \<longleftrightarrow> - b \<le> a"
1.642 -by (auto simp add: le_less minus_less_iff)
1.643 -
1.644 -lemma less_iff_diff_less_0: "a < b \<longleftrightarrow> a - b < 0"
1.645 -proof -
1.646 - have "(a < b) = (a + (- b) < b + (-b))"
1.647 - by (simp only: add_less_cancel_right)
1.648 - also have "... = (a - b < 0)" by (simp add: diff_minus)
1.649 - finally show ?thesis .
1.650 -qed
1.651 -
1.652 -lemma diff_less_eq[algebra_simps]: "a - b < c \<longleftrightarrow> a < c + b"
1.653 -apply (subst less_iff_diff_less_0 [of a])
1.654 -apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst])
1.655 -apply (simp add: diff_minus add_ac)
1.656 -done
1.657 -
1.658 -lemma less_diff_eq[algebra_simps]: "a < c - b \<longleftrightarrow> a + b < c"
1.659 -apply (subst less_iff_diff_less_0 [of "plus a b"])
1.660 -apply (subst less_iff_diff_less_0 [of a])
1.661 -apply (simp add: diff_minus add_ac)
1.662 -done
1.663 -
1.664 -lemma diff_le_eq[algebra_simps]: "a - b \<le> c \<longleftrightarrow> a \<le> c + b"
1.665 -by (auto simp add: le_less diff_less_eq diff_add_cancel add_diff_cancel)
1.666 -
1.667 -lemma le_diff_eq[algebra_simps]: "a \<le> c - b \<longleftrightarrow> a + b \<le> c"
1.668 -by (auto simp add: le_less less_diff_eq diff_add_cancel add_diff_cancel)
1.669 -
1.670 -lemma le_iff_diff_le_0: "a \<le> b \<longleftrightarrow> a - b \<le> 0"
1.671 -by (simp add: algebra_simps)
1.672 -
1.673 -text{*Legacy - use @{text algebra_simps} *}
1.674 -lemmas group_simps[noatp] = algebra_simps
1.675 -
1.676 -end
1.677 -
1.678 -text{*Legacy - use @{text algebra_simps} *}
1.679 -lemmas group_simps[noatp] = algebra_simps
1.680 -
1.681 -class ordered_ab_semigroup_add =
1.682 - linorder + pordered_ab_semigroup_add
1.683 -
1.684 -class ordered_cancel_ab_semigroup_add =
1.685 - linorder + pordered_cancel_ab_semigroup_add
1.686 -begin
1.687 -
1.688 -subclass ordered_ab_semigroup_add ..
1.689 -
1.690 -subclass pordered_ab_semigroup_add_imp_le
1.691 -proof
1.692 - fix a b c :: 'a
1.693 - assume le: "c + a <= c + b"
1.694 - show "a <= b"
1.695 - proof (rule ccontr)
1.696 - assume w: "~ a \<le> b"
1.697 - hence "b <= a" by (simp add: linorder_not_le)
1.698 - hence le2: "c + b <= c + a" by (rule add_left_mono)
1.699 - have "a = b"
1.700 - apply (insert le)
1.701 - apply (insert le2)
1.702 - apply (drule antisym, simp_all)
1.703 - done
1.704 - with w show False
1.705 - by (simp add: linorder_not_le [symmetric])
1.706 - qed
1.707 -qed
1.708 -
1.709 -end
1.710 -
1.711 -class ordered_ab_group_add =
1.712 - linorder + pordered_ab_group_add
1.713 -begin
1.714 -
1.715 -subclass ordered_cancel_ab_semigroup_add ..
1.716 -
1.717 -lemma neg_less_eq_nonneg:
1.718 - "- a \<le> a \<longleftrightarrow> 0 \<le> a"
1.719 -proof
1.720 - assume A: "- a \<le> a" show "0 \<le> a"
1.721 - proof (rule classical)
1.722 - assume "\<not> 0 \<le> a"
1.723 - then have "a < 0" by auto
1.724 - with A have "- a < 0" by (rule le_less_trans)
1.725 - then show ?thesis by auto
1.726 - qed
1.727 -next
1.728 - assume A: "0 \<le> a" show "- a \<le> a"
1.729 - proof (rule order_trans)
1.730 - show "- a \<le> 0" using A by (simp add: minus_le_iff)
1.731 - next
1.732 - show "0 \<le> a" using A .
1.733 - qed
1.734 -qed
1.735 -
1.736 -lemma less_eq_neg_nonpos:
1.737 - "a \<le> - a \<longleftrightarrow> a \<le> 0"
1.738 -proof
1.739 - assume A: "a \<le> - a" show "a \<le> 0"
1.740 - proof (rule classical)
1.741 - assume "\<not> a \<le> 0"
1.742 - then have "0 < a" by auto
1.743 - then have "0 < - a" using A by (rule less_le_trans)
1.744 - then show ?thesis by auto
1.745 - qed
1.746 -next
1.747 - assume A: "a \<le> 0" show "a \<le> - a"
1.748 - proof (rule order_trans)
1.749 - show "0 \<le> - a" using A by (simp add: minus_le_iff)
1.750 - next
1.751 - show "a \<le> 0" using A .
1.752 - qed
1.753 -qed
1.754 -
1.755 -lemma equal_neg_zero:
1.756 - "a = - a \<longleftrightarrow> a = 0"
1.757 -proof
1.758 - assume "a = 0" then show "a = - a" by simp
1.759 -next
1.760 - assume A: "a = - a" show "a = 0"
1.761 - proof (cases "0 \<le> a")
1.762 - case True with A have "0 \<le> - a" by auto
1.763 - with le_minus_iff have "a \<le> 0" by simp
1.764 - with True show ?thesis by (auto intro: order_trans)
1.765 - next
1.766 - case False then have B: "a \<le> 0" by auto
1.767 - with A have "- a \<le> 0" by auto
1.768 - with B show ?thesis by (auto intro: order_trans)
1.769 - qed
1.770 -qed
1.771 -
1.772 -lemma neg_equal_zero:
1.773 - "- a = a \<longleftrightarrow> a = 0"
1.774 - unfolding equal_neg_zero [symmetric] by auto
1.775 -
1.776 -end
1.777 -
1.778 --- {* FIXME localize the following *}
1.779 -
1.780 -lemma add_increasing:
1.781 - fixes c :: "'a::{pordered_ab_semigroup_add_imp_le, comm_monoid_add}"
1.782 - shows "[|0\<le>a; b\<le>c|] ==> b \<le> a + c"
1.783 -by (insert add_mono [of 0 a b c], simp)
1.784 -
1.785 -lemma add_increasing2:
1.786 - fixes c :: "'a::{pordered_ab_semigroup_add_imp_le, comm_monoid_add}"
1.787 - shows "[|0\<le>c; b\<le>a|] ==> b \<le> a + c"
1.788 -by (simp add:add_increasing add_commute[of a])
1.789 -
1.790 -lemma add_strict_increasing:
1.791 - fixes c :: "'a::{pordered_ab_semigroup_add_imp_le, comm_monoid_add}"
1.792 - shows "[|0<a; b\<le>c|] ==> b < a + c"
1.793 -by (insert add_less_le_mono [of 0 a b c], simp)
1.794 -
1.795 -lemma add_strict_increasing2:
1.796 - fixes c :: "'a::{pordered_ab_semigroup_add_imp_le, comm_monoid_add}"
1.797 - shows "[|0\<le>a; b<c|] ==> b < a + c"
1.798 -by (insert add_le_less_mono [of 0 a b c], simp)
1.799 -
1.800 -
1.801 -class pordered_ab_group_add_abs = pordered_ab_group_add + abs +
1.802 - assumes abs_ge_zero [simp]: "\<bar>a\<bar> \<ge> 0"
1.803 - and abs_ge_self: "a \<le> \<bar>a\<bar>"
1.804 - and abs_leI: "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"
1.805 - and abs_minus_cancel [simp]: "\<bar>-a\<bar> = \<bar>a\<bar>"
1.806 - and abs_triangle_ineq: "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
1.807 -begin
1.808 -
1.809 -lemma abs_minus_le_zero: "- \<bar>a\<bar> \<le> 0"
1.810 - unfolding neg_le_0_iff_le by simp
1.811 -
1.812 -lemma abs_of_nonneg [simp]:
1.813 - assumes nonneg: "0 \<le> a" shows "\<bar>a\<bar> = a"
1.814 -proof (rule antisym)
1.815 - from nonneg le_imp_neg_le have "- a \<le> 0" by simp
1.816 - from this nonneg have "- a \<le> a" by (rule order_trans)
1.817 - then show "\<bar>a\<bar> \<le> a" by (auto intro: abs_leI)
1.818 -qed (rule abs_ge_self)
1.819 -
1.820 -lemma abs_idempotent [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>"
1.821 -by (rule antisym)
1.822 - (auto intro!: abs_ge_self abs_leI order_trans [of "uminus (abs a)" zero "abs a"])
1.823 -
1.824 -lemma abs_eq_0 [simp]: "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0"
1.825 -proof -
1.826 - have "\<bar>a\<bar> = 0 \<Longrightarrow> a = 0"
1.827 - proof (rule antisym)
1.828 - assume zero: "\<bar>a\<bar> = 0"
1.829 - with abs_ge_self show "a \<le> 0" by auto
1.830 - from zero have "\<bar>-a\<bar> = 0" by simp
1.831 - with abs_ge_self [of "uminus a"] have "- a \<le> 0" by auto
1.832 - with neg_le_0_iff_le show "0 \<le> a" by auto
1.833 - qed
1.834 - then show ?thesis by auto
1.835 -qed
1.836 -
1.837 -lemma abs_zero [simp]: "\<bar>0\<bar> = 0"
1.838 -by simp
1.839 -
1.840 -lemma abs_0_eq [simp, noatp]: "0 = \<bar>a\<bar> \<longleftrightarrow> a = 0"
1.841 -proof -
1.842 - have "0 = \<bar>a\<bar> \<longleftrightarrow> \<bar>a\<bar> = 0" by (simp only: eq_ac)
1.843 - thus ?thesis by simp
1.844 -qed
1.845 -
1.846 -lemma abs_le_zero_iff [simp]: "\<bar>a\<bar> \<le> 0 \<longleftrightarrow> a = 0"
1.847 -proof
1.848 - assume "\<bar>a\<bar> \<le> 0"
1.849 - then have "\<bar>a\<bar> = 0" by (rule antisym) simp
1.850 - thus "a = 0" by simp
1.851 -next
1.852 - assume "a = 0"
1.853 - thus "\<bar>a\<bar> \<le> 0" by simp
1.854 -qed
1.855 -
1.856 -lemma zero_less_abs_iff [simp]: "0 < \<bar>a\<bar> \<longleftrightarrow> a \<noteq> 0"
1.857 -by (simp add: less_le)
1.858 -
1.859 -lemma abs_not_less_zero [simp]: "\<not> \<bar>a\<bar> < 0"
1.860 -proof -
1.861 - have a: "\<And>x y. x \<le> y \<Longrightarrow> \<not> y < x" by auto
1.862 - show ?thesis by (simp add: a)
1.863 -qed
1.864 -
1.865 -lemma abs_ge_minus_self: "- a \<le> \<bar>a\<bar>"
1.866 -proof -
1.867 - have "- a \<le> \<bar>-a\<bar>" by (rule abs_ge_self)
1.868 - then show ?thesis by simp
1.869 -qed
1.870 -
1.871 -lemma abs_minus_commute:
1.872 - "\<bar>a - b\<bar> = \<bar>b - a\<bar>"
1.873 -proof -
1.874 - have "\<bar>a - b\<bar> = \<bar>- (a - b)\<bar>" by (simp only: abs_minus_cancel)
1.875 - also have "... = \<bar>b - a\<bar>" by simp
1.876 - finally show ?thesis .
1.877 -qed
1.878 -
1.879 -lemma abs_of_pos: "0 < a \<Longrightarrow> \<bar>a\<bar> = a"
1.880 -by (rule abs_of_nonneg, rule less_imp_le)
1.881 -
1.882 -lemma abs_of_nonpos [simp]:
1.883 - assumes "a \<le> 0" shows "\<bar>a\<bar> = - a"
1.884 -proof -
1.885 - let ?b = "- a"
1.886 - have "- ?b \<le> 0 \<Longrightarrow> \<bar>- ?b\<bar> = - (- ?b)"
1.887 - unfolding abs_minus_cancel [of "?b"]
1.888 - unfolding neg_le_0_iff_le [of "?b"]
1.889 - unfolding minus_minus by (erule abs_of_nonneg)
1.890 - then show ?thesis using assms by auto
1.891 -qed
1.892 -
1.893 -lemma abs_of_neg: "a < 0 \<Longrightarrow> \<bar>a\<bar> = - a"
1.894 -by (rule abs_of_nonpos, rule less_imp_le)
1.895 -
1.896 -lemma abs_le_D1: "\<bar>a\<bar> \<le> b \<Longrightarrow> a \<le> b"
1.897 -by (insert abs_ge_self, blast intro: order_trans)
1.898 -
1.899 -lemma abs_le_D2: "\<bar>a\<bar> \<le> b \<Longrightarrow> - a \<le> b"
1.900 -by (insert abs_le_D1 [of "uminus a"], simp)
1.901 -
1.902 -lemma abs_le_iff: "\<bar>a\<bar> \<le> b \<longleftrightarrow> a \<le> b \<and> - a \<le> b"
1.903 -by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2)
1.904 -
1.905 -lemma abs_triangle_ineq2: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>a - b\<bar>"
1.906 - apply (simp add: algebra_simps)
1.907 - apply (subgoal_tac "abs a = abs (plus b (minus a b))")
1.908 - apply (erule ssubst)
1.909 - apply (rule abs_triangle_ineq)
1.910 - apply (rule arg_cong[of _ _ abs])
1.911 - apply (simp add: algebra_simps)
1.912 -done
1.913 -
1.914 -lemma abs_triangle_ineq3: "\<bar>\<bar>a\<bar> - \<bar>b\<bar>\<bar> \<le> \<bar>a - b\<bar>"
1.915 - apply (subst abs_le_iff)
1.916 - apply auto
1.917 - apply (rule abs_triangle_ineq2)
1.918 - apply (subst abs_minus_commute)
1.919 - apply (rule abs_triangle_ineq2)
1.920 -done
1.921 -
1.922 -lemma abs_triangle_ineq4: "\<bar>a - b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
1.923 -proof -
1.924 - have "abs(a - b) = abs(a + - b)" by (subst diff_minus, rule refl)
1.925 - also have "... <= abs a + abs (- b)" by (rule abs_triangle_ineq)
1.926 - finally show ?thesis by simp
1.927 -qed
1.928 -
1.929 -lemma abs_diff_triangle_ineq: "\<bar>a + b - (c + d)\<bar> \<le> \<bar>a - c\<bar> + \<bar>b - d\<bar>"
1.930 -proof -
1.931 - have "\<bar>a + b - (c+d)\<bar> = \<bar>(a-c) + (b-d)\<bar>" by (simp add: diff_minus add_ac)
1.932 - also have "... \<le> \<bar>a-c\<bar> + \<bar>b-d\<bar>" by (rule abs_triangle_ineq)
1.933 - finally show ?thesis .
1.934 -qed
1.935 -
1.936 -lemma abs_add_abs [simp]:
1.937 - "\<bar>\<bar>a\<bar> + \<bar>b\<bar>\<bar> = \<bar>a\<bar> + \<bar>b\<bar>" (is "?L = ?R")
1.938 -proof (rule antisym)
1.939 - show "?L \<ge> ?R" by(rule abs_ge_self)
1.940 -next
1.941 - have "?L \<le> \<bar>\<bar>a\<bar>\<bar> + \<bar>\<bar>b\<bar>\<bar>" by(rule abs_triangle_ineq)
1.942 - also have "\<dots> = ?R" by simp
1.943 - finally show "?L \<le> ?R" .
1.944 -qed
1.945 -
1.946 -end
1.947 -
1.948 -
1.949 -subsection {* Lattice Ordered (Abelian) Groups *}
1.950 -
1.951 -class lordered_ab_group_add_meet = pordered_ab_group_add + lower_semilattice
1.952 -begin
1.953 -
1.954 -lemma add_inf_distrib_left:
1.955 - "a + inf b c = inf (a + b) (a + c)"
1.956 -apply (rule antisym)
1.957 -apply (simp_all add: le_infI)
1.958 -apply (rule add_le_imp_le_left [of "uminus a"])
1.959 -apply (simp only: add_assoc [symmetric], simp)
1.960 -apply rule
1.961 -apply (rule add_le_imp_le_left[of "a"], simp only: add_assoc[symmetric], simp)+
1.962 -done
1.963 -
1.964 -lemma add_inf_distrib_right:
1.965 - "inf a b + c = inf (a + c) (b + c)"
1.966 -proof -
1.967 - have "c + inf a b = inf (c+a) (c+b)" by (simp add: add_inf_distrib_left)
1.968 - thus ?thesis by (simp add: add_commute)
1.969 -qed
1.970 -
1.971 -end
1.972 -
1.973 -class lordered_ab_group_add_join = pordered_ab_group_add + upper_semilattice
1.974 -begin
1.975 -
1.976 -lemma add_sup_distrib_left:
1.977 - "a + sup b c = sup (a + b) (a + c)"
1.978 -apply (rule antisym)
1.979 -apply (rule add_le_imp_le_left [of "uminus a"])
1.980 -apply (simp only: add_assoc[symmetric], simp)
1.981 -apply rule
1.982 -apply (rule add_le_imp_le_left [of "a"], simp only: add_assoc[symmetric], simp)+
1.983 -apply (rule le_supI)
1.984 -apply (simp_all)
1.985 -done
1.986 -
1.987 -lemma add_sup_distrib_right:
1.988 - "sup a b + c = sup (a+c) (b+c)"
1.989 -proof -
1.990 - have "c + sup a b = sup (c+a) (c+b)" by (simp add: add_sup_distrib_left)
1.991 - thus ?thesis by (simp add: add_commute)
1.992 -qed
1.993 -
1.994 -end
1.995 -
1.996 -class lordered_ab_group_add = pordered_ab_group_add + lattice
1.997 -begin
1.998 -
1.999 -subclass lordered_ab_group_add_meet ..
1.1000 -subclass lordered_ab_group_add_join ..
1.1001 -
1.1002 -lemmas add_sup_inf_distribs = add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left
1.1003 -
1.1004 -lemma inf_eq_neg_sup: "inf a b = - sup (-a) (-b)"
1.1005 -proof (rule inf_unique)
1.1006 - fix a b :: 'a
1.1007 - show "- sup (-a) (-b) \<le> a"
1.1008 - by (rule add_le_imp_le_right [of _ "sup (uminus a) (uminus b)"])
1.1009 - (simp, simp add: add_sup_distrib_left)
1.1010 -next
1.1011 - fix a b :: 'a
1.1012 - show "- sup (-a) (-b) \<le> b"
1.1013 - by (rule add_le_imp_le_right [of _ "sup (uminus a) (uminus b)"])
1.1014 - (simp, simp add: add_sup_distrib_left)
1.1015 -next
1.1016 - fix a b c :: 'a
1.1017 - assume "a \<le> b" "a \<le> c"
1.1018 - then show "a \<le> - sup (-b) (-c)" by (subst neg_le_iff_le [symmetric])
1.1019 - (simp add: le_supI)
1.1020 -qed
1.1021 -
1.1022 -lemma sup_eq_neg_inf: "sup a b = - inf (-a) (-b)"
1.1023 -proof (rule sup_unique)
1.1024 - fix a b :: 'a
1.1025 - show "a \<le> - inf (-a) (-b)"
1.1026 - by (rule add_le_imp_le_right [of _ "inf (uminus a) (uminus b)"])
1.1027 - (simp, simp add: add_inf_distrib_left)
1.1028 -next
1.1029 - fix a b :: 'a
1.1030 - show "b \<le> - inf (-a) (-b)"
1.1031 - by (rule add_le_imp_le_right [of _ "inf (uminus a) (uminus b)"])
1.1032 - (simp, simp add: add_inf_distrib_left)
1.1033 -next
1.1034 - fix a b c :: 'a
1.1035 - assume "a \<le> c" "b \<le> c"
1.1036 - then show "- inf (-a) (-b) \<le> c" by (subst neg_le_iff_le [symmetric])
1.1037 - (simp add: le_infI)
1.1038 -qed
1.1039 -
1.1040 -lemma neg_inf_eq_sup: "- inf a b = sup (-a) (-b)"
1.1041 -by (simp add: inf_eq_neg_sup)
1.1042 -
1.1043 -lemma neg_sup_eq_inf: "- sup a b = inf (-a) (-b)"
1.1044 -by (simp add: sup_eq_neg_inf)
1.1045 -
1.1046 -lemma add_eq_inf_sup: "a + b = sup a b + inf a b"
1.1047 -proof -
1.1048 - have "0 = - inf 0 (a-b) + inf (a-b) 0" by (simp add: inf_commute)
1.1049 - hence "0 = sup 0 (b-a) + inf (a-b) 0" by (simp add: inf_eq_neg_sup)
1.1050 - hence "0 = (-a + sup a b) + (inf a b + (-b))"
1.1051 - by (simp add: add_sup_distrib_left add_inf_distrib_right)
1.1052 - (simp add: algebra_simps)
1.1053 - thus ?thesis by (simp add: algebra_simps)
1.1054 -qed
1.1055 -
1.1056 -subsection {* Positive Part, Negative Part, Absolute Value *}
1.1057 -
1.1058 -definition
1.1059 - nprt :: "'a \<Rightarrow> 'a" where
1.1060 - "nprt x = inf x 0"
1.1061 -
1.1062 -definition
1.1063 - pprt :: "'a \<Rightarrow> 'a" where
1.1064 - "pprt x = sup x 0"
1.1065 -
1.1066 -lemma pprt_neg: "pprt (- x) = - nprt x"
1.1067 -proof -
1.1068 - have "sup (- x) 0 = sup (- x) (- 0)" unfolding minus_zero ..
1.1069 - also have "\<dots> = - inf x 0" unfolding neg_inf_eq_sup ..
1.1070 - finally have "sup (- x) 0 = - inf x 0" .
1.1071 - then show ?thesis unfolding pprt_def nprt_def .
1.1072 -qed
1.1073 -
1.1074 -lemma nprt_neg: "nprt (- x) = - pprt x"
1.1075 -proof -
1.1076 - from pprt_neg have "pprt (- (- x)) = - nprt (- x)" .
1.1077 - then have "pprt x = - nprt (- x)" by simp
1.1078 - then show ?thesis by simp
1.1079 -qed
1.1080 -
1.1081 -lemma prts: "a = pprt a + nprt a"
1.1082 -by (simp add: pprt_def nprt_def add_eq_inf_sup[symmetric])
1.1083 -
1.1084 -lemma zero_le_pprt[simp]: "0 \<le> pprt a"
1.1085 -by (simp add: pprt_def)
1.1086 -
1.1087 -lemma nprt_le_zero[simp]: "nprt a \<le> 0"
1.1088 -by (simp add: nprt_def)
1.1089 -
1.1090 -lemma le_eq_neg: "a \<le> - b \<longleftrightarrow> a + b \<le> 0" (is "?l = ?r")
1.1091 -proof -
1.1092 - have a: "?l \<longrightarrow> ?r"
1.1093 - apply (auto)
1.1094 - apply (rule add_le_imp_le_right[of _ "uminus b" _])
1.1095 - apply (simp add: add_assoc)
1.1096 - done
1.1097 - have b: "?r \<longrightarrow> ?l"
1.1098 - apply (auto)
1.1099 - apply (rule add_le_imp_le_right[of _ "b" _])
1.1100 - apply (simp)
1.1101 - done
1.1102 - from a b show ?thesis by blast
1.1103 -qed
1.1104 -
1.1105 -lemma pprt_0[simp]: "pprt 0 = 0" by (simp add: pprt_def)
1.1106 -lemma nprt_0[simp]: "nprt 0 = 0" by (simp add: nprt_def)
1.1107 -
1.1108 -lemma pprt_eq_id [simp, noatp]: "0 \<le> x \<Longrightarrow> pprt x = x"
1.1109 - by (simp add: pprt_def sup_aci sup_absorb1)
1.1110 -
1.1111 -lemma nprt_eq_id [simp, noatp]: "x \<le> 0 \<Longrightarrow> nprt x = x"
1.1112 - by (simp add: nprt_def inf_aci inf_absorb1)
1.1113 -
1.1114 -lemma pprt_eq_0 [simp, noatp]: "x \<le> 0 \<Longrightarrow> pprt x = 0"
1.1115 - by (simp add: pprt_def sup_aci sup_absorb2)
1.1116 -
1.1117 -lemma nprt_eq_0 [simp, noatp]: "0 \<le> x \<Longrightarrow> nprt x = 0"
1.1118 - by (simp add: nprt_def inf_aci inf_absorb2)
1.1119 -
1.1120 -lemma sup_0_imp_0: "sup a (- a) = 0 \<Longrightarrow> a = 0"
1.1121 -proof -
1.1122 - {
1.1123 - fix a::'a
1.1124 - assume hyp: "sup a (-a) = 0"
1.1125 - hence "sup a (-a) + a = a" by (simp)
1.1126 - hence "sup (a+a) 0 = a" by (simp add: add_sup_distrib_right)
1.1127 - hence "sup (a+a) 0 <= a" by (simp)
1.1128 - hence "0 <= a" by (blast intro: order_trans inf_sup_ord)
1.1129 - }
1.1130 - note p = this
1.1131 - assume hyp:"sup a (-a) = 0"
1.1132 - hence hyp2:"sup (-a) (-(-a)) = 0" by (simp add: sup_commute)
1.1133 - from p[OF hyp] p[OF hyp2] show "a = 0" by simp
1.1134 -qed
1.1135 -
1.1136 -lemma inf_0_imp_0: "inf a (-a) = 0 \<Longrightarrow> a = 0"
1.1137 -apply (simp add: inf_eq_neg_sup)
1.1138 -apply (simp add: sup_commute)
1.1139 -apply (erule sup_0_imp_0)
1.1140 -done
1.1141 -
1.1142 -lemma inf_0_eq_0 [simp, noatp]: "inf a (- a) = 0 \<longleftrightarrow> a = 0"
1.1143 -by (rule, erule inf_0_imp_0) simp
1.1144 -
1.1145 -lemma sup_0_eq_0 [simp, noatp]: "sup a (- a) = 0 \<longleftrightarrow> a = 0"
1.1146 -by (rule, erule sup_0_imp_0) simp
1.1147 -
1.1148 -lemma zero_le_double_add_iff_zero_le_single_add [simp]:
1.1149 - "0 \<le> a + a \<longleftrightarrow> 0 \<le> a"
1.1150 -proof
1.1151 - assume "0 <= a + a"
1.1152 - hence a:"inf (a+a) 0 = 0" by (simp add: inf_commute inf_absorb1)
1.1153 - have "(inf a 0)+(inf a 0) = inf (inf (a+a) 0) a" (is "?l=_")
1.1154 - by (simp add: add_sup_inf_distribs inf_aci)
1.1155 - hence "?l = 0 + inf a 0" by (simp add: a, simp add: inf_commute)
1.1156 - hence "inf a 0 = 0" by (simp only: add_right_cancel)
1.1157 - then show "0 <= a" unfolding le_iff_inf by (simp add: inf_commute)
1.1158 -next
1.1159 - assume a: "0 <= a"
1.1160 - show "0 <= a + a" by (simp add: add_mono[OF a a, simplified])
1.1161 -qed
1.1162 -
1.1163 -lemma double_zero: "a + a = 0 \<longleftrightarrow> a = 0"
1.1164 -proof
1.1165 - assume assm: "a + a = 0"
1.1166 - then have "a + a + - a = - a" by simp
1.1167 - then have "a + (a + - a) = - a" by (simp only: add_assoc)
1.1168 - then have a: "- a = a" by simp
1.1169 - show "a = 0" apply (rule antisym)
1.1170 - apply (unfold neg_le_iff_le [symmetric, of a])
1.1171 - unfolding a apply simp
1.1172 - unfolding zero_le_double_add_iff_zero_le_single_add [symmetric, of a]
1.1173 - unfolding assm unfolding le_less apply simp_all done
1.1174 -next
1.1175 - assume "a = 0" then show "a + a = 0" by simp
1.1176 -qed
1.1177 -
1.1178 -lemma zero_less_double_add_iff_zero_less_single_add:
1.1179 - "0 < a + a \<longleftrightarrow> 0 < a"
1.1180 -proof (cases "a = 0")
1.1181 - case True then show ?thesis by auto
1.1182 -next
1.1183 - case False then show ?thesis (*FIXME tune proof*)
1.1184 - unfolding less_le apply simp apply rule
1.1185 - apply clarify
1.1186 - apply rule
1.1187 - apply assumption
1.1188 - apply (rule notI)
1.1189 - unfolding double_zero [symmetric, of a] apply simp
1.1190 - done
1.1191 -qed
1.1192 -
1.1193 -lemma double_add_le_zero_iff_single_add_le_zero [simp]:
1.1194 - "a + a \<le> 0 \<longleftrightarrow> a \<le> 0"
1.1195 -proof -
1.1196 - have "a + a \<le> 0 \<longleftrightarrow> 0 \<le> - (a + a)" by (subst le_minus_iff, simp)
1.1197 - moreover have "\<dots> \<longleftrightarrow> a \<le> 0" by (simp add: zero_le_double_add_iff_zero_le_single_add)
1.1198 - ultimately show ?thesis by blast
1.1199 -qed
1.1200 -
1.1201 -lemma double_add_less_zero_iff_single_less_zero [simp]:
1.1202 - "a + a < 0 \<longleftrightarrow> a < 0"
1.1203 -proof -
1.1204 - have "a + a < 0 \<longleftrightarrow> 0 < - (a + a)" by (subst less_minus_iff, simp)
1.1205 - moreover have "\<dots> \<longleftrightarrow> a < 0" by (simp add: zero_less_double_add_iff_zero_less_single_add)
1.1206 - ultimately show ?thesis by blast
1.1207 -qed
1.1208 -
1.1209 -declare neg_inf_eq_sup [simp] neg_sup_eq_inf [simp]
1.1210 -
1.1211 -lemma le_minus_self_iff: "a \<le> - a \<longleftrightarrow> a \<le> 0"
1.1212 -proof -
1.1213 - from add_le_cancel_left [of "uminus a" "plus a a" zero]
1.1214 - have "(a <= -a) = (a+a <= 0)"
1.1215 - by (simp add: add_assoc[symmetric])
1.1216 - thus ?thesis by simp
1.1217 -qed
1.1218 -
1.1219 -lemma minus_le_self_iff: "- a \<le> a \<longleftrightarrow> 0 \<le> a"
1.1220 -proof -
1.1221 - from add_le_cancel_left [of "uminus a" zero "plus a a"]
1.1222 - have "(-a <= a) = (0 <= a+a)"
1.1223 - by (simp add: add_assoc[symmetric])
1.1224 - thus ?thesis by simp
1.1225 -qed
1.1226 -
1.1227 -lemma zero_le_iff_zero_nprt: "0 \<le> a \<longleftrightarrow> nprt a = 0"
1.1228 -unfolding le_iff_inf by (simp add: nprt_def inf_commute)
1.1229 -
1.1230 -lemma le_zero_iff_zero_pprt: "a \<le> 0 \<longleftrightarrow> pprt a = 0"
1.1231 -unfolding le_iff_sup by (simp add: pprt_def sup_commute)
1.1232 -
1.1233 -lemma le_zero_iff_pprt_id: "0 \<le> a \<longleftrightarrow> pprt a = a"
1.1234 -unfolding le_iff_sup by (simp add: pprt_def sup_commute)
1.1235 -
1.1236 -lemma zero_le_iff_nprt_id: "a \<le> 0 \<longleftrightarrow> nprt a = a"
1.1237 -unfolding le_iff_inf by (simp add: nprt_def inf_commute)
1.1238 -
1.1239 -lemma pprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> pprt a \<le> pprt b"
1.1240 -unfolding le_iff_sup by (simp add: pprt_def sup_aci sup_assoc [symmetric, of a])
1.1241 -
1.1242 -lemma nprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> nprt a \<le> nprt b"
1.1243 -unfolding le_iff_inf by (simp add: nprt_def inf_aci inf_assoc [symmetric, of a])
1.1244 -
1.1245 -end
1.1246 -
1.1247 -lemmas add_sup_inf_distribs = add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left
1.1248 -
1.1249 -
1.1250 -class lordered_ab_group_add_abs = lordered_ab_group_add + abs +
1.1251 - assumes abs_lattice: "\<bar>a\<bar> = sup a (- a)"
1.1252 -begin
1.1253 -
1.1254 -lemma abs_prts: "\<bar>a\<bar> = pprt a - nprt a"
1.1255 -proof -
1.1256 - have "0 \<le> \<bar>a\<bar>"
1.1257 - proof -
1.1258 - have a: "a \<le> \<bar>a\<bar>" and b: "- a \<le> \<bar>a\<bar>" by (auto simp add: abs_lattice)
1.1259 - show ?thesis by (rule add_mono [OF a b, simplified])
1.1260 - qed
1.1261 - then have "0 \<le> sup a (- a)" unfolding abs_lattice .
1.1262 - then have "sup (sup a (- a)) 0 = sup a (- a)" by (rule sup_absorb1)
1.1263 - then show ?thesis
1.1264 - by (simp add: add_sup_inf_distribs sup_aci
1.1265 - pprt_def nprt_def diff_minus abs_lattice)
1.1266 -qed
1.1267 -
1.1268 -subclass pordered_ab_group_add_abs
1.1269 -proof
1.1270 - have abs_ge_zero [simp]: "\<And>a. 0 \<le> \<bar>a\<bar>"
1.1271 - proof -
1.1272 - fix a b
1.1273 - have a: "a \<le> \<bar>a\<bar>" and b: "- a \<le> \<bar>a\<bar>" by (auto simp add: abs_lattice)
1.1274 - show "0 \<le> \<bar>a\<bar>" by (rule add_mono [OF a b, simplified])
1.1275 - qed
1.1276 - have abs_leI: "\<And>a b. a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"
1.1277 - by (simp add: abs_lattice le_supI)
1.1278 - fix a b
1.1279 - show "0 \<le> \<bar>a\<bar>" by simp
1.1280 - show "a \<le> \<bar>a\<bar>"
1.1281 - by (auto simp add: abs_lattice)
1.1282 - show "\<bar>-a\<bar> = \<bar>a\<bar>"
1.1283 - by (simp add: abs_lattice sup_commute)
1.1284 - show "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b" by (fact abs_leI)
1.1285 - show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
1.1286 - proof -
1.1287 - have g:"abs a + abs b = sup (a+b) (sup (-a-b) (sup (-a+b) (a + (-b))))" (is "_=sup ?m ?n")
1.1288 - by (simp add: abs_lattice add_sup_inf_distribs sup_aci diff_minus)
1.1289 - have a:"a+b <= sup ?m ?n" by (simp)
1.1290 - have b:"-a-b <= ?n" by (simp)
1.1291 - have c:"?n <= sup ?m ?n" by (simp)
1.1292 - from b c have d: "-a-b <= sup ?m ?n" by(rule order_trans)
1.1293 - have e:"-a-b = -(a+b)" by (simp add: diff_minus)
1.1294 - from a d e have "abs(a+b) <= sup ?m ?n"
1.1295 - by (drule_tac abs_leI, auto)
1.1296 - with g[symmetric] show ?thesis by simp
1.1297 - qed
1.1298 -qed
1.1299 -
1.1300 -end
1.1301 -
1.1302 -lemma sup_eq_if:
1.1303 - fixes a :: "'a\<Colon>{lordered_ab_group_add, linorder}"
1.1304 - shows "sup a (- a) = (if a < 0 then - a else a)"
1.1305 -proof -
1.1306 - note add_le_cancel_right [of a a "- a", symmetric, simplified]
1.1307 - moreover note add_le_cancel_right [of "-a" a a, symmetric, simplified]
1.1308 - then show ?thesis by (auto simp: sup_max min_max.sup_absorb1 min_max.sup_absorb2)
1.1309 -qed
1.1310 -
1.1311 -lemma abs_if_lattice:
1.1312 - fixes a :: "'a\<Colon>{lordered_ab_group_add_abs, linorder}"
1.1313 - shows "\<bar>a\<bar> = (if a < 0 then - a else a)"
1.1314 -by auto
1.1315 -
1.1316 -
1.1317 -text {* Needed for abelian cancellation simprocs: *}
1.1318 -
1.1319 -lemma add_cancel_21: "((x::'a::ab_group_add) + (y + z) = y + u) = (x + z = u)"
1.1320 -apply (subst add_left_commute)
1.1321 -apply (subst add_left_cancel)
1.1322 -apply simp
1.1323 -done
1.1324 -
1.1325 -lemma add_cancel_end: "(x + (y + z) = y) = (x = - (z::'a::ab_group_add))"
1.1326 -apply (subst add_cancel_21[of _ _ _ 0, simplified])
1.1327 -apply (simp add: add_right_cancel[symmetric, of "x" "-z" "z", simplified])
1.1328 -done
1.1329 -
1.1330 -lemma less_eqI: "(x::'a::pordered_ab_group_add) - y = x' - y' \<Longrightarrow> (x < y) = (x' < y')"
1.1331 -by (simp add: less_iff_diff_less_0[of x y] less_iff_diff_less_0[of x' y'])
1.1332 -
1.1333 -lemma le_eqI: "(x::'a::pordered_ab_group_add) - y = x' - y' \<Longrightarrow> (y <= x) = (y' <= x')"
1.1334 -apply (simp add: le_iff_diff_le_0[of y x] le_iff_diff_le_0[of y' x'])
1.1335 -apply (simp add: neg_le_iff_le[symmetric, of "y-x" 0] neg_le_iff_le[symmetric, of "y'-x'" 0])
1.1336 -done
1.1337 -
1.1338 -lemma eq_eqI: "(x::'a::ab_group_add) - y = x' - y' \<Longrightarrow> (x = y) = (x' = y')"
1.1339 -by (simp only: eq_iff_diff_eq_0[of x y] eq_iff_diff_eq_0[of x' y'])
1.1340 -
1.1341 -lemma diff_def: "(x::'a::ab_group_add) - y == x + (-y)"
1.1342 -by (simp add: diff_minus)
1.1343 -
1.1344 -lemma le_add_right_mono:
1.1345 - assumes
1.1346 - "a <= b + (c::'a::pordered_ab_group_add)"
1.1347 - "c <= d"
1.1348 - shows "a <= b + d"
1.1349 - apply (rule_tac order_trans[where y = "b+c"])
1.1350 - apply (simp_all add: prems)
1.1351 - done
1.1352 -
1.1353 -lemma estimate_by_abs:
1.1354 - "a + b <= (c::'a::lordered_ab_group_add_abs) \<Longrightarrow> a <= c + abs b"
1.1355 -proof -
1.1356 - assume "a+b <= c"
1.1357 - hence 2: "a <= c+(-b)" by (simp add: algebra_simps)
1.1358 - have 3: "(-b) <= abs b" by (rule abs_ge_minus_self)
1.1359 - show ?thesis by (rule le_add_right_mono[OF 2 3])
1.1360 -qed
1.1361 -
1.1362 -subsection {* Tools setup *}
1.1363 -
1.1364 -lemma add_mono_thms_ordered_semiring [noatp]:
1.1365 - fixes i j k :: "'a\<Colon>pordered_ab_semigroup_add"
1.1366 - shows "i \<le> j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
1.1367 - and "i = j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
1.1368 - and "i \<le> j \<and> k = l \<Longrightarrow> i + k \<le> j + l"
1.1369 - and "i = j \<and> k = l \<Longrightarrow> i + k = j + l"
1.1370 -by (rule add_mono, clarify+)+
1.1371 -
1.1372 -lemma add_mono_thms_ordered_field [noatp]:
1.1373 - fixes i j k :: "'a\<Colon>pordered_cancel_ab_semigroup_add"
1.1374 - shows "i < j \<and> k = l \<Longrightarrow> i + k < j + l"
1.1375 - and "i = j \<and> k < l \<Longrightarrow> i + k < j + l"
1.1376 - and "i < j \<and> k \<le> l \<Longrightarrow> i + k < j + l"
1.1377 - and "i \<le> j \<and> k < l \<Longrightarrow> i + k < j + l"
1.1378 - and "i < j \<and> k < l \<Longrightarrow> i + k < j + l"
1.1379 -by (auto intro: add_strict_right_mono add_strict_left_mono
1.1380 - add_less_le_mono add_le_less_mono add_strict_mono)
1.1381 -
1.1382 -text{*Simplification of @{term "x-y < 0"}, etc.*}
1.1383 -lemmas diff_less_0_iff_less [simp, noatp] = less_iff_diff_less_0 [symmetric]
1.1384 -lemmas diff_le_0_iff_le [simp, noatp] = le_iff_diff_le_0 [symmetric]
1.1385 -
1.1386 -ML {*
1.1387 -structure ab_group_add_cancel = Abel_Cancel
1.1388 -(
1.1389 -
1.1390 -(* term order for abelian groups *)
1.1391 -
1.1392 -fun agrp_ord (Const (a, _)) = find_index (fn a' => a = a')
1.1393 - [@{const_name Algebras.zero}, @{const_name Algebras.plus},
1.1394 - @{const_name Algebras.uminus}, @{const_name Algebras.minus}]
1.1395 - | agrp_ord _ = ~1;
1.1396 -
1.1397 -fun termless_agrp (a, b) = (TermOrd.term_lpo agrp_ord (a, b) = LESS);
1.1398 -
1.1399 -local
1.1400 - val ac1 = mk_meta_eq @{thm add_assoc};
1.1401 - val ac2 = mk_meta_eq @{thm add_commute};
1.1402 - val ac3 = mk_meta_eq @{thm add_left_commute};
1.1403 - fun solve_add_ac thy _ (_ $ (Const (@{const_name Algebras.plus},_) $ _ $ _) $ _) =
1.1404 - SOME ac1
1.1405 - | solve_add_ac thy _ (_ $ x $ (Const (@{const_name Algebras.plus},_) $ y $ z)) =
1.1406 - if termless_agrp (y, x) then SOME ac3 else NONE
1.1407 - | solve_add_ac thy _ (_ $ x $ y) =
1.1408 - if termless_agrp (y, x) then SOME ac2 else NONE
1.1409 - | solve_add_ac thy _ _ = NONE
1.1410 -in
1.1411 - val add_ac_proc = Simplifier.simproc @{theory}
1.1412 - "add_ac_proc" ["x + y::'a::ab_semigroup_add"] solve_add_ac;
1.1413 -end;
1.1414 -
1.1415 -val eq_reflection = @{thm eq_reflection};
1.1416 -
1.1417 -val T = @{typ "'a::ab_group_add"};
1.1418 -
1.1419 -val cancel_ss = HOL_basic_ss settermless termless_agrp
1.1420 - addsimprocs [add_ac_proc] addsimps
1.1421 - [@{thm add_0_left}, @{thm add_0_right}, @{thm diff_def},
1.1422 - @{thm minus_add_distrib}, @{thm minus_minus}, @{thm minus_zero},
1.1423 - @{thm right_minus}, @{thm left_minus}, @{thm add_minus_cancel},
1.1424 - @{thm minus_add_cancel}];
1.1425 -
1.1426 -val sum_pats = [@{cterm "x + y::'a::ab_group_add"}, @{cterm "x - y::'a::ab_group_add"}];
1.1427 -
1.1428 -val eqI_rules = [@{thm less_eqI}, @{thm le_eqI}, @{thm eq_eqI}];
1.1429 -
1.1430 -val dest_eqI =
1.1431 - fst o HOLogic.dest_bin "op =" HOLogic.boolT o HOLogic.dest_Trueprop o concl_of;
1.1432 -
1.1433 -);
1.1434 -*}
1.1435 -
1.1436 -ML {*
1.1437 - Addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv];
1.1438 -*}
1.1439 -
1.1440 -code_modulename SML
1.1441 - OrderedGroup Arith
1.1442 -
1.1443 -code_modulename OCaml
1.1444 - OrderedGroup Arith
1.1445 -
1.1446 -code_modulename Haskell
1.1447 - OrderedGroup Arith
1.1448 -
1.1449 -end