author nipkow Wed, 22 Aug 2018 16:41:10 +0200 changeset 68788 d4426a23832e parent 68779 78d9b1783378 child 68789 9270af426282
tuned lemmas
 src/HOL/Lattices_Big.thy file | annotate | diff | comparison | revisions
```--- 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 @@
begin

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

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)"
+  have "\<And>x y. k + max x y = max (k+x) (k+y)"
with assms show ?thesis
-    using hom_Max_commute [of "\<lambda>x. x+k" N, symmetric] by simp
-qed
-
-  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```