# HG changeset patch
# User fleury <Mathias.Fleury@mpi-inf.mpg.de>
# Date 1468324535 -7200
# Node ID 3365c8ec67bdc3e2fdf9a94920e755e522f0cf5b
# Parent  019856db2bb625f6011bd7ec75a55388a94c2349
sharing simp rules between ordered monoids and rings

diff -r 019856db2bb6 -r 3365c8ec67bd NEWS
--- 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
diff -r 019856db2bb6 -r 3365c8ec67bd src/HOL/Groups.thy
--- 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
 
diff -r 019856db2bb6 -r 3365c8ec67bd src/HOL/Nonstandard_Analysis/StarDef.thy
--- 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 ..
 
diff -r 019856db2bb6 -r 3365c8ec67bd src/HOL/Rings.thy
--- 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