author nipkow Thu, 23 Aug 2018 14:49:36 +0200 changeset 68793 462226db648a parent 68792 d2470f3a768b child 68794 63e84bd8e1f6
tuned lemmas
 src/HOL/Lattices_Big.thy file | annotate | diff | comparison | revisions
```--- 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 @@

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)"
-  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)"
+  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

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)"