# HG changeset patch
# User nipkow
# Date 1534948870 -7200
# Node ID d4426a23832e41829514433b0b14f2249c0a66fd
# Parent  78d9b1783378ecb4251773ba933b56358dd9cddd
tuned lemmas

diff -r 78d9b1783378 -r d4426a23832e src/HOL/Lattices_Big.thy
--- a/src/HOL/Lattices_Big.thy	Wed Aug 22 12:31:57 2018 +0200
+++ b/src/HOL/Lattices_Big.thy	Wed Aug 22 16:41:10 2018 +0200
@@ -798,41 +798,26 @@
 context linordered_ab_semigroup_add
 begin
 
-lemma add_Min_commute:
+lemma Min_add_commute:
   fixes k
   assumes "finite N" and "N \<noteq> {}"
-  shows "k + Min N = Min {k + m | m. m \<in> N}"
+  shows "Min ((+) k ` N) = k + Min N"
 proof -
-  have "\<And>x y. k + min x y = min (k + x) (k + y)"
-    by (simp add: min_def not_le)
-      (blast intro: antisym less_imp_le add_left_mono)
+  have "\<And>x y. k + min x y = min (k+x) (k+y)"
+    by(simp add: min_def antisym add_left_mono)
   with assms show ?thesis
-    using hom_Min_commute [of "plus k" N]
-    by simp (blast intro: arg_cong [where f = Min])
+    using hom_Min_commute [of "(+) k" N, symmetric] by simp
 qed
 
 lemma Max_add_commute:
   fixes k
   assumes "finite N" and "N \<noteq> {}"
-  shows "Max((\<lambda>x. x+k) ` N) = Max N + k"
+  shows "Max ((+) k ` N) = k + Max N"
 proof -
-  have "\<And>x y. max x y + k = max (x+k) (y+k)"
-    by(simp add: max_def antisym add_right_mono)
+  have "\<And>x y. k + max x y = max (k+x) (k+y)"
+    by(simp add: max_def antisym add_left_mono)
   with assms show ?thesis
-    using hom_Max_commute [of "\<lambda>x. x+k" N, symmetric] by simp
-qed
-
-lemma add_Max_commute:
-  fixes k
-  assumes "finite N" and "N \<noteq> {}"
-  shows "k + Max N = Max {k + m | m. m \<in> N}"
-proof -
-  have "\<And>x y. k + max x y = max (k + x) (k + y)"
-    by (simp add: max_def not_le)
-      (blast intro: antisym less_imp_le add_left_mono)
-  with assms show ?thesis
-    using hom_Max_commute [of "plus k" N]
-    by simp (blast intro: arg_cong [where f = Max])
+    using hom_Max_commute [of "(+) k" N, symmetric] by simp
 qed
 
 end