--- a/NEWS Tue Jul 12 11:51:05 2016 +0200
+++ b/NEWS Tue Jul 12 13:55:35 2016 +0200
@@ -254,6 +254,29 @@
* Removed obsolete theorem nat_less_cases. INCOMPATIBILITY, use
linorder_cases instead.
+* Some theorems about groups and orders have been generalised from
+ groups to semi-groups that are also monoids:
+ le_add_same_cancel1
+ le_add_same_cancel2
+ less_add_same_cancel1
+ less_add_same_cancel2
+ add_le_same_cancel1
+ add_le_same_cancel2
+ add_less_same_cancel1
+ add_less_same_cancel2
+
+* Some simplifications theorems about rings have been removed, since
+ superseeded by a more general version:
+ less_add_cancel_left_greater_zero ~> less_add_same_cancel1
+ less_add_cancel_right_greater_zero ~> less_add_same_cancel2
+ less_eq_add_cancel_left_greater_eq_zero ~> le_add_same_cancel1
+ less_eq_add_cancel_right_greater_eq_zero ~> le_add_same_cancel2
+ less_eq_add_cancel_left_less_eq_zero ~> add_le_same_cancel1
+ less_eq_add_cancel_right_less_eq_zero ~> add_le_same_cancel2
+ less_add_cancel_left_less_zero ~> add_less_same_cancel1
+ less_add_cancel_right_less_zero ~> add_less_same_cancel2
+INCOMPATIBILITY.
+
* Renamed split_if -> if_split and split_if_asm -> if_split_asm to
resemble the f.split naming convention, INCOMPATIBILITY.
@@ -398,6 +421,12 @@
* Introduced the type classes canonically_ordered_comm_monoid_add and dioid.
+* Introduced the type class ordered_ab_semigroup_monoid_add_imp_le. When
+instantiating linordered_semiring_strict and ordered_ab_group_add, an explicit
+instantiation of ordered_ab_semigroup_monoid_add_imp_le might be
+required.
+INCOMPATIBILITY.
+
* Added topological_monoid
* Library/Complete_Partial_Order2.thy provides reasoning support for
--- a/src/HOL/Groups.thy Tue Jul 12 11:51:05 2016 +0200
+++ b/src/HOL/Groups.thy Tue Jul 12 13:55:35 2016 +0200
@@ -800,12 +800,55 @@
end
+class ordered_ab_semigroup_monoid_add_imp_le = monoid_add + ordered_ab_semigroup_add_imp_le
+begin
+
+lemma add_less_same_cancel1 [simp]:
+ "b + a < b \<longleftrightarrow> a < 0"
+ using add_less_cancel_left [of _ _ 0] by simp
+
+lemma add_less_same_cancel2 [simp]:
+ "a + b < b \<longleftrightarrow> a < 0"
+ using add_less_cancel_right [of _ _ 0] by simp
+
+lemma less_add_same_cancel1 [simp]:
+ "a < a + b \<longleftrightarrow> 0 < b"
+ using add_less_cancel_left [of _ 0] by simp
+
+lemma less_add_same_cancel2 [simp]:
+ "a < b + a \<longleftrightarrow> 0 < b"
+ using add_less_cancel_right [of 0] by simp
+
+lemma add_le_same_cancel1 [simp]:
+ "b + a \<le> b \<longleftrightarrow> a \<le> 0"
+ using add_le_cancel_left [of _ _ 0] by simp
+
+lemma add_le_same_cancel2 [simp]:
+ "a + b \<le> b \<longleftrightarrow> a \<le> 0"
+ using add_le_cancel_right [of _ _ 0] by simp
+
+lemma le_add_same_cancel1 [simp]:
+ "a \<le> a + b \<longleftrightarrow> 0 \<le> b"
+ using add_le_cancel_left [of _ 0] by simp
+
+lemma le_add_same_cancel2 [simp]:
+ "a \<le> b + a \<longleftrightarrow> 0 \<le> b"
+ using add_le_cancel_right [of 0] by simp
+
+subclass cancel_comm_monoid_add
+ by standard auto
+
+subclass ordered_cancel_comm_monoid_add
+ by standard
+
+end
+
class ordered_ab_group_add = ab_group_add + ordered_ab_semigroup_add
begin
subclass ordered_cancel_ab_semigroup_add ..
-subclass ordered_ab_semigroup_add_imp_le
+subclass ordered_ab_semigroup_monoid_add_imp_le
proof
fix a b c :: 'a
assume "c + a \<le> c + b"
@@ -816,32 +859,6 @@
then show "a \<le> b" by simp
qed
-subclass ordered_cancel_comm_monoid_add ..
-
-lemma add_less_same_cancel1 [simp]: "b + a < b \<longleftrightarrow> a < 0"
- using add_less_cancel_left [of _ _ 0] by simp
-
-lemma add_less_same_cancel2 [simp]: "a + b < b \<longleftrightarrow> a < 0"
- using add_less_cancel_right [of _ _ 0] by simp
-
-lemma less_add_same_cancel1 [simp]: "a < a + b \<longleftrightarrow> 0 < b"
- using add_less_cancel_left [of _ 0] by simp
-
-lemma less_add_same_cancel2 [simp]: "a < b + a \<longleftrightarrow> 0 < b"
- using add_less_cancel_right [of 0] by simp
-
-lemma add_le_same_cancel1 [simp]: "b + a \<le> b \<longleftrightarrow> a \<le> 0"
- using add_le_cancel_left [of _ _ 0] by simp
-
-lemma add_le_same_cancel2 [simp]: "a + b \<le> b \<longleftrightarrow> a \<le> 0"
- using add_le_cancel_right [of _ _ 0] by simp
-
-lemma le_add_same_cancel1 [simp]: "a \<le> a + b \<longleftrightarrow> 0 \<le> b"
- using add_le_cancel_left [of _ 0] by simp
-
-lemma le_add_same_cancel2 [simp]: "a \<le> b + a \<longleftrightarrow> 0 \<le> b"
- using add_le_cancel_right [of 0] by simp
-
lemma max_diff_distrib_left: "max x y - z = max (x - z) (y - z)"
using max_add_distrib_left [of x y "- z"] by simp
--- a/src/HOL/Nonstandard_Analysis/StarDef.thy Tue Jul 12 11:51:05 2016 +0200
+++ b/src/HOL/Nonstandard_Analysis/StarDef.thy Tue Jul 12 13:55:35 2016 +0200
@@ -806,6 +806,7 @@
by (intro_classes, transfer, rule add_le_imp_le_left)
instance star :: (ordered_comm_monoid_add) ordered_comm_monoid_add ..
+instance star :: (ordered_ab_semigroup_monoid_add_imp_le) ordered_ab_semigroup_monoid_add_imp_le ..
instance star :: (ordered_cancel_comm_monoid_add) ordered_cancel_comm_monoid_add ..
instance star :: (ordered_ab_group_add) ordered_ab_group_add ..
--- a/src/HOL/Rings.thy Tue Jul 12 11:51:05 2016 +0200
+++ b/src/HOL/Rings.thy Tue Jul 12 13:55:35 2016 +0200
@@ -1292,36 +1292,14 @@
subclass ordered_cancel_comm_monoid_add ..
+subclass ordered_ab_semigroup_monoid_add_imp_le ..
+
lemma mult_left_less_imp_less: "c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
by (force simp add: mult_left_mono not_le [symmetric])
lemma mult_right_less_imp_less: "a * c < b * c \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
by (force simp add: mult_right_mono not_le [symmetric])
-lemma less_eq_add_cancel_left_greater_eq_zero [simp]: "a \<le> a + b \<longleftrightarrow> 0 \<le> b"
- using add_le_cancel_left [of a 0 b] by simp
-
-lemma less_eq_add_cancel_left_less_eq_zero [simp]: "a + b \<le> a \<longleftrightarrow> b \<le> 0"
- using add_le_cancel_left [of a b 0] by simp
-
-lemma less_eq_add_cancel_right_greater_eq_zero [simp]: "a \<le> b + a \<longleftrightarrow> 0 \<le> b"
- using add_le_cancel_right [of 0 a b] by simp
-
-lemma less_eq_add_cancel_right_less_eq_zero [simp]: "b + a \<le> a \<longleftrightarrow> b \<le> 0"
- using add_le_cancel_right [of b a 0] by simp
-
-lemma less_add_cancel_left_greater_zero [simp]: "a < a + b \<longleftrightarrow> 0 < b"
- using add_less_cancel_left [of a 0 b] by simp
-
-lemma less_add_cancel_left_less_zero [simp]: "a + b < a \<longleftrightarrow> b < 0"
- using add_less_cancel_left [of a b 0] by simp
-
-lemma less_add_cancel_right_greater_zero [simp]: "a < b + a \<longleftrightarrow> 0 < b"
- using add_less_cancel_right [of 0 a b] by simp
-
-lemma less_add_cancel_right_less_zero [simp]: "b + a < a \<longleftrightarrow> b < 0"
- using add_less_cancel_right [of b a 0] by simp
-
end
class linordered_semiring_1 = linordered_semiring + semiring_1