src/HOL/OrderedGroup.thy
changeset 25062 af5ef0d4d655
parent 24748 ee0a0eb6b738
child 25077 c2ec5e589d78
     1.1 --- a/src/HOL/OrderedGroup.thy	Tue Oct 16 23:12:38 2007 +0200
     1.2 +++ b/src/HOL/OrderedGroup.thy	Tue Oct 16 23:12:45 2007 +0200
     1.3 @@ -27,58 +27,75 @@
     1.4  subsection {* Semigroups and Monoids *}
     1.5  
     1.6  class semigroup_add = plus +
     1.7 -  assumes add_assoc: "(a \<^loc>+ b) \<^loc>+ c = a \<^loc>+ (b \<^loc>+ c)"
     1.8 +  assumes add_assoc: "(a + b) + c = a + (b + c)"
     1.9  
    1.10  class ab_semigroup_add = semigroup_add +
    1.11 -  assumes add_commute: "a \<^loc>+ b = b \<^loc>+ a"
    1.12 +  assumes add_commute: "a + b = b + a"
    1.13 +begin
    1.14  
    1.15 -lemma add_left_commute: "a + (b + c) = b + (a + (c::'a::ab_semigroup_add))"
    1.16 -  by (rule mk_left_commute [of "op +", OF add_assoc add_commute])
    1.17 +lemma add_left_commute: "a + (b + c) = b + (a + c)"
    1.18 +  by (rule mk_left_commute [of "plus", OF add_assoc add_commute])
    1.19 +  (*FIXME term_check*)
    1.20 +
    1.21 +theorems add_ac = add_assoc add_commute add_left_commute
    1.22 +
    1.23 +end
    1.24  
    1.25  theorems add_ac = add_assoc add_commute add_left_commute
    1.26  
    1.27  class semigroup_mult = times +
    1.28 -  assumes mult_assoc: "(a \<^loc>* b) \<^loc>* c = a \<^loc>* (b \<^loc>* c)"
    1.29 +  assumes mult_assoc: "(a * b) * c = a * (b * c)"
    1.30  
    1.31  class ab_semigroup_mult = semigroup_mult +
    1.32 -  assumes mult_commute: "a \<^loc>* b = b \<^loc>* a"
    1.33 +  assumes mult_commute: "a * b = b * a"
    1.34  begin
    1.35  
    1.36 -lemma mult_left_commute: "a \<^loc>* (b \<^loc>* c) = b \<^loc>* (a \<^loc>* c)"
    1.37 -  by (rule mk_left_commute [of "op \<^loc>*", OF mult_assoc mult_commute])
    1.38 +lemma mult_left_commute: "a * (b * c) = b * (a * c)"
    1.39 +  by (rule mk_left_commute [of "times", OF mult_assoc mult_commute])
    1.40 +  (*FIXME term_check*)
    1.41 +
    1.42 +theorems mult_ac = mult_assoc mult_commute mult_left_commute
    1.43  
    1.44  end
    1.45  
    1.46  theorems mult_ac = mult_assoc mult_commute mult_left_commute
    1.47  
    1.48  class monoid_add = zero + semigroup_add +
    1.49 -  assumes add_0_left [simp]: "\<^loc>0 \<^loc>+ a = a" and add_0_right [simp]: "a \<^loc>+ \<^loc>0 = a"
    1.50 +  assumes add_0_left [simp]: "0 + a = a"
    1.51 +    and add_0_right [simp]: "a + 0 = a"
    1.52  
    1.53  class comm_monoid_add = zero + ab_semigroup_add +
    1.54 -  assumes add_0: "\<^loc>0 \<^loc>+ a = a"
    1.55 +  assumes add_0: "0 + a = a"
    1.56 +begin
    1.57  
    1.58 -instance comm_monoid_add < monoid_add
    1.59 -by intro_classes (insert comm_monoid_add_class.zero_plus.add_0, simp_all add: add_commute, auto)
    1.60 +subclass monoid_add
    1.61 +  by unfold_locales (insert add_0, simp_all add: add_commute)
    1.62 +
    1.63 +end
    1.64  
    1.65  class monoid_mult = one + semigroup_mult +
    1.66 -  assumes mult_1_left [simp]: "\<^loc>1 \<^loc>* a  = a"
    1.67 -  assumes mult_1_right [simp]: "a \<^loc>* \<^loc>1 = a"
    1.68 +  assumes mult_1_left [simp]: "1 * a  = a"
    1.69 +  assumes mult_1_right [simp]: "a * 1 = a"
    1.70  
    1.71  class comm_monoid_mult = one + ab_semigroup_mult +
    1.72 -  assumes mult_1: "\<^loc>1 \<^loc>* a = a"
    1.73 +  assumes mult_1: "1 * a = a"
    1.74 +begin
    1.75  
    1.76 -instance comm_monoid_mult \<subseteq> monoid_mult
    1.77 -  by intro_classes (insert mult_1, simp_all add: mult_commute, auto)
    1.78 +subclass monoid_mult
    1.79 +  by unfold_locales (insert mult_1, simp_all add: mult_commute) 
    1.80 +
    1.81 +end
    1.82  
    1.83  class cancel_semigroup_add = semigroup_add +
    1.84 -  assumes add_left_imp_eq: "a \<^loc>+ b = a \<^loc>+ c \<Longrightarrow> b = c"
    1.85 -  assumes add_right_imp_eq: "b \<^loc>+ a = c \<^loc>+ a \<Longrightarrow> b = c"
    1.86 +  assumes add_left_imp_eq: "a + b = a + c \<Longrightarrow> b = c"
    1.87 +  assumes add_right_imp_eq: "b + a = c + a \<Longrightarrow> b = c"
    1.88  
    1.89  class cancel_ab_semigroup_add = ab_semigroup_add +
    1.90 -  assumes add_imp_eq: "a \<^loc>+ b = a \<^loc>+ c \<Longrightarrow> b = c"
    1.91 +  assumes add_imp_eq: "a + b = a + c \<Longrightarrow> b = c"
    1.92 +begin
    1.93  
    1.94 -instance cancel_ab_semigroup_add \<subseteq> cancel_semigroup_add
    1.95 -proof intro_classes
    1.96 +subclass cancel_semigroup_add
    1.97 +proof unfold_locales
    1.98    fix a b c :: 'a
    1.99    assume "a + b = a + c" 
   1.100    then show "b = c" by (rule add_imp_eq)
   1.101 @@ -89,60 +106,50 @@
   1.102    then show "b = c" by (rule add_imp_eq)
   1.103  qed
   1.104  
   1.105 +end context cancel_ab_semigroup_add begin
   1.106 +
   1.107  lemma add_left_cancel [simp]:
   1.108 -  "a + b = a + c \<longleftrightarrow> b = (c \<Colon> 'a\<Colon>cancel_semigroup_add)"
   1.109 +  "a + b = a + c \<longleftrightarrow> b = c"
   1.110    by (blast dest: add_left_imp_eq)
   1.111  
   1.112  lemma add_right_cancel [simp]:
   1.113 -  "b + a = c + a \<longleftrightarrow> b = (c \<Colon> 'a\<Colon>cancel_semigroup_add)"
   1.114 +  "b + a = c + a \<longleftrightarrow> b = c"
   1.115    by (blast dest: add_right_imp_eq)
   1.116  
   1.117 +end
   1.118 +
   1.119  subsection {* Groups *}
   1.120  
   1.121 -class ab_group_add = minus + comm_monoid_add +
   1.122 -  assumes ab_left_minus: "uminus a \<^loc>+ a = \<^loc>0"
   1.123 -  assumes ab_diff_minus: "a \<^loc>- b = a \<^loc>+ (uminus b)"
   1.124 -
   1.125  class group_add = minus + monoid_add +
   1.126 -  assumes left_minus [simp]: "uminus a \<^loc>+ a = \<^loc>0"
   1.127 -  assumes diff_minus: "a \<^loc>- b = a \<^loc>+ (uminus b)"
   1.128 -
   1.129 -instance ab_group_add < group_add
   1.130 -by intro_classes (simp_all add: ab_left_minus ab_diff_minus)
   1.131 +  assumes left_minus [simp]: "- a + a = 0"
   1.132 +  assumes diff_minus: "a - b = a + (- b)"
   1.133 +begin
   1.134  
   1.135 -instance ab_group_add \<subseteq> cancel_ab_semigroup_add
   1.136 -proof intro_classes
   1.137 -  fix a b c :: 'a
   1.138 -  assume "a + b = a + c"
   1.139 -  then have "uminus a + a + b = uminus a + a + c" unfolding add_assoc by simp
   1.140 -  then show "b = c" by simp
   1.141 -qed
   1.142 +lemma minus_add_cancel: "- a + (a + b) = b"
   1.143 +  by (simp add: add_assoc[symmetric])
   1.144  
   1.145 -lemma minus_add_cancel: "-(a::'a::group_add) + (a+b) = b"
   1.146 -by(simp add:add_assoc[symmetric])
   1.147 -
   1.148 -lemma minus_zero[simp]: "-(0::'a::group_add) = 0"
   1.149 +lemma minus_zero [simp]: "- 0 = 0"
   1.150  proof -
   1.151 -  have "-(0::'a::group_add) = - 0 + (0+0)" by(simp only: add_0_right)
   1.152 -  also have "\<dots> = 0" by(rule minus_add_cancel)
   1.153 +  have "- 0 = - 0 + (0 + 0)" by (simp only: add_0_right)
   1.154 +  also have "\<dots> = 0" by (rule minus_add_cancel)
   1.155    finally show ?thesis .
   1.156  qed
   1.157  
   1.158 -lemma minus_minus[simp]: "- (-(a::'a::group_add)) = a"
   1.159 +lemma minus_minus [simp]: "- (- a) = a"
   1.160  proof -
   1.161 -  have "-(-a) = -(-a) + (-a + a)" by simp
   1.162 -  also have "\<dots> = a" by(rule minus_add_cancel)
   1.163 +  have "- (- a) = - (- a) + (- a + a)" by simp
   1.164 +  also have "\<dots> = a" by (rule minus_add_cancel)
   1.165    finally show ?thesis .
   1.166  qed
   1.167  
   1.168 -lemma right_minus[simp]: "a + - a = (0::'a::group_add)"
   1.169 +lemma right_minus [simp]: "a + - a = 0"
   1.170  proof -
   1.171 -  have "a + -a = -(-a) + -a" by simp
   1.172 -  also have "\<dots> = 0" thm group_add.left_minus by(rule left_minus)
   1.173 +  have "a + - a = - (- a) + - a" by simp
   1.174 +  also have "\<dots> = 0" by (rule left_minus)
   1.175    finally show ?thesis .
   1.176  qed
   1.177  
   1.178 -lemma right_minus_eq: "(a - b = 0) = (a = (b::'a::group_add))"
   1.179 +lemma right_minus_eq: "a - b = 0 \<longleftrightarrow> a = b"
   1.180  proof
   1.181    assume "a - b = 0"
   1.182    have "a = (a - b) + b" by (simp add:diff_minus add_assoc)
   1.183 @@ -152,154 +159,173 @@
   1.184    assume "a = b" thus "a - b = 0" by (simp add: diff_minus)
   1.185  qed
   1.186  
   1.187 -lemma equals_zero_I: assumes "a+b = 0" shows "-a = (b::'a::group_add)"
   1.188 +lemma equals_zero_I:
   1.189 +  assumes "a + b = 0"
   1.190 +  shows "- a = b"
   1.191  proof -
   1.192 -  have "- a = -a + (a+b)" using assms by simp
   1.193 -  also have "\<dots> = b" by(simp add:add_assoc[symmetric])
   1.194 +  have "- a = - a + (a + b)" using assms by simp
   1.195 +  also have "\<dots> = b" by (simp add: add_assoc[symmetric])
   1.196    finally show ?thesis .
   1.197  qed
   1.198  
   1.199 -lemma diff_self[simp]: "(a::'a::group_add) - a = 0"
   1.200 -by(simp add: diff_minus)
   1.201 +lemma diff_self [simp]: "a - a = 0"
   1.202 +  by (simp add: diff_minus)
   1.203  
   1.204 -lemma diff_0 [simp]: "(0::'a::group_add) - a = -a"
   1.205 -by (simp add: diff_minus)
   1.206 +lemma diff_0 [simp]: "0 - a = - a"
   1.207 +  by (simp add: diff_minus)
   1.208  
   1.209 -lemma diff_0_right [simp]: "a - (0::'a::group_add) = a" 
   1.210 -by (simp add: diff_minus)
   1.211 +lemma diff_0_right [simp]: "a - 0 = a" 
   1.212 +  by (simp add: diff_minus)
   1.213  
   1.214 -lemma diff_minus_eq_add [simp]: "a - - b = a + (b::'a::group_add)"
   1.215 -by (simp add: diff_minus)
   1.216 +lemma diff_minus_eq_add [simp]: "a - - b = a + b"
   1.217 +  by (simp add: diff_minus)
   1.218  
   1.219 -lemma uminus_add_conv_diff: "-a + b = b - (a::'a::ab_group_add)"
   1.220 -by(simp add:diff_minus add_commute)
   1.221 -
   1.222 -lemma neg_equal_iff_equal [simp]: "(-a = -b) = (a = (b::'a::group_add))" 
   1.223 +lemma neg_equal_iff_equal [simp]:
   1.224 +  "- a = - b \<longleftrightarrow> a = b" 
   1.225  proof 
   1.226    assume "- a = - b"
   1.227    hence "- (- a) = - (- b)"
   1.228      by simp
   1.229 -  thus "a=b" by simp
   1.230 +  thus "a = b" by simp
   1.231  next
   1.232 -  assume "a=b"
   1.233 -  thus "-a = -b" by simp
   1.234 +  assume "a = b"
   1.235 +  thus "- a = - b" by simp
   1.236  qed
   1.237  
   1.238 -lemma neg_equal_0_iff_equal [simp]: "(-a = 0) = (a = (0::'a::group_add))"
   1.239 -by (subst neg_equal_iff_equal [symmetric], simp)
   1.240 +lemma neg_equal_0_iff_equal [simp]:
   1.241 +  "- a = 0 \<longleftrightarrow> a = 0"
   1.242 +  by (subst neg_equal_iff_equal [symmetric], simp)
   1.243  
   1.244 -lemma neg_0_equal_iff_equal [simp]: "(0 = -a) = (0 = (a::'a::group_add))"
   1.245 -by (subst neg_equal_iff_equal [symmetric], simp)
   1.246 +lemma neg_0_equal_iff_equal [simp]:
   1.247 +  "0 = - a \<longleftrightarrow> 0 = a"
   1.248 +  by (subst neg_equal_iff_equal [symmetric], simp)
   1.249  
   1.250  text{*The next two equations can make the simplifier loop!*}
   1.251  
   1.252 -lemma equation_minus_iff: "(a = - b) = (b = - (a::'a::group_add))"
   1.253 +lemma equation_minus_iff:
   1.254 +  "a = - b \<longleftrightarrow> b = - a"
   1.255  proof -
   1.256 -  have "(- (-a) = - b) = (- a = b)" by (rule neg_equal_iff_equal)
   1.257 +  have "- (- a) = - b \<longleftrightarrow> - a = b" by (rule neg_equal_iff_equal)
   1.258 +  thus ?thesis by (simp add: eq_commute)
   1.259 +qed
   1.260 +
   1.261 +lemma minus_equation_iff:
   1.262 +  "- a = b \<longleftrightarrow> - b = a"
   1.263 +proof -
   1.264 +  have "- a = - (- b) \<longleftrightarrow> a = -b" by (rule neg_equal_iff_equal)
   1.265    thus ?thesis by (simp add: eq_commute)
   1.266  qed
   1.267  
   1.268 -lemma minus_equation_iff: "(- a = b) = (- (b::'a::group_add) = a)"
   1.269 -proof -
   1.270 -  have "(- a = - (-b)) = (a = -b)" by (rule neg_equal_iff_equal)
   1.271 -  thus ?thesis by (simp add: eq_commute)
   1.272 +end
   1.273 +
   1.274 +class ab_group_add = minus + comm_monoid_add +
   1.275 +  assumes ab_left_minus: "- a + a = 0"
   1.276 +  assumes ab_diff_minus: "a - b = a + (- b)"
   1.277 +
   1.278 +subclass (in ab_group_add) group_add
   1.279 +  by unfold_locales (simp_all add: ab_left_minus ab_diff_minus)
   1.280 +
   1.281 +subclass (in ab_group_add) cancel_semigroup_add
   1.282 +proof unfold_locales
   1.283 +  fix a b c :: 'a
   1.284 +  assume "a + b = a + c"
   1.285 +  then have "- a + a + b = - a + a + c"
   1.286 +    unfolding add_assoc by simp
   1.287 +  then show "b = c" by simp
   1.288 +next
   1.289 +  fix a b c :: 'a
   1.290 +  assume "b + a = c + a"
   1.291 +  then have "b + (a + - a) = c + (a + - a)"
   1.292 +    unfolding add_assoc [symmetric] by simp
   1.293 +  then show "b = c" by simp
   1.294  qed
   1.295  
   1.296 -lemma minus_add_distrib [simp]: "- (a + b) = -a + -(b::'a::ab_group_add)"
   1.297 -apply (rule equals_zero_I)
   1.298 -apply (simp add: add_ac)
   1.299 -done
   1.300 +subclass (in ab_group_add) cancel_ab_semigroup_add
   1.301 +proof unfold_locales
   1.302 +  fix a b c :: 'a
   1.303 +  assume "a + b = a + c"
   1.304 +  then have "- a + a + b = - a + a + c"
   1.305 +    unfolding add_assoc by simp
   1.306 +  then show "b = c" by simp
   1.307 +qed
   1.308 +
   1.309 +context ab_group_add
   1.310 +begin
   1.311  
   1.312 -lemma minus_diff_eq [simp]: "- (a - b) = b - (a::'a::ab_group_add)"
   1.313 -by (simp add: diff_minus add_commute)
   1.314 +lemma uminus_add_conv_diff:
   1.315 +  "- a + b = b - a"
   1.316 +  by (simp add:diff_minus add_commute)
   1.317 +
   1.318 +lemma minus_add_distrib [simp]:
   1.319 +  "- (a + b) = - a + - b"
   1.320 +  by (rule equals_zero_I) (simp add: add_ac)
   1.321 +
   1.322 +lemma minus_diff_eq [simp]:
   1.323 +  "- (a - b) = b - a"
   1.324 +  by (simp add: diff_minus add_commute)
   1.325 +
   1.326 +end
   1.327  
   1.328  subsection {* (Partially) Ordered Groups *} 
   1.329  
   1.330  class pordered_ab_semigroup_add = order + ab_semigroup_add +
   1.331 -  assumes add_left_mono: "a \<^loc>\<le> b \<Longrightarrow> c \<^loc>+ a \<^loc>\<le> c \<^loc>+ b"
   1.332 -
   1.333 -class pordered_cancel_ab_semigroup_add =
   1.334 -  pordered_ab_semigroup_add + cancel_ab_semigroup_add
   1.335 -
   1.336 -class pordered_ab_semigroup_add_imp_le = pordered_cancel_ab_semigroup_add +
   1.337 -  assumes add_le_imp_le_left: "c \<^loc>+ a \<^loc>\<le> c \<^loc>+ b \<Longrightarrow> a \<^loc>\<le> b"
   1.338 -
   1.339 -class pordered_ab_group_add = ab_group_add + pordered_ab_semigroup_add
   1.340 -
   1.341 -instance pordered_ab_group_add \<subseteq> pordered_ab_semigroup_add_imp_le
   1.342 -proof
   1.343 -  fix a b c :: 'a
   1.344 -  assume "c + a \<le> c + b"
   1.345 -  hence "(-c) + (c + a) \<le> (-c) + (c + b)" by (rule add_left_mono)
   1.346 -  hence "((-c) + c) + a \<le> ((-c) + c) + b" by (simp only: add_assoc)
   1.347 -  thus "a \<le> b" by simp
   1.348 -qed
   1.349 -
   1.350 -class ordered_ab_semigroup_add =
   1.351 -  linorder + pordered_ab_semigroup_add
   1.352 +  assumes add_left_mono: "a \<le> b \<Longrightarrow> c + a \<le> c + b"
   1.353 +begin
   1.354  
   1.355 -class ordered_cancel_ab_semigroup_add =
   1.356 -  linorder + pordered_cancel_ab_semigroup_add
   1.357 -
   1.358 -instance ordered_cancel_ab_semigroup_add \<subseteq> ordered_ab_semigroup_add ..
   1.359 -
   1.360 -instance ordered_cancel_ab_semigroup_add \<subseteq> pordered_ab_semigroup_add_imp_le
   1.361 -proof
   1.362 -  fix a b c :: 'a
   1.363 -  assume le: "c + a <= c + b"  
   1.364 -  show "a <= b"
   1.365 -  proof (rule ccontr)
   1.366 -    assume w: "~ a \<le> b"
   1.367 -    hence "b <= a" by (simp add: linorder_not_le)
   1.368 -    hence le2: "c+b <= c+a" by (rule add_left_mono)
   1.369 -    have "a = b" 
   1.370 -      apply (insert le)
   1.371 -      apply (insert le2)
   1.372 -      apply (drule order_antisym, simp_all)
   1.373 -      done
   1.374 -    with w  show False 
   1.375 -      by (simp add: linorder_not_le [symmetric])
   1.376 -  qed
   1.377 -qed
   1.378 -
   1.379 -lemma add_right_mono: "a \<le> (b::'a::pordered_ab_semigroup_add) ==> a + c \<le> b + c"
   1.380 +lemma add_right_mono:
   1.381 +  "a \<le> b \<Longrightarrow> a + c \<le> b + c"
   1.382    by (simp add: add_commute [of _ c] add_left_mono)
   1.383  
   1.384  text {* non-strict, in both arguments *}
   1.385  lemma add_mono:
   1.386 -     "[|a \<le> b;  c \<le> d|] ==> a + c \<le> b + (d::'a::pordered_ab_semigroup_add)"
   1.387 +  "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c \<le> b + d"
   1.388    apply (erule add_right_mono [THEN order_trans])
   1.389    apply (simp add: add_commute add_left_mono)
   1.390    done
   1.391  
   1.392 +end
   1.393 +
   1.394 +class pordered_cancel_ab_semigroup_add =
   1.395 +  pordered_ab_semigroup_add + cancel_ab_semigroup_add
   1.396 +begin
   1.397 +
   1.398  lemma add_strict_left_mono:
   1.399 -     "a < b ==> c + a < c + (b::'a::pordered_cancel_ab_semigroup_add)"
   1.400 - by (simp add: order_less_le add_left_mono) 
   1.401 +  "a < b \<Longrightarrow> c + a < c + b"
   1.402 +  by (auto simp add: less_le add_left_mono)
   1.403  
   1.404  lemma add_strict_right_mono:
   1.405 -     "a < b ==> a + c < b + (c::'a::pordered_cancel_ab_semigroup_add)"
   1.406 - by (simp add: add_commute [of _ c] add_strict_left_mono)
   1.407 +  "a < b \<Longrightarrow> a + c < b + c"
   1.408 +  by (simp add: add_commute [of _ c] add_strict_left_mono)
   1.409  
   1.410  text{*Strict monotonicity in both arguments*}
   1.411 -lemma add_strict_mono: "[|a<b; c<d|] ==> a + c < b + (d::'a::pordered_cancel_ab_semigroup_add)"
   1.412 -apply (erule add_strict_right_mono [THEN order_less_trans])
   1.413 +lemma add_strict_mono:
   1.414 +  "a < b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
   1.415 +apply (erule add_strict_right_mono [THEN less_trans])
   1.416  apply (erule add_strict_left_mono)
   1.417  done
   1.418  
   1.419  lemma add_less_le_mono:
   1.420 -     "[| a<b; c\<le>d |] ==> a + c < b + (d::'a::pordered_cancel_ab_semigroup_add)"
   1.421 -apply (erule add_strict_right_mono [THEN order_less_le_trans])
   1.422 -apply (erule add_left_mono) 
   1.423 +  "a < b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c < b + d"
   1.424 +apply (erule add_strict_right_mono [THEN less_le_trans])
   1.425 +apply (erule add_left_mono)
   1.426  done
   1.427  
   1.428  lemma add_le_less_mono:
   1.429 -     "[| a\<le>b; c<d |] ==> a + c < b + (d::'a::pordered_cancel_ab_semigroup_add)"
   1.430 -apply (erule add_right_mono [THEN order_le_less_trans])
   1.431 +  "a \<le> b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
   1.432 +apply (erule add_right_mono [THEN le_less_trans])
   1.433  apply (erule add_strict_left_mono) 
   1.434  done
   1.435  
   1.436 +end
   1.437 +
   1.438 +class pordered_ab_semigroup_add_imp_le =
   1.439 +  pordered_cancel_ab_semigroup_add +
   1.440 +  assumes add_le_imp_le_left: "c + a \<le> c + b \<Longrightarrow> a \<le> b"
   1.441 +begin
   1.442 +
   1.443  lemma add_less_imp_less_left:
   1.444 -      assumes less: "c + a < c + b"  shows "a < (b::'a::pordered_ab_semigroup_add_imp_le)"
   1.445 +   assumes less: "c + a < c + b"
   1.446 +   shows "a < b"
   1.447  proof -
   1.448    from less have le: "c + a <= c + b" by (simp add: order_le_less)
   1.449    have "a <= b" 
   1.450 @@ -317,30 +343,90 @@
   1.451  qed
   1.452  
   1.453  lemma add_less_imp_less_right:
   1.454 -      "a + c < b + c ==> a < (b::'a::pordered_ab_semigroup_add_imp_le)"
   1.455 +  "a + c < b + c \<Longrightarrow> a < b"
   1.456  apply (rule add_less_imp_less_left [of c])
   1.457  apply (simp add: add_commute)  
   1.458  done
   1.459  
   1.460  lemma add_less_cancel_left [simp]:
   1.461 -    "(c+a < c+b) = (a < (b::'a::pordered_ab_semigroup_add_imp_le))"
   1.462 -by (blast intro: add_less_imp_less_left add_strict_left_mono) 
   1.463 +  "c + a < c + b \<longleftrightarrow> a < b"
   1.464 +  by (blast intro: add_less_imp_less_left add_strict_left_mono) 
   1.465  
   1.466  lemma add_less_cancel_right [simp]:
   1.467 -    "(a+c < b+c) = (a < (b::'a::pordered_ab_semigroup_add_imp_le))"
   1.468 -by (blast intro: add_less_imp_less_right add_strict_right_mono)
   1.469 +  "a + c < b + c \<longleftrightarrow> a < b"
   1.470 +  by (blast intro: add_less_imp_less_right add_strict_right_mono)
   1.471  
   1.472  lemma add_le_cancel_left [simp]:
   1.473 -    "(c+a \<le> c+b) = (a \<le> (b::'a::pordered_ab_semigroup_add_imp_le))"
   1.474 -by (auto, drule add_le_imp_le_left, simp_all add: add_left_mono) 
   1.475 +  "c + a \<le> c + b \<longleftrightarrow> a \<le> b"
   1.476 +  by (auto, drule add_le_imp_le_left, simp_all add: add_left_mono) 
   1.477  
   1.478  lemma add_le_cancel_right [simp]:
   1.479 -    "(a+c \<le> b+c) = (a \<le> (b::'a::pordered_ab_semigroup_add_imp_le))"
   1.480 -by (simp add: add_commute[of a c] add_commute[of b c])
   1.481 +  "a + c \<le> b + c \<longleftrightarrow> a \<le> b"
   1.482 +  by (simp add: add_commute [of a c] add_commute [of b c])
   1.483  
   1.484  lemma add_le_imp_le_right:
   1.485 -      "a + c \<le> b + c ==> a \<le> (b::'a::pordered_ab_semigroup_add_imp_le)"
   1.486 -by simp
   1.487 +  "a + c \<le> b + c \<Longrightarrow> a \<le> b"
   1.488 +  by simp
   1.489 +
   1.490 +end
   1.491 +
   1.492 +class pordered_ab_group_add =
   1.493 +  ab_group_add + pordered_ab_semigroup_add
   1.494 +begin
   1.495 +
   1.496 +subclass pordered_cancel_ab_semigroup_add
   1.497 +  by unfold_locales
   1.498 +
   1.499 +subclass pordered_ab_semigroup_add_imp_le
   1.500 +proof unfold_locales
   1.501 +  fix a b c :: 'a
   1.502 +  assume "c + a \<le> c + b"
   1.503 +  hence "(-c) + (c + a) \<le> (-c) + (c + b)" by (rule add_left_mono)
   1.504 +  hence "((-c) + c) + a \<le> ((-c) + c) + b" by (simp only: add_assoc)
   1.505 +  thus "a \<le> b" by simp
   1.506 +qed
   1.507 +
   1.508 +end
   1.509 +
   1.510 +class ordered_ab_semigroup_add =
   1.511 +  linorder + pordered_ab_semigroup_add
   1.512 +
   1.513 +class ordered_cancel_ab_semigroup_add =
   1.514 +  linorder + pordered_cancel_ab_semigroup_add
   1.515 +
   1.516 +subclass (in ordered_cancel_ab_semigroup_add) ordered_ab_semigroup_add
   1.517 +  by unfold_locales
   1.518 +
   1.519 +subclass (in ordered_cancel_ab_semigroup_add) pordered_ab_semigroup_add_imp_le
   1.520 +proof unfold_locales
   1.521 +  fix a b c :: 'a
   1.522 +  assume le: "c + a <= c + b"  
   1.523 +  show "a <= b"
   1.524 +  proof (rule ccontr)
   1.525 +    assume w: "~ a \<le> b"
   1.526 +    hence "b <= a" by (simp add: linorder_not_le)
   1.527 +    hence le2: "c + b <= c + a" by (rule add_left_mono)
   1.528 +    have "a = b" 
   1.529 +      apply (insert le)
   1.530 +      apply (insert le2)
   1.531 +      apply (drule antisym, simp_all)
   1.532 +      done
   1.533 +    with w show False 
   1.534 +      by (simp add: linorder_not_le [symmetric])
   1.535 +  qed
   1.536 +qed
   1.537 +
   1.538 +-- {* FIXME continue localization here *}
   1.539 +
   1.540 +lemma max_add_distrib_left:
   1.541 +  fixes z :: "'a::pordered_ab_semigroup_add_imp_le"
   1.542 +  shows  "(max x y) + z = max (x+z) (y+z)"
   1.543 +by (rule max_of_mono [THEN sym], rule add_le_cancel_right)
   1.544 +
   1.545 +lemma min_add_distrib_left:
   1.546 +  fixes z :: "'a::pordered_ab_semigroup_add_imp_le"
   1.547 +  shows  "(min x y) + z = min (x+z) (y+z)"
   1.548 +by (rule min_of_mono [THEN sym], rule add_le_cancel_right)
   1.549  
   1.550  lemma add_increasing:
   1.551    fixes c :: "'a::{pordered_ab_semigroup_add_imp_le, comm_monoid_add}"
   1.552 @@ -362,16 +448,6 @@
   1.553    shows "[|0\<le>a; b<c|] ==> b < a + c"
   1.554  by (insert add_le_less_mono [of 0 a b c], simp)
   1.555  
   1.556 -lemma max_add_distrib_left:
   1.557 -  fixes z :: "'a::pordered_ab_semigroup_add_imp_le"
   1.558 -  shows  "(max x y) + z = max (x+z) (y+z)"
   1.559 -by (rule max_of_mono [THEN sym], rule add_le_cancel_right)
   1.560 -
   1.561 -lemma min_add_distrib_left:
   1.562 -  fixes z :: "'a::pordered_ab_semigroup_add_imp_le"
   1.563 -  shows  "(min x y) + z = min (x+z) (y+z)"
   1.564 -by (rule min_of_mono [THEN sym], rule add_le_cancel_right)
   1.565 -
   1.566  lemma max_diff_distrib_left:
   1.567    fixes z :: "'a::pordered_ab_group_add"
   1.568    shows  "(max x y) - z = max (x-z) (y-z)"