src/HOL/Groups.thy
changeset 63456 3365c8ec67bd
parent 63364 4fa441c2f20c
child 63588 d0e2bad67bd4
     1.1 --- a/src/HOL/Groups.thy	Tue Jul 12 11:51:05 2016 +0200
     1.2 +++ b/src/HOL/Groups.thy	Tue Jul 12 13:55:35 2016 +0200
     1.3 @@ -800,12 +800,55 @@
     1.4  
     1.5  end
     1.6  
     1.7 +class ordered_ab_semigroup_monoid_add_imp_le = monoid_add + ordered_ab_semigroup_add_imp_le
     1.8 +begin
     1.9 +
    1.10 +lemma add_less_same_cancel1 [simp]:
    1.11 +  "b + a < b \<longleftrightarrow> a < 0"
    1.12 +  using add_less_cancel_left [of _ _ 0] by simp
    1.13 +
    1.14 +lemma add_less_same_cancel2 [simp]:
    1.15 +  "a + b < b \<longleftrightarrow> a < 0"
    1.16 +  using add_less_cancel_right [of _ _ 0] by simp
    1.17 +
    1.18 +lemma less_add_same_cancel1 [simp]:
    1.19 +  "a < a + b \<longleftrightarrow> 0 < b"
    1.20 +  using add_less_cancel_left [of _ 0] by simp
    1.21 +
    1.22 +lemma less_add_same_cancel2 [simp]:
    1.23 +  "a < b + a \<longleftrightarrow> 0 < b"
    1.24 +  using add_less_cancel_right [of 0] by simp
    1.25 +
    1.26 +lemma add_le_same_cancel1 [simp]:
    1.27 +  "b + a \<le> b \<longleftrightarrow> a \<le> 0"
    1.28 +  using add_le_cancel_left [of _ _ 0] by simp
    1.29 +
    1.30 +lemma add_le_same_cancel2 [simp]:
    1.31 +  "a + b \<le> b \<longleftrightarrow> a \<le> 0"
    1.32 +  using add_le_cancel_right [of _ _ 0] by simp
    1.33 +
    1.34 +lemma le_add_same_cancel1 [simp]:
    1.35 +  "a \<le> a + b \<longleftrightarrow> 0 \<le> b"
    1.36 +  using add_le_cancel_left [of _ 0] by simp
    1.37 +
    1.38 +lemma le_add_same_cancel2 [simp]:
    1.39 +  "a \<le> b + a \<longleftrightarrow> 0 \<le> b"
    1.40 +  using add_le_cancel_right [of 0] by simp
    1.41 +
    1.42 +subclass cancel_comm_monoid_add
    1.43 +  by standard auto
    1.44 +
    1.45 +subclass ordered_cancel_comm_monoid_add
    1.46 +  by standard
    1.47 +
    1.48 +end
    1.49 +
    1.50  class ordered_ab_group_add = ab_group_add + ordered_ab_semigroup_add
    1.51  begin
    1.52  
    1.53  subclass ordered_cancel_ab_semigroup_add ..
    1.54  
    1.55 -subclass ordered_ab_semigroup_add_imp_le
    1.56 +subclass ordered_ab_semigroup_monoid_add_imp_le
    1.57  proof
    1.58    fix a b c :: 'a
    1.59    assume "c + a \<le> c + b"
    1.60 @@ -816,32 +859,6 @@
    1.61    then show "a \<le> b" by simp
    1.62  qed
    1.63  
    1.64 -subclass ordered_cancel_comm_monoid_add ..
    1.65 -
    1.66 -lemma add_less_same_cancel1 [simp]: "b + a < b \<longleftrightarrow> a < 0"
    1.67 -  using add_less_cancel_left [of _ _ 0] by simp
    1.68 -
    1.69 -lemma add_less_same_cancel2 [simp]: "a + b < b \<longleftrightarrow> a < 0"
    1.70 -  using add_less_cancel_right [of _ _ 0] by simp
    1.71 -
    1.72 -lemma less_add_same_cancel1 [simp]: "a < a + b \<longleftrightarrow> 0 < b"
    1.73 -  using add_less_cancel_left [of _ 0] by simp
    1.74 -
    1.75 -lemma less_add_same_cancel2 [simp]: "a < b + a \<longleftrightarrow> 0 < b"
    1.76 -  using add_less_cancel_right [of 0] by simp
    1.77 -
    1.78 -lemma add_le_same_cancel1 [simp]: "b + a \<le> b \<longleftrightarrow> a \<le> 0"
    1.79 -  using add_le_cancel_left [of _ _ 0] by simp
    1.80 -
    1.81 -lemma add_le_same_cancel2 [simp]: "a + b \<le> b \<longleftrightarrow> a \<le> 0"
    1.82 -  using add_le_cancel_right [of _ _ 0] by simp
    1.83 -
    1.84 -lemma le_add_same_cancel1 [simp]: "a \<le> a + b \<longleftrightarrow> 0 \<le> b"
    1.85 -  using add_le_cancel_left [of _ 0] by simp
    1.86 -
    1.87 -lemma le_add_same_cancel2 [simp]: "a \<le> b + a \<longleftrightarrow> 0 \<le> b"
    1.88 -  using add_le_cancel_right [of 0] by simp
    1.89 -
    1.90  lemma max_diff_distrib_left: "max x y - z = max (x - z) (y - z)"
    1.91    using max_add_distrib_left [of x y "- z"] by simp
    1.92