src/HOL/OrderedGroup.thy
changeset 29667 53103fc8ffa3
parent 29269 5c25a2012975
child 29668 33ba3faeaa0e
     1.1 --- a/src/HOL/OrderedGroup.thy	Sun Jan 18 13:58:17 2009 +0100
     1.2 +++ b/src/HOL/OrderedGroup.thy	Wed Jan 28 16:29:16 2009 +0100
     1.3 @@ -22,17 +22,34 @@
     1.4    \end{itemize}
     1.5  *}
     1.6  
     1.7 +ML{*
     1.8 +structure AlgebraSimps =
     1.9 +  NamedThmsFun(val name = "algebra_simps"
    1.10 +               val description = "algebra simplification rules");
    1.11 +*}
    1.12 +
    1.13 +setup AlgebraSimps.setup
    1.14 +
    1.15 +text{* The rewrites accumulated in @{text algebra_simps} deal with the
    1.16 +classical algebraic structures of groups, rings and family. They simplify
    1.17 +terms by multiplying everything out (in case of a ring) and bringing sums and
    1.18 +products into a canonical form (by ordered rewriting). As a result it decides
    1.19 +group and ring equalities but also helps with inequalities.
    1.20 +
    1.21 +Of course it also works for fields, but it knows nothing about multiplicative
    1.22 +inverses or division. This is catered for by @{text field_simps}. *}
    1.23 +
    1.24  subsection {* Semigroups and Monoids *}
    1.25  
    1.26  class semigroup_add = plus +
    1.27 -  assumes add_assoc: "(a + b) + c = a + (b + c)"
    1.28 +  assumes add_assoc[algebra_simps]: "(a + b) + c = a + (b + c)"
    1.29  
    1.30  class ab_semigroup_add = semigroup_add +
    1.31 -  assumes add_commute: "a + b = b + a"
    1.32 +  assumes add_commute[algebra_simps]: "a + b = b + a"
    1.33  begin
    1.34  
    1.35 -lemma add_left_commute: "a + (b + c) = b + (a + c)"
    1.36 -  by (rule mk_left_commute [of "plus", OF add_assoc add_commute])
    1.37 +lemma add_left_commute[algebra_simps]: "a + (b + c) = b + (a + c)"
    1.38 +by (rule mk_left_commute [of "plus", OF add_assoc add_commute])
    1.39  
    1.40  theorems add_ac = add_assoc add_commute add_left_commute
    1.41  
    1.42 @@ -41,14 +58,14 @@
    1.43  theorems add_ac = add_assoc add_commute add_left_commute
    1.44  
    1.45  class semigroup_mult = times +
    1.46 -  assumes mult_assoc: "(a * b) * c = a * (b * c)"
    1.47 +  assumes mult_assoc[algebra_simps]: "(a * b) * c = a * (b * c)"
    1.48  
    1.49  class ab_semigroup_mult = semigroup_mult +
    1.50 -  assumes mult_commute: "a * b = b * a"
    1.51 +  assumes mult_commute[algebra_simps]: "a * b = b * a"
    1.52  begin
    1.53  
    1.54 -lemma mult_left_commute: "a * (b * c) = b * (a * c)"
    1.55 -  by (rule mk_left_commute [of "times", OF mult_assoc mult_commute])
    1.56 +lemma mult_left_commute[algebra_simps]: "a * (b * c) = b * (a * c)"
    1.57 +by (rule mk_left_commute [of "times", OF mult_assoc mult_commute])
    1.58  
    1.59  theorems mult_ac = mult_assoc mult_commute mult_left_commute
    1.60  
    1.61 @@ -57,24 +74,20 @@
    1.62  theorems mult_ac = mult_assoc mult_commute mult_left_commute
    1.63  
    1.64  class ab_semigroup_idem_mult = ab_semigroup_mult +
    1.65 -  assumes mult_idem: "x * x = x"
    1.66 +  assumes mult_idem[simp]: "x * x = x"
    1.67  begin
    1.68  
    1.69 -lemma mult_left_idem: "x * (x * y) = x * y"
    1.70 +lemma mult_left_idem[simp]: "x * (x * y) = x * y"
    1.71    unfolding mult_assoc [symmetric, of x] mult_idem ..
    1.72  
    1.73 -lemmas mult_ac_idem = mult_ac mult_idem mult_left_idem
    1.74 -
    1.75  end
    1.76  
    1.77 -lemmas mult_ac_idem = mult_ac mult_idem mult_left_idem
    1.78 -
    1.79  class monoid_add = zero + semigroup_add +
    1.80    assumes add_0_left [simp]: "0 + a = a"
    1.81      and add_0_right [simp]: "a + 0 = a"
    1.82  
    1.83  lemma zero_reorient: "0 = x \<longleftrightarrow> x = 0"
    1.84 -  by (rule eq_commute)
    1.85 +by (rule eq_commute)
    1.86  
    1.87  class comm_monoid_add = zero + ab_semigroup_add +
    1.88    assumes add_0: "0 + a = a"
    1.89 @@ -90,7 +103,7 @@
    1.90    assumes mult_1_right [simp]: "a * 1 = a"
    1.91  
    1.92  lemma one_reorient: "1 = x \<longleftrightarrow> x = 1"
    1.93 -  by (rule eq_commute)
    1.94 +by (rule eq_commute)
    1.95  
    1.96  class comm_monoid_mult = one + ab_semigroup_mult +
    1.97    assumes mult_1: "1 * a = a"
    1.98 @@ -108,11 +121,11 @@
    1.99  
   1.100  lemma add_left_cancel [simp]:
   1.101    "a + b = a + c \<longleftrightarrow> b = c"
   1.102 -  by (blast dest: add_left_imp_eq)
   1.103 +by (blast dest: add_left_imp_eq)
   1.104  
   1.105  lemma add_right_cancel [simp]:
   1.106    "b + a = c + a \<longleftrightarrow> b = c"
   1.107 -  by (blast dest: add_right_imp_eq)
   1.108 +by (blast dest: add_right_imp_eq)
   1.109  
   1.110  end
   1.111  
   1.112 @@ -142,7 +155,7 @@
   1.113  begin
   1.114  
   1.115  lemma minus_add_cancel: "- a + (a + b) = b"
   1.116 -  by (simp add: add_assoc[symmetric])
   1.117 +by (simp add: add_assoc[symmetric])
   1.118  
   1.119  lemma minus_zero [simp]: "- 0 = 0"
   1.120  proof -
   1.121 @@ -176,8 +189,7 @@
   1.122  qed
   1.123  
   1.124  lemma equals_zero_I:
   1.125 -  assumes "a + b = 0"
   1.126 -  shows "- a = b"
   1.127 +  assumes "a + b = 0" shows "- a = b"
   1.128  proof -
   1.129    have "- a = - a + (a + b)" using assms by simp
   1.130    also have "\<dots> = b" by (simp add: add_assoc[symmetric])
   1.131 @@ -185,23 +197,22 @@
   1.132  qed
   1.133  
   1.134  lemma diff_self [simp]: "a - a = 0"
   1.135 -  by (simp add: diff_minus)
   1.136 +by (simp add: diff_minus)
   1.137  
   1.138  lemma diff_0 [simp]: "0 - a = - a"
   1.139 -  by (simp add: diff_minus)
   1.140 +by (simp add: diff_minus)
   1.141  
   1.142  lemma diff_0_right [simp]: "a - 0 = a" 
   1.143 -  by (simp add: diff_minus)
   1.144 +by (simp add: diff_minus)
   1.145  
   1.146  lemma diff_minus_eq_add [simp]: "a - - b = a + b"
   1.147 -  by (simp add: diff_minus)
   1.148 +by (simp add: diff_minus)
   1.149  
   1.150  lemma neg_equal_iff_equal [simp]:
   1.151    "- a = - b \<longleftrightarrow> a = b" 
   1.152  proof 
   1.153    assume "- a = - b"
   1.154 -  hence "- (- a) = - (- b)"
   1.155 -    by simp
   1.156 +  hence "- (- a) = - (- b)" by simp
   1.157    thus "a = b" by simp
   1.158  next
   1.159    assume "a = b"
   1.160 @@ -210,11 +221,11 @@
   1.161  
   1.162  lemma neg_equal_0_iff_equal [simp]:
   1.163    "- a = 0 \<longleftrightarrow> a = 0"
   1.164 -  by (subst neg_equal_iff_equal [symmetric], simp)
   1.165 +by (subst neg_equal_iff_equal [symmetric], simp)
   1.166  
   1.167  lemma neg_0_equal_iff_equal [simp]:
   1.168    "0 = - a \<longleftrightarrow> 0 = a"
   1.169 -  by (subst neg_equal_iff_equal [symmetric], simp)
   1.170 +by (subst neg_equal_iff_equal [symmetric], simp)
   1.171  
   1.172  text{*The next two equations can make the simplifier loop!*}
   1.173  
   1.174 @@ -233,10 +244,12 @@
   1.175  qed
   1.176  
   1.177  lemma diff_add_cancel: "a - b + b = a"
   1.178 -  by (simp add: diff_minus add_assoc)
   1.179 +by (simp add: diff_minus add_assoc)
   1.180  
   1.181  lemma add_diff_cancel: "a + b - b = a"
   1.182 -  by (simp add: diff_minus add_assoc)
   1.183 +by (simp add: diff_minus add_assoc)
   1.184 +
   1.185 +declare diff_minus[symmetric, algebra_simps]
   1.186  
   1.187  end
   1.188  
   1.189 @@ -257,43 +270,38 @@
   1.190    then show "b = c" by simp
   1.191  qed
   1.192  
   1.193 -lemma uminus_add_conv_diff:
   1.194 +lemma uminus_add_conv_diff[algebra_simps]:
   1.195    "- a + b = b - a"
   1.196 -  by (simp add:diff_minus add_commute)
   1.197 +by (simp add:diff_minus add_commute)
   1.198  
   1.199  lemma minus_add_distrib [simp]:
   1.200    "- (a + b) = - a + - b"
   1.201 -  by (rule equals_zero_I) (simp add: add_ac)
   1.202 +by (rule equals_zero_I) (simp add: add_ac)
   1.203  
   1.204  lemma minus_diff_eq [simp]:
   1.205    "- (a - b) = b - a"
   1.206 -  by (simp add: diff_minus add_commute)
   1.207 -
   1.208 -lemma add_diff_eq: "a + (b - c) = (a + b) - c"
   1.209 -  by (simp add: diff_minus add_ac)
   1.210 +by (simp add: diff_minus add_commute)
   1.211  
   1.212 -lemma diff_add_eq: "(a - b) + c = (a + c) - b"
   1.213 -  by (simp add: diff_minus add_ac)
   1.214 +lemma add_diff_eq[algebra_simps]: "a + (b - c) = (a + b) - c"
   1.215 +by (simp add: diff_minus add_ac)
   1.216  
   1.217 -lemma diff_eq_eq: "a - b = c \<longleftrightarrow> a = c + b"
   1.218 -  by (auto simp add: diff_minus add_assoc)
   1.219 +lemma diff_add_eq[algebra_simps]: "(a - b) + c = (a + c) - b"
   1.220 +by (simp add: diff_minus add_ac)
   1.221  
   1.222 -lemma eq_diff_eq: "a = c - b \<longleftrightarrow> a + b = c"
   1.223 -  by (auto simp add: diff_minus add_assoc)
   1.224 +lemma diff_eq_eq[algebra_simps]: "a - b = c \<longleftrightarrow> a = c + b"
   1.225 +by (auto simp add: diff_minus add_assoc)
   1.226  
   1.227 -lemma diff_diff_eq: "(a - b) - c = a - (b + c)"
   1.228 -  by (simp add: diff_minus add_ac)
   1.229 +lemma eq_diff_eq[algebra_simps]: "a = c - b \<longleftrightarrow> a + b = c"
   1.230 +by (auto simp add: diff_minus add_assoc)
   1.231  
   1.232 -lemma diff_diff_eq2: "a - (b - c) = (a + c) - b"
   1.233 -  by (simp add: diff_minus add_ac)
   1.234 +lemma diff_diff_eq[algebra_simps]: "(a - b) - c = a - (b + c)"
   1.235 +by (simp add: diff_minus add_ac)
   1.236  
   1.237 -lemmas compare_rls =
   1.238 -       diff_minus [symmetric]
   1.239 -       add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2
   1.240 -       diff_eq_eq eq_diff_eq
   1.241 +lemma diff_diff_eq2[algebra_simps]: "a - (b - c) = (a + c) - b"
   1.242 +by (simp add: diff_minus add_ac)
   1.243  
   1.244  lemma eq_iff_diff_eq_0: "a = b \<longleftrightarrow> a - b = 0"
   1.245 -  by (simp add: compare_rls)
   1.246 +by (simp add: algebra_simps)
   1.247  
   1.248  end
   1.249  
   1.250 @@ -305,7 +313,7 @@
   1.251  
   1.252  lemma add_right_mono:
   1.253    "a \<le> b \<Longrightarrow> a + c \<le> b + c"
   1.254 -  by (simp add: add_commute [of _ c] add_left_mono)
   1.255 +by (simp add: add_commute [of _ c] add_left_mono)
   1.256  
   1.257  text {* non-strict, in both arguments *}
   1.258  lemma add_mono:
   1.259 @@ -322,11 +330,11 @@
   1.260  
   1.261  lemma add_strict_left_mono:
   1.262    "a < b \<Longrightarrow> c + a < c + b"
   1.263 -  by (auto simp add: less_le add_left_mono)
   1.264 +by (auto simp add: less_le add_left_mono)
   1.265  
   1.266  lemma add_strict_right_mono:
   1.267    "a < b \<Longrightarrow> a + c < b + c"
   1.268 -  by (simp add: add_commute [of _ c] add_strict_left_mono)
   1.269 +by (simp add: add_commute [of _ c] add_strict_left_mono)
   1.270  
   1.271  text{*Strict monotonicity in both arguments*}
   1.272  lemma add_strict_mono:
   1.273 @@ -355,8 +363,7 @@
   1.274  begin
   1.275  
   1.276  lemma add_less_imp_less_left:
   1.277 -   assumes less: "c + a < c + b"
   1.278 -   shows "a < b"
   1.279 +  assumes less: "c + a < c + b" shows "a < b"
   1.280  proof -
   1.281    from less have le: "c + a <= c + b" by (simp add: order_le_less)
   1.282    have "a <= b" 
   1.283 @@ -381,23 +388,23 @@
   1.284  
   1.285  lemma add_less_cancel_left [simp]:
   1.286    "c + a < c + b \<longleftrightarrow> a < b"
   1.287 -  by (blast intro: add_less_imp_less_left add_strict_left_mono) 
   1.288 +by (blast intro: add_less_imp_less_left add_strict_left_mono) 
   1.289  
   1.290  lemma add_less_cancel_right [simp]:
   1.291    "a + c < b + c \<longleftrightarrow> a < b"
   1.292 -  by (blast intro: add_less_imp_less_right add_strict_right_mono)
   1.293 +by (blast intro: add_less_imp_less_right add_strict_right_mono)
   1.294  
   1.295  lemma add_le_cancel_left [simp]:
   1.296    "c + a \<le> c + b \<longleftrightarrow> a \<le> b"
   1.297 -  by (auto, drule add_le_imp_le_left, simp_all add: add_left_mono) 
   1.298 +by (auto, drule add_le_imp_le_left, simp_all add: add_left_mono) 
   1.299  
   1.300  lemma add_le_cancel_right [simp]:
   1.301    "a + c \<le> b + c \<longleftrightarrow> a \<le> b"
   1.302 -  by (simp add: add_commute [of a c] add_commute [of b c])
   1.303 +by (simp add: add_commute [of a c] add_commute [of b c])
   1.304  
   1.305  lemma add_le_imp_le_right:
   1.306    "a + c \<le> b + c \<Longrightarrow> a \<le> b"
   1.307 -  by simp
   1.308 +by simp
   1.309  
   1.310  lemma max_add_distrib_left:
   1.311    "max x y + z = max (x + z) (y + z)"
   1.312 @@ -416,8 +423,7 @@
   1.313  begin
   1.314  
   1.315  lemma add_pos_nonneg:
   1.316 -  assumes "0 < a" and "0 \<le> b"
   1.317 -    shows "0 < a + b"
   1.318 +  assumes "0 < a" and "0 \<le> b" shows "0 < a + b"
   1.319  proof -
   1.320    have "0 + 0 < a + b" 
   1.321      using assms by (rule add_less_le_mono)
   1.322 @@ -425,13 +431,11 @@
   1.323  qed
   1.324  
   1.325  lemma add_pos_pos:
   1.326 -  assumes "0 < a" and "0 < b"
   1.327 -    shows "0 < a + b"
   1.328 -  by (rule add_pos_nonneg) (insert assms, auto)
   1.329 +  assumes "0 < a" and "0 < b" shows "0 < a + b"
   1.330 +by (rule add_pos_nonneg) (insert assms, auto)
   1.331  
   1.332  lemma add_nonneg_pos:
   1.333 -  assumes "0 \<le> a" and "0 < b"
   1.334 -    shows "0 < a + b"
   1.335 +  assumes "0 \<le> a" and "0 < b" shows "0 < a + b"
   1.336  proof -
   1.337    have "0 + 0 < a + b" 
   1.338      using assms by (rule add_le_less_mono)
   1.339 @@ -439,8 +443,7 @@
   1.340  qed
   1.341  
   1.342  lemma add_nonneg_nonneg:
   1.343 -  assumes "0 \<le> a" and "0 \<le> b"
   1.344 -    shows "0 \<le> a + b"
   1.345 +  assumes "0 \<le> a" and "0 \<le> b" shows "0 \<le> a + b"
   1.346  proof -
   1.347    have "0 + 0 \<le> a + b" 
   1.348      using assms by (rule add_mono)
   1.349 @@ -448,8 +451,7 @@
   1.350  qed
   1.351  
   1.352  lemma add_neg_nonpos: 
   1.353 -  assumes "a < 0" and "b \<le> 0"
   1.354 -  shows "a + b < 0"
   1.355 +  assumes "a < 0" and "b \<le> 0" shows "a + b < 0"
   1.356  proof -
   1.357    have "a + b < 0 + 0"
   1.358      using assms by (rule add_less_le_mono)
   1.359 @@ -457,13 +459,11 @@
   1.360  qed
   1.361  
   1.362  lemma add_neg_neg: 
   1.363 -  assumes "a < 0" and "b < 0"
   1.364 -  shows "a + b < 0"
   1.365 -  by (rule add_neg_nonpos) (insert assms, auto)
   1.366 +  assumes "a < 0" and "b < 0" shows "a + b < 0"
   1.367 +by (rule add_neg_nonpos) (insert assms, auto)
   1.368  
   1.369  lemma add_nonpos_neg:
   1.370 -  assumes "a \<le> 0" and "b < 0"
   1.371 -  shows "a + b < 0"
   1.372 +  assumes "a \<le> 0" and "b < 0" shows "a + b < 0"
   1.373  proof -
   1.374    have "a + b < 0 + 0"
   1.375      using assms by (rule add_le_less_mono)
   1.376 @@ -471,8 +471,7 @@
   1.377  qed
   1.378  
   1.379  lemma add_nonpos_nonpos:
   1.380 -  assumes "a \<le> 0" and "b \<le> 0"
   1.381 -  shows "a + b \<le> 0"
   1.382 +  assumes "a \<le> 0" and "b \<le> 0" shows "a + b \<le> 0"
   1.383  proof -
   1.384    have "a + b \<le> 0 + 0"
   1.385      using assms by (rule add_mono)
   1.386 @@ -500,31 +499,25 @@
   1.387  
   1.388  lemma max_diff_distrib_left:
   1.389    shows "max x y - z = max (x - z) (y - z)"
   1.390 -  by (simp add: diff_minus, rule max_add_distrib_left) 
   1.391 +by (simp add: diff_minus, rule max_add_distrib_left) 
   1.392  
   1.393  lemma min_diff_distrib_left:
   1.394    shows "min x y - z = min (x - z) (y - z)"
   1.395 -  by (simp add: diff_minus, rule min_add_distrib_left) 
   1.396 +by (simp add: diff_minus, rule min_add_distrib_left) 
   1.397  
   1.398  lemma le_imp_neg_le:
   1.399 -  assumes "a \<le> b"
   1.400 -  shows "-b \<le> -a"
   1.401 +  assumes "a \<le> b" shows "-b \<le> -a"
   1.402  proof -
   1.403 -  have "-a+a \<le> -a+b"
   1.404 -    using `a \<le> b` by (rule add_left_mono) 
   1.405 -  hence "0 \<le> -a+b"
   1.406 -    by simp
   1.407 -  hence "0 + (-b) \<le> (-a + b) + (-b)"
   1.408 -    by (rule add_right_mono) 
   1.409 -  thus ?thesis
   1.410 -    by (simp add: add_assoc)
   1.411 +  have "-a+a \<le> -a+b" using `a \<le> b` by (rule add_left_mono) 
   1.412 +  hence "0 \<le> -a+b" by simp
   1.413 +  hence "0 + (-b) \<le> (-a + b) + (-b)" by (rule add_right_mono) 
   1.414 +  thus ?thesis by (simp add: add_assoc)
   1.415  qed
   1.416  
   1.417  lemma neg_le_iff_le [simp]: "- b \<le> - a \<longleftrightarrow> a \<le> b"
   1.418  proof 
   1.419    assume "- b \<le> - a"
   1.420 -  hence "- (- a) \<le> - (- b)"
   1.421 -    by (rule le_imp_neg_le)
   1.422 +  hence "- (- a) \<le> - (- b)" by (rule le_imp_neg_le)
   1.423    thus "a\<le>b" by simp
   1.424  next
   1.425    assume "a\<le>b"
   1.426 @@ -532,19 +525,19 @@
   1.427  qed
   1.428  
   1.429  lemma neg_le_0_iff_le [simp]: "- a \<le> 0 \<longleftrightarrow> 0 \<le> a"
   1.430 -  by (subst neg_le_iff_le [symmetric], simp)
   1.431 +by (subst neg_le_iff_le [symmetric], simp)
   1.432  
   1.433  lemma neg_0_le_iff_le [simp]: "0 \<le> - a \<longleftrightarrow> a \<le> 0"
   1.434 -  by (subst neg_le_iff_le [symmetric], simp)
   1.435 +by (subst neg_le_iff_le [symmetric], simp)
   1.436  
   1.437  lemma neg_less_iff_less [simp]: "- b < - a \<longleftrightarrow> a < b"
   1.438 -  by (force simp add: less_le) 
   1.439 +by (force simp add: less_le) 
   1.440  
   1.441  lemma neg_less_0_iff_less [simp]: "- a < 0 \<longleftrightarrow> 0 < a"
   1.442 -  by (subst neg_less_iff_less [symmetric], simp)
   1.443 +by (subst neg_less_iff_less [symmetric], simp)
   1.444  
   1.445  lemma neg_0_less_iff_less [simp]: "0 < - a \<longleftrightarrow> a < 0"
   1.446 -  by (subst neg_less_iff_less [symmetric], simp)
   1.447 +by (subst neg_less_iff_less [symmetric], simp)
   1.448  
   1.449  text{*The next several equations can make the simplifier loop!*}
   1.450  
   1.451 @@ -573,7 +566,7 @@
   1.452  qed
   1.453  
   1.454  lemma minus_le_iff: "- a \<le> b \<longleftrightarrow> - b \<le> a"
   1.455 -  by (auto simp add: le_less minus_less_iff)
   1.456 +by (auto simp add: le_less minus_less_iff)
   1.457  
   1.458  lemma less_iff_diff_less_0: "a < b \<longleftrightarrow> a - b < 0"
   1.459  proof -
   1.460 @@ -583,56 +576,34 @@
   1.461    finally show ?thesis .
   1.462  qed
   1.463  
   1.464 -lemma diff_less_eq: "a - b < c \<longleftrightarrow> a < c + b"
   1.465 +lemma diff_less_eq[algebra_simps]: "a - b < c \<longleftrightarrow> a < c + b"
   1.466  apply (subst less_iff_diff_less_0 [of a])
   1.467  apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst])
   1.468  apply (simp add: diff_minus add_ac)
   1.469  done
   1.470  
   1.471 -lemma less_diff_eq: "a < c - b \<longleftrightarrow> a + b < c"
   1.472 +lemma less_diff_eq[algebra_simps]: "a < c - b \<longleftrightarrow> a + b < c"
   1.473  apply (subst less_iff_diff_less_0 [of "plus a b"])
   1.474  apply (subst less_iff_diff_less_0 [of a])
   1.475  apply (simp add: diff_minus add_ac)
   1.476  done
   1.477  
   1.478 -lemma diff_le_eq: "a - b \<le> c \<longleftrightarrow> a \<le> c + b"
   1.479 -  by (auto simp add: le_less diff_less_eq diff_add_cancel add_diff_cancel)
   1.480 -
   1.481 -lemma le_diff_eq: "a \<le> c - b \<longleftrightarrow> a + b \<le> c"
   1.482 -  by (auto simp add: le_less less_diff_eq diff_add_cancel add_diff_cancel)
   1.483 +lemma diff_le_eq[algebra_simps]: "a - b \<le> c \<longleftrightarrow> a \<le> c + b"
   1.484 +by (auto simp add: le_less diff_less_eq diff_add_cancel add_diff_cancel)
   1.485  
   1.486 -lemmas compare_rls =
   1.487 -       diff_minus [symmetric]
   1.488 -       add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2
   1.489 -       diff_less_eq less_diff_eq diff_le_eq le_diff_eq
   1.490 -       diff_eq_eq eq_diff_eq
   1.491 -
   1.492 -text{*This list of rewrites simplifies (in)equalities by bringing subtractions
   1.493 -  to the top and then moving negative terms to the other side.
   1.494 -  Use with @{text add_ac}*}
   1.495 -lemmas (in -) compare_rls =
   1.496 -       diff_minus [symmetric]
   1.497 -       add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2
   1.498 -       diff_less_eq less_diff_eq diff_le_eq le_diff_eq
   1.499 -       diff_eq_eq eq_diff_eq
   1.500 +lemma le_diff_eq[algebra_simps]: "a \<le> c - b \<longleftrightarrow> a + b \<le> c"
   1.501 +by (auto simp add: le_less less_diff_eq diff_add_cancel add_diff_cancel)
   1.502  
   1.503  lemma le_iff_diff_le_0: "a \<le> b \<longleftrightarrow> a - b \<le> 0"
   1.504 -  by (simp add: compare_rls)
   1.505 +by (simp add: algebra_simps)
   1.506  
   1.507 -lemmas group_simps =
   1.508 -  add_ac
   1.509 -  add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2
   1.510 -  diff_eq_eq eq_diff_eq diff_minus [symmetric] uminus_add_conv_diff
   1.511 -  diff_less_eq less_diff_eq diff_le_eq le_diff_eq
   1.512 +text{*Legacy - use @{text algebra_simps} *}
   1.513 +lemmas group_simps = algebra_simps
   1.514  
   1.515  end
   1.516  
   1.517 -lemmas group_simps =
   1.518 -  mult_ac
   1.519 -  add_ac
   1.520 -  add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2
   1.521 -  diff_eq_eq eq_diff_eq diff_minus [symmetric] uminus_add_conv_diff
   1.522 -  diff_less_eq less_diff_eq diff_le_eq le_diff_eq
   1.523 +text{*Legacy - use @{text algebra_simps} *}
   1.524 +lemmas group_simps = algebra_simps
   1.525  
   1.526  class ordered_ab_semigroup_add =
   1.527    linorder + pordered_ab_semigroup_add
   1.528 @@ -766,8 +737,7 @@
   1.529    unfolding neg_le_0_iff_le by simp
   1.530  
   1.531  lemma abs_of_nonneg [simp]:
   1.532 -  assumes nonneg: "0 \<le> a"
   1.533 -  shows "\<bar>a\<bar> = a"
   1.534 +  assumes nonneg: "0 \<le> a" shows "\<bar>a\<bar> = a"
   1.535  proof (rule antisym)
   1.536    from nonneg le_imp_neg_le have "- a \<le> 0" by simp
   1.537    from this nonneg have "- a \<le> a" by (rule order_trans)
   1.538 @@ -775,8 +745,8 @@
   1.539  qed (rule abs_ge_self)
   1.540  
   1.541  lemma abs_idempotent [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>"
   1.542 -  by (rule antisym)
   1.543 -    (auto intro!: abs_ge_self abs_leI order_trans [of "uminus (abs a)" zero "abs a"])
   1.544 +by (rule antisym)
   1.545 +   (auto intro!: abs_ge_self abs_leI order_trans [of "uminus (abs a)" zero "abs a"])
   1.546  
   1.547  lemma abs_eq_0 [simp]: "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0"
   1.548  proof -
   1.549 @@ -792,7 +762,7 @@
   1.550  qed
   1.551  
   1.552  lemma abs_zero [simp]: "\<bar>0\<bar> = 0"
   1.553 -  by simp
   1.554 +by simp
   1.555  
   1.556  lemma abs_0_eq [simp, noatp]: "0 = \<bar>a\<bar> \<longleftrightarrow> a = 0"
   1.557  proof -
   1.558 @@ -811,7 +781,7 @@
   1.559  qed
   1.560  
   1.561  lemma zero_less_abs_iff [simp]: "0 < \<bar>a\<bar> \<longleftrightarrow> a \<noteq> 0"
   1.562 -  by (simp add: less_le)
   1.563 +by (simp add: less_le)
   1.564  
   1.565  lemma abs_not_less_zero [simp]: "\<not> \<bar>a\<bar> < 0"
   1.566  proof -
   1.567 @@ -834,11 +804,10 @@
   1.568  qed
   1.569  
   1.570  lemma abs_of_pos: "0 < a \<Longrightarrow> \<bar>a\<bar> = a"
   1.571 -  by (rule abs_of_nonneg, rule less_imp_le)
   1.572 +by (rule abs_of_nonneg, rule less_imp_le)
   1.573  
   1.574  lemma abs_of_nonpos [simp]:
   1.575 -  assumes "a \<le> 0"
   1.576 -  shows "\<bar>a\<bar> = - a"
   1.577 +  assumes "a \<le> 0" shows "\<bar>a\<bar> = - a"
   1.578  proof -
   1.579    let ?b = "- a"
   1.580    have "- ?b \<le> 0 \<Longrightarrow> \<bar>- ?b\<bar> = - (- ?b)"
   1.581 @@ -849,24 +818,24 @@
   1.582  qed
   1.583    
   1.584  lemma abs_of_neg: "a < 0 \<Longrightarrow> \<bar>a\<bar> = - a"
   1.585 -  by (rule abs_of_nonpos, rule less_imp_le)
   1.586 +by (rule abs_of_nonpos, rule less_imp_le)
   1.587  
   1.588  lemma abs_le_D1: "\<bar>a\<bar> \<le> b \<Longrightarrow> a \<le> b"
   1.589 -  by (insert abs_ge_self, blast intro: order_trans)
   1.590 +by (insert abs_ge_self, blast intro: order_trans)
   1.591  
   1.592  lemma abs_le_D2: "\<bar>a\<bar> \<le> b \<Longrightarrow> - a \<le> b"
   1.593 -  by (insert abs_le_D1 [of "uminus a"], simp)
   1.594 +by (insert abs_le_D1 [of "uminus a"], simp)
   1.595  
   1.596  lemma abs_le_iff: "\<bar>a\<bar> \<le> b \<longleftrightarrow> a \<le> b \<and> - a \<le> b"
   1.597 -  by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2)
   1.598 +by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2)
   1.599  
   1.600  lemma abs_triangle_ineq2: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>a - b\<bar>"
   1.601 -  apply (simp add: compare_rls)
   1.602 -  apply (subgoal_tac "abs a = abs (plus (minus a b) b)")
   1.603 +  apply (simp add: algebra_simps)
   1.604 +  apply (subgoal_tac "abs a = abs (plus b (minus a b))")
   1.605    apply (erule ssubst)
   1.606    apply (rule abs_triangle_ineq)
   1.607 -  apply (rule arg_cong) back
   1.608 -  apply (simp add: compare_rls)
   1.609 +  apply (rule arg_cong[of _ _ abs])
   1.610 +  apply (simp add: algebra_simps)
   1.611  done
   1.612  
   1.613  lemma abs_triangle_ineq3: "\<bar>\<bar>a\<bar> - \<bar>b\<bar>\<bar> \<le> \<bar>a - b\<bar>"
   1.614 @@ -879,12 +848,9 @@
   1.615  
   1.616  lemma abs_triangle_ineq4: "\<bar>a - b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
   1.617  proof -
   1.618 -  have "abs(a - b) = abs(a + - b)"
   1.619 -    by (subst diff_minus, rule refl)
   1.620 -  also have "... <= abs a + abs (- b)"
   1.621 -    by (rule abs_triangle_ineq)
   1.622 -  finally show ?thesis
   1.623 -    by simp
   1.624 +  have "abs(a - b) = abs(a + - b)" by (subst diff_minus, rule refl)
   1.625 +  also have "... <= abs a + abs (- b)" by (rule abs_triangle_ineq)
   1.626 +  finally show ?thesis by simp
   1.627  qed
   1.628  
   1.629  lemma abs_diff_triangle_ineq: "\<bar>a + b - (c + d)\<bar> \<le> \<bar>a - c\<bar> + \<bar>b - d\<bar>"
   1.630 @@ -999,23 +965,19 @@
   1.631  qed
   1.632  
   1.633  lemma neg_inf_eq_sup: "- inf a b = sup (-a) (-b)"
   1.634 -  by (simp add: inf_eq_neg_sup)
   1.635 +by (simp add: inf_eq_neg_sup)
   1.636  
   1.637  lemma neg_sup_eq_inf: "- sup a b = inf (-a) (-b)"
   1.638 -  by (simp add: sup_eq_neg_inf)
   1.639 +by (simp add: sup_eq_neg_inf)
   1.640  
   1.641  lemma add_eq_inf_sup: "a + b = sup a b + inf a b"
   1.642  proof -
   1.643    have "0 = - inf 0 (a-b) + inf (a-b) 0" by (simp add: inf_commute)
   1.644    hence "0 = sup 0 (b-a) + inf (a-b) 0" by (simp add: inf_eq_neg_sup)
   1.645    hence "0 = (-a + sup a b) + (inf a b + (-b))"
   1.646 -    apply (simp add: add_sup_distrib_left add_inf_distrib_right)
   1.647 -    by (simp add: diff_minus add_commute)
   1.648 -  thus ?thesis
   1.649 -    apply (simp add: compare_rls)
   1.650 -    apply (subst add_left_cancel [symmetric, of "plus a b" "plus (sup a b) (inf a b)" "uminus a"])
   1.651 -    apply (simp only: add_assoc, simp add: add_assoc[symmetric])
   1.652 -    done
   1.653 +    by (simp add: add_sup_distrib_left add_inf_distrib_right)
   1.654 +       (simp add: algebra_simps)
   1.655 +  thus ?thesis by (simp add: algebra_simps)
   1.656  qed
   1.657  
   1.658  subsection {* Positive Part, Negative Part, Absolute Value *}
   1.659 @@ -1044,13 +1006,13 @@
   1.660  qed
   1.661  
   1.662  lemma prts: "a = pprt a + nprt a"
   1.663 -  by (simp add: pprt_def nprt_def add_eq_inf_sup[symmetric])
   1.664 +by (simp add: pprt_def nprt_def add_eq_inf_sup[symmetric])
   1.665  
   1.666  lemma zero_le_pprt[simp]: "0 \<le> pprt a"
   1.667 -  by (simp add: pprt_def)
   1.668 +by (simp add: pprt_def)
   1.669  
   1.670  lemma nprt_le_zero[simp]: "nprt a \<le> 0"
   1.671 -  by (simp add: nprt_def)
   1.672 +by (simp add: nprt_def)
   1.673  
   1.674  lemma le_eq_neg: "a \<le> - b \<longleftrightarrow> a + b \<le> 0" (is "?l = ?r")
   1.675  proof -
   1.676 @@ -1071,16 +1033,16 @@
   1.677  lemma nprt_0[simp]: "nprt 0 = 0" by (simp add: nprt_def)
   1.678  
   1.679  lemma pprt_eq_id [simp, noatp]: "0 \<le> x \<Longrightarrow> pprt x = x"
   1.680 -  by (simp add: pprt_def le_iff_sup sup_ACI)
   1.681 +by (simp add: pprt_def le_iff_sup sup_ACI)
   1.682  
   1.683  lemma nprt_eq_id [simp, noatp]: "x \<le> 0 \<Longrightarrow> nprt x = x"
   1.684 -  by (simp add: nprt_def le_iff_inf inf_ACI)
   1.685 +by (simp add: nprt_def le_iff_inf inf_ACI)
   1.686  
   1.687  lemma pprt_eq_0 [simp, noatp]: "x \<le> 0 \<Longrightarrow> pprt x = 0"
   1.688 -  by (simp add: pprt_def le_iff_sup sup_ACI)
   1.689 +by (simp add: pprt_def le_iff_sup sup_ACI)
   1.690  
   1.691  lemma nprt_eq_0 [simp, noatp]: "0 \<le> x \<Longrightarrow> nprt x = 0"
   1.692 -  by (simp add: nprt_def le_iff_inf inf_ACI)
   1.693 +by (simp add: nprt_def le_iff_inf inf_ACI)
   1.694  
   1.695  lemma sup_0_imp_0: "sup a (- a) = 0 \<Longrightarrow> a = 0"
   1.696  proof -
   1.697 @@ -1105,10 +1067,10 @@
   1.698  done
   1.699  
   1.700  lemma inf_0_eq_0 [simp, noatp]: "inf a (- a) = 0 \<longleftrightarrow> a = 0"
   1.701 -  by (rule, erule inf_0_imp_0) simp
   1.702 +by (rule, erule inf_0_imp_0) simp
   1.703  
   1.704  lemma sup_0_eq_0 [simp, noatp]: "sup a (- a) = 0 \<longleftrightarrow> a = 0"
   1.705 -  by (rule, erule sup_0_imp_0) simp
   1.706 +by (rule, erule sup_0_imp_0) simp
   1.707  
   1.708  lemma zero_le_double_add_iff_zero_le_single_add [simp]:
   1.709    "0 \<le> a + a \<longleftrightarrow> 0 \<le> a"
   1.710 @@ -1190,22 +1152,22 @@
   1.711  qed
   1.712  
   1.713  lemma zero_le_iff_zero_nprt: "0 \<le> a \<longleftrightarrow> nprt a = 0"
   1.714 -  by (simp add: le_iff_inf nprt_def inf_commute)
   1.715 +by (simp add: le_iff_inf nprt_def inf_commute)
   1.716  
   1.717  lemma le_zero_iff_zero_pprt: "a \<le> 0 \<longleftrightarrow> pprt a = 0"
   1.718 -  by (simp add: le_iff_sup pprt_def sup_commute)
   1.719 +by (simp add: le_iff_sup pprt_def sup_commute)
   1.720  
   1.721  lemma le_zero_iff_pprt_id: "0 \<le> a \<longleftrightarrow> pprt a = a"
   1.722 -  by (simp add: le_iff_sup pprt_def sup_commute)
   1.723 +by (simp add: le_iff_sup pprt_def sup_commute)
   1.724  
   1.725  lemma zero_le_iff_nprt_id: "a \<le> 0 \<longleftrightarrow> nprt a = a"
   1.726 -  by (simp add: le_iff_inf nprt_def inf_commute)
   1.727 +by (simp add: le_iff_inf nprt_def inf_commute)
   1.728  
   1.729  lemma pprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> pprt a \<le> pprt b"
   1.730 -  by (simp add: le_iff_sup pprt_def sup_ACI sup_assoc [symmetric, of a])
   1.731 +by (simp add: le_iff_sup pprt_def sup_ACI sup_assoc [symmetric, of a])
   1.732  
   1.733  lemma nprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> nprt a \<le> nprt b"
   1.734 -  by (simp add: le_iff_inf nprt_def inf_ACI inf_assoc [symmetric, of a])
   1.735 +by (simp add: le_iff_inf nprt_def inf_ACI inf_assoc [symmetric, of a])
   1.736  
   1.737  end
   1.738  
   1.739 @@ -1246,12 +1208,10 @@
   1.740      show "0 \<le> \<bar>a\<bar>" by simp
   1.741    next
   1.742      fix a
   1.743 -    show "a \<le> \<bar>a\<bar>"
   1.744 -      by (auto simp add: abs_lattice)
   1.745 +    show "a \<le> \<bar>a\<bar>" by (auto simp add: abs_lattice)
   1.746    next
   1.747      fix a
   1.748 -    show "\<bar>-a\<bar> = \<bar>a\<bar>"
   1.749 -      by (simp add: abs_lattice sup_commute)
   1.750 +    show "\<bar>-a\<bar> = \<bar>a\<bar>" by (simp add: abs_lattice sup_commute)
   1.751    next
   1.752      fix a b
   1.753      show "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b" by (erule abs_leI)
   1.754 @@ -1266,8 +1226,7 @@
   1.755        have c:"?n <= sup ?m ?n" by (simp)
   1.756        from b c have d: "-a-b <= sup ?m ?n" by(rule order_trans)
   1.757        have e:"-a-b = -(a+b)" by (simp add: diff_minus)
   1.758 -      from a d e have "abs(a+b) <= sup ?m ?n" 
   1.759 -        by (drule_tac abs_leI, auto)
   1.760 +      from a d e have "abs(a+b) <= sup ?m ?n" by (drule_tac abs_leI, auto)
   1.761        with g[symmetric] show ?thesis by simp
   1.762      qed
   1.763    qed auto
   1.764 @@ -1287,7 +1246,7 @@
   1.765  lemma abs_if_lattice:
   1.766    fixes a :: "'a\<Colon>{lordered_ab_group_add_abs, linorder}"
   1.767    shows "\<bar>a\<bar> = (if a < 0 then - a else a)"
   1.768 -  by auto
   1.769 +by auto
   1.770  
   1.771  
   1.772  text {* Needed for abelian cancellation simprocs: *}
   1.773 @@ -1333,7 +1292,7 @@
   1.774    "a + b <= (c::'a::lordered_ab_group_add_abs) \<Longrightarrow> a <= c + abs b" 
   1.775  proof -
   1.776    assume "a+b <= c"
   1.777 -  hence 2: "a <= c+(-b)" by (simp add: group_simps)
   1.778 +  hence 2: "a <= c+(-b)" by (simp add: algebra_simps)
   1.779    have 3: "(-b) <= abs b" by (rule abs_ge_minus_self)
   1.780    show ?thesis by (rule le_add_right_mono[OF 2 3])
   1.781  qed