# HG changeset patch
# User nipkow
# Date 1534933917 -7200
# Node ID 78d9b1783378ecb4251773ba933b56358dd9cddd
# Parent  4566bac4517dff708d12ff4169baabdefd7bdc58
copied but not adapted

diff -r 4566bac4517d -r 78d9b1783378 src/HOL/Lattices_Big.thy
--- a/src/HOL/Lattices_Big.thy	Tue Aug 21 17:29:46 2018 +0200
+++ b/src/HOL/Lattices_Big.thy	Wed Aug 22 12:31:57 2018 +0200
@@ -499,8 +499,8 @@
   "MAX x\<in>A. B"   \<rightleftharpoons> "CONST MAXIMUM A (\<lambda>x. B)"
 
 print_translation \<open>
-  [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INFIMUM} @{syntax_const "_INF"},
-    Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax SUPREMUM} @{syntax_const "_SUP"}]
+  [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax MINIMUM} @{syntax_const "_MIN"},
+    Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax MAXIMUM} @{syntax_const "_MAX"}]
 \<close> \<comment> \<open>to avoid eta-contraction of body\<close>
 
 text \<open>An aside: @{const Min}/@{const Max} on linear orders as special case of @{const Inf_fin}/@{const Sup_fin}\<close>
@@ -811,6 +811,17 @@
     by simp (blast intro: arg_cong [where f = Min])
 qed
 
+lemma Max_add_commute:
+  fixes k
+  assumes "finite N" and "N \<noteq> {}"
+  shows "Max((\<lambda>x. x+k) ` N) = Max N + k"
+proof -
+  have "\<And>x y. max x y + k = max (x+k) (y+k)"
+    by(simp add: max_def antisym add_right_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> {}"