# HG changeset patch
# User nipkow
# Date 1535028576 -7200
# Node ID 462226db648aef8aa75267f5d034f60d6bf02a6e
# Parent  d2470f3a768b27d860cb22e0ddea30c772050945
tuned lemmas

diff -r d2470f3a768b -r 462226db648a src/HOL/Lattices_Big.thy
--- a/src/HOL/Lattices_Big.thy	Thu Aug 23 07:02:29 2018 +0200
+++ b/src/HOL/Lattices_Big.thy	Thu Aug 23 14:49:36 2018 +0200
@@ -800,24 +800,28 @@
 
 lemma Min_add_commute:
   fixes k
-  assumes "finite N" and "N \<noteq> {}"
-  shows "Min ((+) k ` N) = k + Min N"
+  assumes "finite S" and "S \<noteq> {}"
+  shows "Min ((\<lambda>x. f x + k) ` S) = Min(f ` S) + k"
 proof -
-  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 "(+) k" N, symmetric] by simp
+  have m: "\<And>x y. min x y + k = min (x+k) (y+k)"
+    by(simp add: min_def antisym add_right_mono)
+  have "(\<lambda>x. f x + k) ` S = (\<lambda>y. y + k) ` (f ` S)" by auto
+  also have "Min \<dots> = Min (f ` S) + k"
+    using assms hom_Min_commute [of "\<lambda>y. y+k" "f ` S", OF m, symmetric] by simp
+  finally show ?thesis by simp
 qed
 
 lemma Max_add_commute:
   fixes k
-  assumes "finite N" and "N \<noteq> {}"
-  shows "Max ((+) k ` N) = k + Max N"
+  assumes "finite S" and "S \<noteq> {}"
+  shows "Max ((\<lambda>x. f x + k) ` S) = Max(f ` S) + k"
 proof -
-  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 "(+) k" N, symmetric] by simp
+  have m: "\<And>x y. max x y + k = max (x+k) (y+k)"
+    by(simp add: max_def antisym add_right_mono)
+  have "(\<lambda>x. f x + k) ` S = (\<lambda>y. y + k) ` (f ` S)" by auto
+  also have "Max \<dots> = Max (f ` S) + k"
+    using assms hom_Max_commute [of "\<lambda>y. y+k" "f ` S", OF m, symmetric] by simp
+  finally show ?thesis by simp
 qed
 
 end