1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/OrderedGroup.thy Tue May 11 20:11:08 2004 +0200
1.3 @@ -0,0 +1,950 @@
1.4 +(* Title: HOL/Group.thy
1.5 + ID: $Id$
1.6 + Author: Gertrud Bauer and Markus Wenzel, TU Muenchen
1.7 + Lawrence C Paulson, University of Cambridge
1.8 + Revised and decoupled from Ring_and_Field.thy
1.9 + by Steven Obua, TU Muenchen, in May 2004
1.10 + License: GPL (GNU GENERAL PUBLIC LICENSE)
1.11 +*)
1.12 +
1.13 +header {* Ordered Groups *}
1.14 +
1.15 +theory OrderedGroup = Inductive + LOrder:
1.16 +
1.17 +text {*
1.18 + The theory of partially ordered groups is taken from the books:
1.19 + \begin{itemize}
1.20 + \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979
1.21 + \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963
1.22 + \end{itemize}
1.23 + Most of the used notions can also be looked up in
1.24 + \begin{itemize}
1.25 + \item \emph{www.mathworld.com} by Eric Weisstein et. al.
1.26 + \item \emph{Algebra I} by van der Waerden, Springer.
1.27 + \end{itemize}
1.28 +*}
1.29 +
1.30 +subsection {* Semigroups, Groups *}
1.31 +
1.32 +axclass semigroup_add \<subseteq> plus
1.33 + add_assoc: "(a + b) + c = a + (b + c)"
1.34 +
1.35 +axclass ab_semigroup_add \<subseteq> semigroup_add
1.36 + add_commute: "a + b = b + a"
1.37 +
1.38 +lemma add_left_commute: "a + (b + c) = b + (a + (c::'a::ab_semigroup_add))"
1.39 + by (rule mk_left_commute [of "op +", OF add_assoc add_commute])
1.40 +
1.41 +theorems add_ac = add_assoc add_commute add_left_commute
1.42 +
1.43 +axclass semigroup_mult \<subseteq> times
1.44 + mult_assoc: "(a * b) * c = a * (b * c)"
1.45 +
1.46 +axclass ab_semigroup_mult \<subseteq> semigroup_mult
1.47 + mult_commute: "a * b = b * a"
1.48 +
1.49 +lemma mult_left_commute: "a * (b * c) = b * (a * (c::'a::ab_semigroup_mult))"
1.50 + by (rule mk_left_commute [of "op *", OF mult_assoc mult_commute])
1.51 +
1.52 +theorems mult_ac = mult_assoc mult_commute mult_left_commute
1.53 +
1.54 +axclass comm_monoid_add \<subseteq> zero, ab_semigroup_add
1.55 + add_0[simp]: "0 + a = a"
1.56 +
1.57 +axclass monoid_mult \<subseteq> one, semigroup_mult
1.58 + mult_1_left[simp]: "1 * a = a"
1.59 + mult_1_right[simp]: "a * 1 = a"
1.60 +
1.61 +axclass comm_monoid_mult \<subseteq> one, ab_semigroup_mult
1.62 + mult_1: "1 * a = a"
1.63 +
1.64 +instance comm_monoid_mult \<subseteq> monoid_mult
1.65 +by (intro_classes, insert mult_1, simp_all add: mult_commute, auto)
1.66 +
1.67 +axclass cancel_semigroup_add \<subseteq> semigroup_add
1.68 + add_left_imp_eq: "a + b = a + c \<Longrightarrow> b = c"
1.69 + add_right_imp_eq: "b + a = c + a \<Longrightarrow> b = c"
1.70 +
1.71 +axclass cancel_ab_semigroup_add \<subseteq> ab_semigroup_add
1.72 + add_imp_eq: "a + b = a + c \<Longrightarrow> b = c"
1.73 +
1.74 +instance cancel_ab_semigroup_add \<subseteq> cancel_semigroup_add
1.75 +proof
1.76 + {
1.77 + fix a b c :: 'a
1.78 + assume "a + b = a + c"
1.79 + thus "b = c" by (rule add_imp_eq)
1.80 + }
1.81 + note f = this
1.82 + fix a b c :: 'a
1.83 + assume "b + a = c + a"
1.84 + hence "a + b = a + c" by (simp only: add_commute)
1.85 + thus "b = c" by (rule f)
1.86 +qed
1.87 +
1.88 +axclass ab_group_add \<subseteq> minus, comm_monoid_add
1.89 + left_minus[simp]: " - a + a = 0"
1.90 + diff_minus: "a - b = a + (-b)"
1.91 +
1.92 +instance ab_group_add \<subseteq> cancel_ab_semigroup_add
1.93 +proof
1.94 + fix a b c :: 'a
1.95 + assume "a + b = a + c"
1.96 + hence "-a + a + b = -a + a + c" by (simp only: add_assoc)
1.97 + thus "b = c" by simp
1.98 +qed
1.99 +
1.100 +lemma add_0_right [simp]: "a + 0 = (a::'a::comm_monoid_add)"
1.101 +proof -
1.102 + have "a + 0 = 0 + a" by (simp only: add_commute)
1.103 + also have "... = a" by simp
1.104 + finally show ?thesis .
1.105 +qed
1.106 +
1.107 +lemma add_left_cancel [simp]:
1.108 + "(a + b = a + c) = (b = (c::'a::cancel_semigroup_add))"
1.109 +by (blast dest: add_left_imp_eq)
1.110 +
1.111 +lemma add_right_cancel [simp]:
1.112 + "(b + a = c + a) = (b = (c::'a::cancel_semigroup_add))"
1.113 + by (blast dest: add_right_imp_eq)
1.114 +
1.115 +lemma right_minus [simp]: "a + -(a::'a::ab_group_add) = 0"
1.116 +proof -
1.117 + have "a + -a = -a + a" by (simp add: add_ac)
1.118 + also have "... = 0" by simp
1.119 + finally show ?thesis .
1.120 +qed
1.121 +
1.122 +lemma right_minus_eq: "(a - b = 0) = (a = (b::'a::ab_group_add))"
1.123 +proof
1.124 + have "a = a - b + b" by (simp add: diff_minus add_ac)
1.125 + also assume "a - b = 0"
1.126 + finally show "a = b" by simp
1.127 +next
1.128 + assume "a = b"
1.129 + thus "a - b = 0" by (simp add: diff_minus)
1.130 +qed
1.131 +
1.132 +lemma minus_minus [simp]: "- (- (a::'a::ab_group_add)) = a"
1.133 +proof (rule add_left_cancel [of "-a", THEN iffD1])
1.134 + show "(-a + -(-a) = -a + a)"
1.135 + by simp
1.136 +qed
1.137 +
1.138 +lemma equals_zero_I: "a+b = 0 ==> -a = (b::'a::ab_group_add)"
1.139 +apply (rule right_minus_eq [THEN iffD1, symmetric])
1.140 +apply (simp add: diff_minus add_commute)
1.141 +done
1.142 +
1.143 +lemma minus_zero [simp]: "- 0 = (0::'a::ab_group_add)"
1.144 +by (simp add: equals_zero_I)
1.145 +
1.146 +lemma diff_self [simp]: "a - (a::'a::ab_group_add) = 0"
1.147 + by (simp add: diff_minus)
1.148 +
1.149 +lemma diff_0 [simp]: "(0::'a::ab_group_add) - a = -a"
1.150 +by (simp add: diff_minus)
1.151 +
1.152 +lemma diff_0_right [simp]: "a - (0::'a::ab_group_add) = a"
1.153 +by (simp add: diff_minus)
1.154 +
1.155 +lemma diff_minus_eq_add [simp]: "a - - b = a + (b::'a::ab_group_add)"
1.156 +by (simp add: diff_minus)
1.157 +
1.158 +lemma neg_equal_iff_equal [simp]: "(-a = -b) = (a = (b::'a::ab_group_add))"
1.159 +proof
1.160 + assume "- a = - b"
1.161 + hence "- (- a) = - (- b)"
1.162 + by simp
1.163 + thus "a=b" by simp
1.164 +next
1.165 + assume "a=b"
1.166 + thus "-a = -b" by simp
1.167 +qed
1.168 +
1.169 +lemma neg_equal_0_iff_equal [simp]: "(-a = 0) = (a = (0::'a::ab_group_add))"
1.170 +by (subst neg_equal_iff_equal [symmetric], simp)
1.171 +
1.172 +lemma neg_0_equal_iff_equal [simp]: "(0 = -a) = (0 = (a::'a::ab_group_add))"
1.173 +by (subst neg_equal_iff_equal [symmetric], simp)
1.174 +
1.175 +text{*The next two equations can make the simplifier loop!*}
1.176 +
1.177 +lemma equation_minus_iff: "(a = - b) = (b = - (a::'a::ab_group_add))"
1.178 +proof -
1.179 + have "(- (-a) = - b) = (- a = b)" by (rule neg_equal_iff_equal)
1.180 + thus ?thesis by (simp add: eq_commute)
1.181 +qed
1.182 +
1.183 +lemma minus_equation_iff: "(- a = b) = (- (b::'a::ab_group_add) = a)"
1.184 +proof -
1.185 + have "(- a = - (-b)) = (a = -b)" by (rule neg_equal_iff_equal)
1.186 + thus ?thesis by (simp add: eq_commute)
1.187 +qed
1.188 +
1.189 +lemma minus_add_distrib [simp]: "- (a + b) = -a + -(b::'a::ab_group_add)"
1.190 +apply (rule equals_zero_I)
1.191 +apply (simp add: add_ac)
1.192 +done
1.193 +
1.194 +lemma minus_diff_eq [simp]: "- (a - b) = b - (a::'a::ab_group_add)"
1.195 +by (simp add: diff_minus add_commute)
1.196 +
1.197 +subsection {* (Partially) Ordered Groups *}
1.198 +
1.199 +axclass pordered_ab_semigroup_add \<subseteq> order, ab_semigroup_add
1.200 + add_left_mono: "a \<le> b \<Longrightarrow> c + a \<le> c + b"
1.201 +
1.202 +axclass pordered_cancel_ab_semigroup_add \<subseteq> pordered_ab_semigroup_add, cancel_ab_semigroup_add
1.203 +
1.204 +instance pordered_cancel_ab_semigroup_add \<subseteq> pordered_ab_semigroup_add ..
1.205 +
1.206 +axclass pordered_ab_semigroup_add_imp_le \<subseteq> pordered_cancel_ab_semigroup_add
1.207 + add_le_imp_le_left: "c + a \<le> c + b \<Longrightarrow> a \<le> b"
1.208 +
1.209 +axclass pordered_ab_group_add \<subseteq> ab_group_add, pordered_ab_semigroup_add
1.210 +
1.211 +instance pordered_ab_group_add \<subseteq> pordered_ab_semigroup_add_imp_le
1.212 +proof
1.213 + fix a b c :: 'a
1.214 + assume "c + a \<le> c + b"
1.215 + hence "(-c) + (c + a) \<le> (-c) + (c + b)" by (rule add_left_mono)
1.216 + hence "((-c) + c) + a \<le> ((-c) + c) + b" by (simp only: add_assoc)
1.217 + thus "a \<le> b" by simp
1.218 +qed
1.219 +
1.220 +axclass ordered_cancel_ab_semigroup_add \<subseteq> pordered_cancel_ab_semigroup_add, linorder
1.221 +
1.222 +instance ordered_cancel_ab_semigroup_add \<subseteq> pordered_ab_semigroup_add_imp_le
1.223 +proof
1.224 + fix a b c :: 'a
1.225 + assume le: "c + a <= c + b"
1.226 + show "a <= b"
1.227 + proof (rule ccontr)
1.228 + assume w: "~ a \<le> b"
1.229 + hence "b <= a" by (simp add: linorder_not_le)
1.230 + hence le2: "c+b <= c+a" by (rule add_left_mono)
1.231 + have "a = b"
1.232 + apply (insert le)
1.233 + apply (insert le2)
1.234 + apply (drule order_antisym, simp_all)
1.235 + done
1.236 + with w show False
1.237 + by (simp add: linorder_not_le [symmetric])
1.238 + qed
1.239 +qed
1.240 +
1.241 +lemma add_right_mono: "a \<le> (b::'a::pordered_ab_semigroup_add) ==> a + c \<le> b + c"
1.242 +by (simp add: add_commute[of _ c] add_left_mono)
1.243 +
1.244 +text {* non-strict, in both arguments *}
1.245 +lemma add_mono:
1.246 + "[|a \<le> b; c \<le> d|] ==> a + c \<le> b + (d::'a::pordered_ab_semigroup_add)"
1.247 + apply (erule add_right_mono [THEN order_trans])
1.248 + apply (simp add: add_commute add_left_mono)
1.249 + done
1.250 +
1.251 +lemma add_strict_left_mono:
1.252 + "a < b ==> c + a < c + (b::'a::pordered_cancel_ab_semigroup_add)"
1.253 + by (simp add: order_less_le add_left_mono)
1.254 +
1.255 +lemma add_strict_right_mono:
1.256 + "a < b ==> a + c < b + (c::'a::pordered_cancel_ab_semigroup_add)"
1.257 + by (simp add: add_commute [of _ c] add_strict_left_mono)
1.258 +
1.259 +text{*Strict monotonicity in both arguments*}
1.260 +lemma add_strict_mono: "[|a<b; c<d|] ==> a + c < b + (d::'a::pordered_cancel_ab_semigroup_add)"
1.261 +apply (erule add_strict_right_mono [THEN order_less_trans])
1.262 +apply (erule add_strict_left_mono)
1.263 +done
1.264 +
1.265 +lemma add_less_le_mono:
1.266 + "[| a<b; c\<le>d |] ==> a + c < b + (d::'a::pordered_cancel_ab_semigroup_add)"
1.267 +apply (erule add_strict_right_mono [THEN order_less_le_trans])
1.268 +apply (erule add_left_mono)
1.269 +done
1.270 +
1.271 +lemma add_le_less_mono:
1.272 + "[| a\<le>b; c<d |] ==> a + c < b + (d::'a::pordered_cancel_ab_semigroup_add)"
1.273 +apply (erule add_right_mono [THEN order_le_less_trans])
1.274 +apply (erule add_strict_left_mono)
1.275 +done
1.276 +
1.277 +lemma add_less_imp_less_left:
1.278 + assumes less: "c + a < c + b" shows "a < (b::'a::pordered_ab_semigroup_add_imp_le)"
1.279 +proof -
1.280 + from less have le: "c + a <= c + b" by (simp add: order_le_less)
1.281 + have "a <= b"
1.282 + apply (insert le)
1.283 + apply (drule add_le_imp_le_left)
1.284 + by (insert le, drule add_le_imp_le_left, assumption)
1.285 + moreover have "a \<noteq> b"
1.286 + proof (rule ccontr)
1.287 + assume "~(a \<noteq> b)"
1.288 + then have "a = b" by simp
1.289 + then have "c + a = c + b" by simp
1.290 + with less show "False"by simp
1.291 + qed
1.292 + ultimately show "a < b" by (simp add: order_le_less)
1.293 +qed
1.294 +
1.295 +lemma add_less_imp_less_right:
1.296 + "a + c < b + c ==> a < (b::'a::pordered_ab_semigroup_add_imp_le)"
1.297 +apply (rule add_less_imp_less_left [of c])
1.298 +apply (simp add: add_commute)
1.299 +done
1.300 +
1.301 +lemma add_less_cancel_left [simp]:
1.302 + "(c+a < c+b) = (a < (b::'a::pordered_ab_semigroup_add_imp_le))"
1.303 +by (blast intro: add_less_imp_less_left add_strict_left_mono)
1.304 +
1.305 +lemma add_less_cancel_right [simp]:
1.306 + "(a+c < b+c) = (a < (b::'a::pordered_ab_semigroup_add_imp_le))"
1.307 +by (blast intro: add_less_imp_less_right add_strict_right_mono)
1.308 +
1.309 +lemma add_le_cancel_left [simp]:
1.310 + "(c+a \<le> c+b) = (a \<le> (b::'a::pordered_ab_semigroup_add_imp_le))"
1.311 +by (auto, drule add_le_imp_le_left, simp_all add: add_left_mono)
1.312 +
1.313 +lemma add_le_cancel_right [simp]:
1.314 + "(a+c \<le> b+c) = (a \<le> (b::'a::pordered_ab_semigroup_add_imp_le))"
1.315 +by (simp add: add_commute[of a c] add_commute[of b c])
1.316 +
1.317 +lemma add_le_imp_le_right:
1.318 + "a + c \<le> b + c ==> a \<le> (b::'a::pordered_ab_semigroup_add_imp_le)"
1.319 +by simp
1.320 +
1.321 +lemma add_increasing: "[|0\<le>a; b\<le>c|] ==> b \<le> a + (c::'a::{pordered_ab_semigroup_add_imp_le, comm_monoid_add})"
1.322 +by (insert add_mono [of 0 a b c], simp)
1.323 +
1.324 +subsection {* Ordering Rules for Unary Minus *}
1.325 +
1.326 +lemma le_imp_neg_le:
1.327 + assumes "a \<le> (b::'a::{pordered_ab_semigroup_add_imp_le, ab_group_add})" shows "-b \<le> -a"
1.328 +proof -
1.329 + have "-a+a \<le> -a+b"
1.330 + by (rule add_left_mono)
1.331 + hence "0 \<le> -a+b"
1.332 + by simp
1.333 + hence "0 + (-b) \<le> (-a + b) + (-b)"
1.334 + by (rule add_right_mono)
1.335 + thus ?thesis
1.336 + by (simp add: add_assoc)
1.337 +qed
1.338 +
1.339 +lemma neg_le_iff_le [simp]: "(-b \<le> -a) = (a \<le> (b::'a::pordered_ab_group_add))"
1.340 +proof
1.341 + assume "- b \<le> - a"
1.342 + hence "- (- a) \<le> - (- b)"
1.343 + by (rule le_imp_neg_le)
1.344 + thus "a\<le>b" by simp
1.345 +next
1.346 + assume "a\<le>b"
1.347 + thus "-b \<le> -a" by (rule le_imp_neg_le)
1.348 +qed
1.349 +
1.350 +lemma neg_le_0_iff_le [simp]: "(-a \<le> 0) = (0 \<le> (a::'a::pordered_ab_group_add))"
1.351 +by (subst neg_le_iff_le [symmetric], simp)
1.352 +
1.353 +lemma neg_0_le_iff_le [simp]: "(0 \<le> -a) = (a \<le> (0::'a::pordered_ab_group_add))"
1.354 +by (subst neg_le_iff_le [symmetric], simp)
1.355 +
1.356 +lemma neg_less_iff_less [simp]: "(-b < -a) = (a < (b::'a::pordered_ab_group_add))"
1.357 +by (force simp add: order_less_le)
1.358 +
1.359 +lemma neg_less_0_iff_less [simp]: "(-a < 0) = (0 < (a::'a::pordered_ab_group_add))"
1.360 +by (subst neg_less_iff_less [symmetric], simp)
1.361 +
1.362 +lemma neg_0_less_iff_less [simp]: "(0 < -a) = (a < (0::'a::pordered_ab_group_add))"
1.363 +by (subst neg_less_iff_less [symmetric], simp)
1.364 +
1.365 +text{*The next several equations can make the simplifier loop!*}
1.366 +
1.367 +lemma less_minus_iff: "(a < - b) = (b < - (a::'a::pordered_ab_group_add))"
1.368 +proof -
1.369 + have "(- (-a) < - b) = (b < - a)" by (rule neg_less_iff_less)
1.370 + thus ?thesis by simp
1.371 +qed
1.372 +
1.373 +lemma minus_less_iff: "(- a < b) = (- b < (a::'a::pordered_ab_group_add))"
1.374 +proof -
1.375 + have "(- a < - (-b)) = (- b < a)" by (rule neg_less_iff_less)
1.376 + thus ?thesis by simp
1.377 +qed
1.378 +
1.379 +lemma le_minus_iff: "(a \<le> - b) = (b \<le> - (a::'a::pordered_ab_group_add))"
1.380 +proof -
1.381 + have mm: "!! a (b::'a). (-(-a)) < -b \<Longrightarrow> -(-b) < -a" by (simp only: minus_less_iff)
1.382 + have "(- (- a) <= -b) = (b <= - a)"
1.383 + apply (auto simp only: order_le_less)
1.384 + apply (drule mm)
1.385 + apply (simp_all)
1.386 + apply (drule mm[simplified], assumption)
1.387 + done
1.388 + then show ?thesis by simp
1.389 +qed
1.390 +
1.391 +lemma minus_le_iff: "(- a \<le> b) = (- b \<le> (a::'a::pordered_ab_group_add))"
1.392 +by (auto simp add: order_le_less minus_less_iff)
1.393 +
1.394 +lemma add_diff_eq: "a + (b - c) = (a + b) - (c::'a::ab_group_add)"
1.395 +by (simp add: diff_minus add_ac)
1.396 +
1.397 +lemma diff_add_eq: "(a - b) + c = (a + c) - (b::'a::ab_group_add)"
1.398 +by (simp add: diff_minus add_ac)
1.399 +
1.400 +lemma diff_eq_eq: "(a-b = c) = (a = c + (b::'a::ab_group_add))"
1.401 +by (auto simp add: diff_minus add_assoc)
1.402 +
1.403 +lemma eq_diff_eq: "(a = c-b) = (a + (b::'a::ab_group_add) = c)"
1.404 +by (auto simp add: diff_minus add_assoc)
1.405 +
1.406 +lemma diff_diff_eq: "(a - b) - c = a - (b + (c::'a::ab_group_add))"
1.407 +by (simp add: diff_minus add_ac)
1.408 +
1.409 +lemma diff_diff_eq2: "a - (b - c) = (a + c) - (b::'a::ab_group_add)"
1.410 +by (simp add: diff_minus add_ac)
1.411 +
1.412 +lemma diff_add_cancel: "a - b + b = (a::'a::ab_group_add)"
1.413 +by (simp add: diff_minus add_ac)
1.414 +
1.415 +lemma add_diff_cancel: "a + b - b = (a::'a::ab_group_add)"
1.416 +by (simp add: diff_minus add_ac)
1.417 +
1.418 +text{*Further subtraction laws for ordered rings*}
1.419 +
1.420 +lemma less_iff_diff_less_0: "(a < b) = (a - b < (0::'a::pordered_ab_group_add))"
1.421 +proof -
1.422 + have "(a < b) = (a + (- b) < b + (-b))"
1.423 + by (simp only: add_less_cancel_right)
1.424 + also have "... = (a - b < 0)" by (simp add: diff_minus)
1.425 + finally show ?thesis .
1.426 +qed
1.427 +
1.428 +lemma diff_less_eq: "(a-b < c) = (a < c + (b::'a::pordered_ab_group_add))"
1.429 +apply (subst less_iff_diff_less_0)
1.430 +apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst])
1.431 +apply (simp add: diff_minus add_ac)
1.432 +done
1.433 +
1.434 +lemma less_diff_eq: "(a < c-b) = (a + (b::'a::pordered_ab_group_add) < c)"
1.435 +apply (subst less_iff_diff_less_0)
1.436 +apply (rule less_iff_diff_less_0 [of _ "c-b", THEN ssubst])
1.437 +apply (simp add: diff_minus add_ac)
1.438 +done
1.439 +
1.440 +lemma diff_le_eq: "(a-b \<le> c) = (a \<le> c + (b::'a::pordered_ab_group_add))"
1.441 +by (auto simp add: order_le_less diff_less_eq diff_add_cancel add_diff_cancel)
1.442 +
1.443 +lemma le_diff_eq: "(a \<le> c-b) = (a + (b::'a::pordered_ab_group_add) \<le> c)"
1.444 +by (auto simp add: order_le_less less_diff_eq diff_add_cancel add_diff_cancel)
1.445 +
1.446 +text{*This list of rewrites simplifies (in)equalities by bringing subtractions
1.447 + to the top and then moving negative terms to the other side.
1.448 + Use with @{text add_ac}*}
1.449 +lemmas compare_rls =
1.450 + diff_minus [symmetric]
1.451 + add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2
1.452 + diff_less_eq less_diff_eq diff_le_eq le_diff_eq
1.453 + diff_eq_eq eq_diff_eq
1.454 +
1.455 +
1.456 +subsection{*Lemmas for the @{text cancel_numerals} simproc*}
1.457 +
1.458 +lemma eq_iff_diff_eq_0: "(a = b) = (a-b = (0::'a::ab_group_add))"
1.459 +by (simp add: compare_rls)
1.460 +
1.461 +lemma le_iff_diff_le_0: "(a \<le> b) = (a-b \<le> (0::'a::pordered_ab_group_add))"
1.462 +by (simp add: compare_rls)
1.463 +
1.464 +subsection {* Lattice Ordered (Abelian) Groups *}
1.465 +
1.466 +axclass lordered_ab_group_meet < pordered_ab_group_add, meet_semilorder
1.467 +
1.468 +axclass lordered_ab_group_join < pordered_ab_group_add, join_semilorder
1.469 +
1.470 +lemma add_meet_distrib_left: "a + (meet b c) = meet (a + b) (a + (c::'a::{pordered_ab_group_add, meet_semilorder}))"
1.471 +apply (rule order_antisym)
1.472 +apply (rule meet_imp_le, simp_all add: meet_join_le)
1.473 +apply (rule add_le_imp_le_left [of "-a"])
1.474 +apply (simp only: add_assoc[symmetric], simp)
1.475 +apply (rule meet_imp_le)
1.476 +apply (rule add_le_imp_le_left[of "a"], simp only: add_assoc[symmetric], simp add: meet_join_le)+
1.477 +done
1.478 +
1.479 +lemma add_join_distrib_left: "a + (join b c) = join (a + b) (a+ (c::'a::{pordered_ab_group_add, join_semilorder}))"
1.480 +apply (rule order_antisym)
1.481 +apply (rule add_le_imp_le_left [of "-a"])
1.482 +apply (simp only: add_assoc[symmetric], simp)
1.483 +apply (rule join_imp_le)
1.484 +apply (rule add_le_imp_le_left [of "a"], simp only: add_assoc[symmetric], simp add: meet_join_le)+
1.485 +apply (rule join_imp_le)
1.486 +apply (simp_all add: meet_join_le)
1.487 +done
1.488 +
1.489 +lemma is_join_neg_meet: "is_join (% (a::'a::{pordered_ab_group_add, meet_semilorder}) b. - (meet (-a) (-b)))"
1.490 +apply (auto simp add: is_join_def)
1.491 +apply (rule_tac c="meet (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_meet_distrib_left meet_join_le)
1.492 +apply (rule_tac c="meet (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_meet_distrib_left meet_join_le)
1.493 +apply (subst neg_le_iff_le[symmetric])
1.494 +apply (simp add: meet_imp_le)
1.495 +done
1.496 +
1.497 +lemma is_meet_neg_join: "is_meet (% (a::'a::{pordered_ab_group_add, join_semilorder}) b. - (join (-a) (-b)))"
1.498 +apply (auto simp add: is_meet_def)
1.499 +apply (rule_tac c="join (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_join_distrib_left meet_join_le)
1.500 +apply (rule_tac c="join (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_join_distrib_left meet_join_le)
1.501 +apply (subst neg_le_iff_le[symmetric])
1.502 +apply (simp add: join_imp_le)
1.503 +done
1.504 +
1.505 +axclass lordered_ab_group \<subseteq> pordered_ab_group_add, lorder
1.506 +
1.507 +instance lordered_ab_group_meet \<subseteq> lordered_ab_group
1.508 +proof
1.509 + show "? j. is_join (j::'a\<Rightarrow>'a\<Rightarrow>('a::lordered_ab_group_meet))" by (blast intro: is_join_neg_meet)
1.510 +qed
1.511 +
1.512 +instance lordered_ab_group_join \<subseteq> lordered_ab_group
1.513 +proof
1.514 + show "? m. is_meet (m::'a\<Rightarrow>'a\<Rightarrow>('a::lordered_ab_group_join))" by (blast intro: is_meet_neg_join)
1.515 +qed
1.516 +
1.517 +lemma add_join_distrib_right: "(join a b) + (c::'a::lordered_ab_group) = join (a+c) (b+c)"
1.518 +proof -
1.519 + have "c + (join a b) = join (c+a) (c+b)" by (simp add: add_join_distrib_left)
1.520 + thus ?thesis by (simp add: add_commute)
1.521 +qed
1.522 +
1.523 +lemma add_meet_distrib_right: "(meet a b) + (c::'a::lordered_ab_group) = meet (a+c) (b+c)"
1.524 +proof -
1.525 + have "c + (meet a b) = meet (c+a) (c+b)" by (simp add: add_meet_distrib_left)
1.526 + thus ?thesis by (simp add: add_commute)
1.527 +qed
1.528 +
1.529 +lemmas add_meet_join_distribs = add_meet_distrib_right add_meet_distrib_left add_join_distrib_right add_join_distrib_left
1.530 +
1.531 +lemma join_eq_neg_meet: "join a (b::'a::lordered_ab_group) = - meet (-a) (-b)"
1.532 +by (simp add: is_join_unique[OF is_join_join is_join_neg_meet])
1.533 +
1.534 +lemma meet_eq_neg_join: "meet a (b::'a::lordered_ab_group) = - join (-a) (-b)"
1.535 +by (simp add: is_meet_unique[OF is_meet_meet is_meet_neg_join])
1.536 +
1.537 +lemma add_eq_meet_join: "a + b = (join a b) + (meet a (b::'a::lordered_ab_group))"
1.538 +proof -
1.539 + have "0 = - meet 0 (a-b) + meet (a-b) 0" by (simp add: meet_comm)
1.540 + hence "0 = join 0 (b-a) + meet (a-b) 0" by (simp add: meet_eq_neg_join)
1.541 + hence "0 = (-a + join a b) + (meet a b + (-b))"
1.542 + apply (simp add: add_join_distrib_left add_meet_distrib_right)
1.543 + by (simp add: diff_minus add_commute)
1.544 + thus ?thesis
1.545 + apply (simp add: compare_rls)
1.546 + apply (subst add_left_cancel[symmetric, of "a+b" "join a b + meet a b" "-a"])
1.547 + apply (simp only: add_assoc, simp add: add_assoc[symmetric])
1.548 + done
1.549 +qed
1.550 +
1.551 +subsection {* Positive Part, Negative Part, Absolute Value *}
1.552 +
1.553 +constdefs
1.554 + pprt :: "'a \<Rightarrow> ('a::lordered_ab_group)"
1.555 + "pprt x == join x 0"
1.556 + nprt :: "'a \<Rightarrow> ('a::lordered_ab_group)"
1.557 + "nprt x == meet x 0"
1.558 +
1.559 +lemma prts: "a = pprt a + nprt a"
1.560 +by (simp add: pprt_def nprt_def add_eq_meet_join[symmetric])
1.561 +
1.562 +lemma zero_le_pprt[simp]: "0 \<le> pprt a"
1.563 +by (simp add: pprt_def meet_join_le)
1.564 +
1.565 +lemma nprt_le_zero[simp]: "nprt a \<le> 0"
1.566 +by (simp add: nprt_def meet_join_le)
1.567 +
1.568 +lemma le_eq_neg: "(a \<le> -b) = (a + b \<le> (0::_::lordered_ab_group))" (is "?l = ?r")
1.569 +proof -
1.570 + have a: "?l \<longrightarrow> ?r"
1.571 + apply (auto)
1.572 + apply (rule add_le_imp_le_right[of _ "-b" _])
1.573 + apply (simp add: add_assoc)
1.574 + done
1.575 + have b: "?r \<longrightarrow> ?l"
1.576 + apply (auto)
1.577 + apply (rule add_le_imp_le_right[of _ "b" _])
1.578 + apply (simp)
1.579 + done
1.580 + from a b show ?thesis by blast
1.581 +qed
1.582 +
1.583 +lemma join_0_imp_0: "join a (-a) = 0 \<Longrightarrow> a = (0::'a::lordered_ab_group)"
1.584 +proof -
1.585 + {
1.586 + fix a::'a
1.587 + assume hyp: "join a (-a) = 0"
1.588 + hence "join a (-a) + a = a" by (simp)
1.589 + hence "join (a+a) 0 = a" by (simp add: add_join_distrib_right)
1.590 + hence "join (a+a) 0 <= a" by (simp)
1.591 + hence "0 <= a" by (blast intro: order_trans meet_join_le)
1.592 + }
1.593 + note p = this
1.594 + thm p
1.595 + assume hyp:"join a (-a) = 0"
1.596 + hence hyp2:"join (-a) (-(-a)) = 0" by (simp add: join_comm)
1.597 + from p[OF hyp] p[OF hyp2] show "a = 0" by simp
1.598 +qed
1.599 +
1.600 +lemma meet_0_imp_0: "meet a (-a) = 0 \<Longrightarrow> a = (0::'a::lordered_ab_group)"
1.601 +apply (simp add: meet_eq_neg_join)
1.602 +apply (simp add: join_comm)
1.603 +apply (subst join_0_imp_0)
1.604 +by auto
1.605 +
1.606 +lemma join_0_eq_0[simp]: "(join a (-a) = 0) = (a = (0::'a::lordered_ab_group))"
1.607 +by (auto, erule join_0_imp_0)
1.608 +
1.609 +lemma meet_0_eq_0[simp]: "(meet a (-a) = 0) = (a = (0::'a::lordered_ab_group))"
1.610 +by (auto, erule meet_0_imp_0)
1.611 +
1.612 +lemma zero_le_double_add_iff_zero_le_single_add[simp]: "(0 \<le> a + a) = (0 \<le> (a::'a::lordered_ab_group))"
1.613 +proof
1.614 + assume "0 <= a + a"
1.615 + hence a:"meet (a+a) 0 = 0" by (simp add: le_def_meet meet_comm)
1.616 + have "(meet a 0)+(meet a 0) = meet (meet (a+a) 0) a" (is "?l=_") by (simp add: add_meet_join_distribs meet_aci)
1.617 + hence "?l = 0 + meet a 0" by (simp add: a, simp add: meet_comm)
1.618 + hence "meet a 0 = 0" by (simp only: add_right_cancel)
1.619 + then show "0 <= a" by (simp add: le_def_meet meet_comm)
1.620 +next
1.621 + assume a: "0 <= a"
1.622 + show "0 <= a + a" by (simp add: add_mono[OF a a, simplified])
1.623 +qed
1.624 +
1.625 +lemma double_add_le_zero_iff_single_add_le_zero[simp]: "(a + a <= 0) = ((a::'a::lordered_ab_group) <= 0)"
1.626 +proof -
1.627 + have "(a + a <= 0) = (0 <= -(a+a))" by (subst le_minus_iff, simp)
1.628 + moreover have "\<dots> = (a <= 0)" by (simp add: zero_le_double_add_iff_zero_le_single_add)
1.629 + ultimately show ?thesis by blast
1.630 +qed
1.631 +
1.632 +lemma double_add_less_zero_iff_single_less_zero[simp]: "(a+a<0) = ((a::'a::{pordered_ab_group_add,linorder}) < 0)" (is ?s)
1.633 +proof cases
1.634 + assume a: "a < 0"
1.635 + thus ?s by (simp add: add_strict_mono[OF a a, simplified])
1.636 +next
1.637 + assume "~(a < 0)"
1.638 + hence a:"0 <= a" by (simp)
1.639 + hence "0 <= a+a" by (simp add: add_mono[OF a a, simplified])
1.640 + hence "~(a+a < 0)" by simp
1.641 + with a show ?thesis by simp
1.642 +qed
1.643 +
1.644 +axclass lordered_ab_group_abs \<subseteq> lordered_ab_group
1.645 + abs_lattice: "abs x = join x (-x)"
1.646 +
1.647 +lemma abs_zero[simp]: "abs 0 = (0::'a::lordered_ab_group_abs)"
1.648 +by (simp add: abs_lattice)
1.649 +
1.650 +lemma abs_eq_0[simp]: "(abs a = 0) = (a = (0::'a::lordered_ab_group_abs))"
1.651 +by (simp add: abs_lattice)
1.652 +
1.653 +lemma abs_0_eq[simp]: "(0 = abs a) = (a = (0::'a::lordered_ab_group_abs))"
1.654 +proof -
1.655 + have "(0 = abs a) = (abs a = 0)" by (simp only: eq_ac)
1.656 + thus ?thesis by simp
1.657 +qed
1.658 +
1.659 +lemma neg_meet_eq_join[simp]: "- meet a (b::_::lordered_ab_group) = join (-a) (-b)"
1.660 +by (simp add: meet_eq_neg_join)
1.661 +
1.662 +lemma neg_join_eq_meet[simp]: "- join a (b::_::lordered_ab_group) = meet (-a) (-b)"
1.663 +by (simp del: neg_meet_eq_join add: join_eq_neg_meet)
1.664 +
1.665 +lemma join_eq_if: "join a (-a) = (if a < 0 then -a else (a::'a::{lordered_ab_group, linorder}))"
1.666 +proof -
1.667 + note b = add_le_cancel_right[of a a "-a",symmetric,simplified]
1.668 + have c: "a + a = 0 \<Longrightarrow> -a = a" by (rule add_right_imp_eq[of _ a], simp)
1.669 + show ?thesis
1.670 + apply (auto simp add: join_max max_def b linorder_not_less)
1.671 + apply (drule order_antisym, auto)
1.672 + done
1.673 +qed
1.674 +
1.675 +lemma abs_if_lattice: "\<bar>a\<bar> = (if a < 0 then -a else (a::'a::{lordered_ab_group_abs, linorder}))"
1.676 +proof -
1.677 + show ?thesis by (simp add: abs_lattice join_eq_if)
1.678 +qed
1.679 +
1.680 +lemma abs_ge_zero[simp]: "0 \<le> abs (a::'a::lordered_ab_group_abs)"
1.681 +proof -
1.682 + have a:"a <= abs a" and b:"-a <= abs a" by (auto simp add: abs_lattice meet_join_le)
1.683 + show ?thesis by (rule add_mono[OF a b, simplified])
1.684 +qed
1.685 +
1.686 +lemma abs_le_zero_iff [simp]: "(abs a \<le> (0::'a::lordered_ab_group_abs)) = (a = 0)"
1.687 +proof
1.688 + assume "abs a <= 0"
1.689 + hence "abs a = 0" by (auto dest: order_antisym)
1.690 + thus "a = 0" by simp
1.691 +next
1.692 + assume "a = 0"
1.693 + thus "abs a <= 0" by simp
1.694 +qed
1.695 +
1.696 +lemma zero_less_abs_iff [simp]: "(0 < abs a) = (a \<noteq> (0::'a::lordered_ab_group_abs))"
1.697 +by (simp add: order_less_le)
1.698 +
1.699 +lemma abs_not_less_zero [simp]: "~ abs a < (0::'a::lordered_ab_group_abs)"
1.700 +proof -
1.701 + have a:"!! x (y::_::order). x <= y \<Longrightarrow> ~(y < x)" by auto
1.702 + show ?thesis by (simp add: a)
1.703 +qed
1.704 +
1.705 +lemma abs_ge_self: "a \<le> abs (a::'a::lordered_ab_group_abs)"
1.706 +by (simp add: abs_lattice meet_join_le)
1.707 +
1.708 +lemma abs_ge_minus_self: "-a \<le> abs (a::'a::lordered_ab_group_abs)"
1.709 +by (simp add: abs_lattice meet_join_le)
1.710 +
1.711 +lemma le_imp_join_eq: "a \<le> b \<Longrightarrow> join a b = b"
1.712 +by (simp add: le_def_join)
1.713 +
1.714 +lemma ge_imp_join_eq: "b \<le> a \<Longrightarrow> join a b = a"
1.715 +by (simp add: le_def_join join_aci)
1.716 +
1.717 +lemma le_imp_meet_eq: "a \<le> b \<Longrightarrow> meet a b = a"
1.718 +by (simp add: le_def_meet)
1.719 +
1.720 +lemma ge_imp_meet_eq: "b \<le> a \<Longrightarrow> meet a b = b"
1.721 +by (simp add: le_def_meet meet_aci)
1.722 +
1.723 +lemma abs_prts: "abs (a::_::lordered_ab_group_abs) = pprt a - nprt a"
1.724 +apply (simp add: pprt_def nprt_def diff_minus)
1.725 +apply (simp add: add_meet_join_distribs join_aci abs_lattice[symmetric])
1.726 +apply (subst le_imp_join_eq, auto)
1.727 +done
1.728 +
1.729 +lemma abs_minus_cancel [simp]: "abs (-a) = abs(a::'a::lordered_ab_group_abs)"
1.730 +by (simp add: abs_lattice join_comm)
1.731 +
1.732 +lemma abs_idempotent [simp]: "abs (abs a) = abs (a::'a::lordered_ab_group_abs)"
1.733 +apply (simp add: abs_lattice[of "abs a"])
1.734 +apply (subst ge_imp_join_eq)
1.735 +apply (rule order_trans[of _ 0])
1.736 +by auto
1.737 +
1.738 +lemma zero_le_iff_zero_nprt: "(0 \<le> a) = (nprt a = 0)"
1.739 +by (simp add: le_def_meet nprt_def meet_comm)
1.740 +
1.741 +lemma le_zero_iff_zero_pprt: "(a \<le> 0) = (pprt a = 0)"
1.742 +by (simp add: le_def_join pprt_def join_comm)
1.743 +
1.744 +lemma le_zero_iff_pprt_id: "(0 \<le> a) = (pprt a = a)"
1.745 +by (simp add: le_def_join pprt_def join_comm)
1.746 +
1.747 +lemma zero_le_iff_nprt_id: "(a \<le> 0) = (nprt a = a)"
1.748 +by (simp add: le_def_meet nprt_def meet_comm)
1.749 +
1.750 +lemma iff2imp: "(A=B) \<Longrightarrow> (A \<Longrightarrow> B)"
1.751 +by (simp)
1.752 +
1.753 +lemma imp_abs_id: "0 \<le> a \<Longrightarrow> abs a = (a::'a::lordered_ab_group_abs)"
1.754 +by (simp add: iff2imp[OF zero_le_iff_zero_nprt] iff2imp[OF le_zero_iff_pprt_id] abs_prts)
1.755 +
1.756 +lemma imp_abs_neg_id: "a \<le> 0 \<Longrightarrow> abs a = -(a::'a::lordered_ab_group_abs)"
1.757 +by (simp add: iff2imp[OF le_zero_iff_zero_pprt] iff2imp[OF zero_le_iff_nprt_id] abs_prts)
1.758 +
1.759 +lemma abs_leI: "[|a \<le> b; -a \<le> b|] ==> abs a \<le> (b::'a::lordered_ab_group_abs)"
1.760 +by (simp add: abs_lattice join_imp_le)
1.761 +
1.762 +lemma le_minus_self_iff: "(a \<le> -a) = (a \<le> (0::'a::lordered_ab_group))"
1.763 +proof -
1.764 + from add_le_cancel_left[of "-a" "a+a" "0"] have "(a <= -a) = (a+a <= 0)"
1.765 + by (simp add: add_assoc[symmetric])
1.766 + thus ?thesis by simp
1.767 +qed
1.768 +
1.769 +lemma minus_le_self_iff: "(-a \<le> a) = (0 \<le> (a::'a::lordered_ab_group))"
1.770 +proof -
1.771 + from add_le_cancel_left[of "-a" "0" "a+a"] have "(-a <= a) = (0 <= a+a)"
1.772 + by (simp add: add_assoc[symmetric])
1.773 + thus ?thesis by simp
1.774 +qed
1.775 +
1.776 +lemma abs_le_D1: "abs a \<le> b ==> a \<le> (b::'a::lordered_ab_group_abs)"
1.777 +by (insert abs_ge_self, blast intro: order_trans)
1.778 +
1.779 +lemma abs_le_D2: "abs a \<le> b ==> -a \<le> (b::'a::lordered_ab_group_abs)"
1.780 +by (insert abs_le_D1 [of "-a"], simp)
1.781 +
1.782 +lemma abs_le_iff: "(abs a \<le> b) = (a \<le> b & -a \<le> (b::'a::lordered_ab_group_abs))"
1.783 +by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2)
1.784 +
1.785 +lemma abs_triangle_ineq: "abs (a+b) \<le> abs a + abs (b::'a::lordered_ab_group_abs)"
1.786 +proof -
1.787 + have g:"abs a + abs b = join (a+b) (join (-a-b) (join (-a+b) (a + (-b))))" (is "_=join ?m ?n")
1.788 + apply (simp add: abs_lattice add_meet_join_distribs join_aci)
1.789 + by (simp only: diff_minus)
1.790 + have a:"a+b <= join ?m ?n" by (simp add: meet_join_le)
1.791 + have b:"-a-b <= ?n" by (simp add: meet_join_le)
1.792 + have c:"?n <= join ?m ?n" by (simp add: meet_join_le)
1.793 + from b c have d: "-a-b <= join ?m ?n" by simp
1.794 + have e:"-a-b = -(a+b)" by (simp add: diff_minus)
1.795 + from a d e have "abs(a+b) <= join ?m ?n"
1.796 + by (drule_tac abs_leI, auto)
1.797 + with g[symmetric] show ?thesis by simp
1.798 +qed
1.799 +
1.800 +lemma abs_diff_triangle_ineq:
1.801 + "\<bar>(a::'a::lordered_ab_group_abs) + b - (c+d)\<bar> \<le> \<bar>a-c\<bar> + \<bar>b-d\<bar>"
1.802 +proof -
1.803 + have "\<bar>a + b - (c+d)\<bar> = \<bar>(a-c) + (b-d)\<bar>" by (simp add: diff_minus add_ac)
1.804 + also have "... \<le> \<bar>a-c\<bar> + \<bar>b-d\<bar>" by (rule abs_triangle_ineq)
1.805 + finally show ?thesis .
1.806 +qed
1.807 +
1.808 +ML {*
1.809 +val add_zero_left = thm"add_0";
1.810 +val add_zero_right = thm"add_0_right";
1.811 +*}
1.812 +
1.813 +ML {*
1.814 +val add_assoc = thm "add_assoc";
1.815 +val add_commute = thm "add_commute";
1.816 +val add_left_commute = thm "add_left_commute";
1.817 +val add_ac = thms "add_ac";
1.818 +val mult_assoc = thm "mult_assoc";
1.819 +val mult_commute = thm "mult_commute";
1.820 +val mult_left_commute = thm "mult_left_commute";
1.821 +val mult_ac = thms "mult_ac";
1.822 +val add_0 = thm "add_0";
1.823 +val mult_1_left = thm "mult_1_left";
1.824 +val mult_1_right = thm "mult_1_right";
1.825 +val mult_1 = thm "mult_1";
1.826 +val add_left_imp_eq = thm "add_left_imp_eq";
1.827 +val add_right_imp_eq = thm "add_right_imp_eq";
1.828 +val add_imp_eq = thm "add_imp_eq";
1.829 +val left_minus = thm "left_minus";
1.830 +val diff_minus = thm "diff_minus";
1.831 +val add_0_right = thm "add_0_right";
1.832 +val add_left_cancel = thm "add_left_cancel";
1.833 +val add_right_cancel = thm "add_right_cancel";
1.834 +val right_minus = thm "right_minus";
1.835 +val right_minus_eq = thm "right_minus_eq";
1.836 +val minus_minus = thm "minus_minus";
1.837 +val equals_zero_I = thm "equals_zero_I";
1.838 +val minus_zero = thm "minus_zero";
1.839 +val diff_self = thm "diff_self";
1.840 +val diff_0 = thm "diff_0";
1.841 +val diff_0_right = thm "diff_0_right";
1.842 +val diff_minus_eq_add = thm "diff_minus_eq_add";
1.843 +val neg_equal_iff_equal = thm "neg_equal_iff_equal";
1.844 +val neg_equal_0_iff_equal = thm "neg_equal_0_iff_equal";
1.845 +val neg_0_equal_iff_equal = thm "neg_0_equal_iff_equal";
1.846 +val equation_minus_iff = thm "equation_minus_iff";
1.847 +val minus_equation_iff = thm "minus_equation_iff";
1.848 +val minus_add_distrib = thm "minus_add_distrib";
1.849 +val minus_diff_eq = thm "minus_diff_eq";
1.850 +val add_left_mono = thm "add_left_mono";
1.851 +val add_le_imp_le_left = thm "add_le_imp_le_left";
1.852 +val add_right_mono = thm "add_right_mono";
1.853 +val add_mono = thm "add_mono";
1.854 +val add_strict_left_mono = thm "add_strict_left_mono";
1.855 +val add_strict_right_mono = thm "add_strict_right_mono";
1.856 +val add_strict_mono = thm "add_strict_mono";
1.857 +val add_less_le_mono = thm "add_less_le_mono";
1.858 +val add_le_less_mono = thm "add_le_less_mono";
1.859 +val add_less_imp_less_left = thm "add_less_imp_less_left";
1.860 +val add_less_imp_less_right = thm "add_less_imp_less_right";
1.861 +val add_less_cancel_left = thm "add_less_cancel_left";
1.862 +val add_less_cancel_right = thm "add_less_cancel_right";
1.863 +val add_le_cancel_left = thm "add_le_cancel_left";
1.864 +val add_le_cancel_right = thm "add_le_cancel_right";
1.865 +val add_le_imp_le_right = thm "add_le_imp_le_right";
1.866 +val add_increasing = thm "add_increasing";
1.867 +val le_imp_neg_le = thm "le_imp_neg_le";
1.868 +val neg_le_iff_le = thm "neg_le_iff_le";
1.869 +val neg_le_0_iff_le = thm "neg_le_0_iff_le";
1.870 +val neg_0_le_iff_le = thm "neg_0_le_iff_le";
1.871 +val neg_less_iff_less = thm "neg_less_iff_less";
1.872 +val neg_less_0_iff_less = thm "neg_less_0_iff_less";
1.873 +val neg_0_less_iff_less = thm "neg_0_less_iff_less";
1.874 +val less_minus_iff = thm "less_minus_iff";
1.875 +val minus_less_iff = thm "minus_less_iff";
1.876 +val le_minus_iff = thm "le_minus_iff";
1.877 +val minus_le_iff = thm "minus_le_iff";
1.878 +val add_diff_eq = thm "add_diff_eq";
1.879 +val diff_add_eq = thm "diff_add_eq";
1.880 +val diff_eq_eq = thm "diff_eq_eq";
1.881 +val eq_diff_eq = thm "eq_diff_eq";
1.882 +val diff_diff_eq = thm "diff_diff_eq";
1.883 +val diff_diff_eq2 = thm "diff_diff_eq2";
1.884 +val diff_add_cancel = thm "diff_add_cancel";
1.885 +val add_diff_cancel = thm "add_diff_cancel";
1.886 +val less_iff_diff_less_0 = thm "less_iff_diff_less_0";
1.887 +val diff_less_eq = thm "diff_less_eq";
1.888 +val less_diff_eq = thm "less_diff_eq";
1.889 +val diff_le_eq = thm "diff_le_eq";
1.890 +val le_diff_eq = thm "le_diff_eq";
1.891 +val compare_rls = thms "compare_rls";
1.892 +val eq_iff_diff_eq_0 = thm "eq_iff_diff_eq_0";
1.893 +val le_iff_diff_le_0 = thm "le_iff_diff_le_0";
1.894 +val add_meet_distrib_left = thm "add_meet_distrib_left";
1.895 +val add_join_distrib_left = thm "add_join_distrib_left";
1.896 +val is_join_neg_meet = thm "is_join_neg_meet";
1.897 +val is_meet_neg_join = thm "is_meet_neg_join";
1.898 +val add_join_distrib_right = thm "add_join_distrib_right";
1.899 +val add_meet_distrib_right = thm "add_meet_distrib_right";
1.900 +val add_meet_join_distribs = thms "add_meet_join_distribs";
1.901 +val join_eq_neg_meet = thm "join_eq_neg_meet";
1.902 +val meet_eq_neg_join = thm "meet_eq_neg_join";
1.903 +val add_eq_meet_join = thm "add_eq_meet_join";
1.904 +val prts = thm "prts";
1.905 +val zero_le_pprt = thm "zero_le_pprt";
1.906 +val nprt_le_zero = thm "nprt_le_zero";
1.907 +val le_eq_neg = thm "le_eq_neg";
1.908 +val join_0_imp_0 = thm "join_0_imp_0";
1.909 +val meet_0_imp_0 = thm "meet_0_imp_0";
1.910 +val join_0_eq_0 = thm "join_0_eq_0";
1.911 +val meet_0_eq_0 = thm "meet_0_eq_0";
1.912 +val zero_le_double_add_iff_zero_le_single_add = thm "zero_le_double_add_iff_zero_le_single_add";
1.913 +val double_add_le_zero_iff_single_add_le_zero = thm "double_add_le_zero_iff_single_add_le_zero";
1.914 +val double_add_less_zero_iff_single_less_zero = thm "double_add_less_zero_iff_single_less_zero";
1.915 +val abs_lattice = thm "abs_lattice";
1.916 +val abs_zero = thm "abs_zero";
1.917 +val abs_eq_0 = thm "abs_eq_0";
1.918 +val abs_0_eq = thm "abs_0_eq";
1.919 +val neg_meet_eq_join = thm "neg_meet_eq_join";
1.920 +val neg_join_eq_meet = thm "neg_join_eq_meet";
1.921 +val join_eq_if = thm "join_eq_if";
1.922 +val abs_if_lattice = thm "abs_if_lattice";
1.923 +val abs_ge_zero = thm "abs_ge_zero";
1.924 +val abs_le_zero_iff = thm "abs_le_zero_iff";
1.925 +val zero_less_abs_iff = thm "zero_less_abs_iff";
1.926 +val abs_not_less_zero = thm "abs_not_less_zero";
1.927 +val abs_ge_self = thm "abs_ge_self";
1.928 +val abs_ge_minus_self = thm "abs_ge_minus_self";
1.929 +val le_imp_join_eq = thm "le_imp_join_eq";
1.930 +val ge_imp_join_eq = thm "ge_imp_join_eq";
1.931 +val le_imp_meet_eq = thm "le_imp_meet_eq";
1.932 +val ge_imp_meet_eq = thm "ge_imp_meet_eq";
1.933 +val abs_prts = thm "abs_prts";
1.934 +val abs_minus_cancel = thm "abs_minus_cancel";
1.935 +val abs_idempotent = thm "abs_idempotent";
1.936 +val zero_le_iff_zero_nprt = thm "zero_le_iff_zero_nprt";
1.937 +val le_zero_iff_zero_pprt = thm "le_zero_iff_zero_pprt";
1.938 +val le_zero_iff_pprt_id = thm "le_zero_iff_pprt_id";
1.939 +val zero_le_iff_nprt_id = thm "zero_le_iff_nprt_id";
1.940 +val iff2imp = thm "iff2imp";
1.941 +val imp_abs_id = thm "imp_abs_id";
1.942 +val imp_abs_neg_id = thm "imp_abs_neg_id";
1.943 +val abs_leI = thm "abs_leI";
1.944 +val le_minus_self_iff = thm "le_minus_self_iff";
1.945 +val minus_le_self_iff = thm "minus_le_self_iff";
1.946 +val abs_le_D1 = thm "abs_le_D1";
1.947 +val abs_le_D2 = thm "abs_le_D2";
1.948 +val abs_le_iff = thm "abs_le_iff";
1.949 +val abs_triangle_ineq = thm "abs_triangle_ineq";
1.950 +val abs_diff_triangle_ineq = thm "abs_diff_triangle_ineq";
1.951 +*}
1.952 +
1.953 +end