# 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 \ {}" - shows "Min ((+) k ` N) = k + Min N" + assumes "finite S" and "S \ {}" + shows "Min ((\x. f x + k) ` S) = Min(f ` S) + k" proof - - have "\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: "\x y. min x y + k = min (x+k) (y+k)" + by(simp add: min_def antisym add_right_mono) + have "(\x. f x + k) ` S = (\y. y + k) ` (f ` S)" by auto + also have "Min \ = Min (f ` S) + k" + using assms hom_Min_commute [of "\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 \ {}" - shows "Max ((+) k ` N) = k + Max N" + assumes "finite S" and "S \ {}" + shows "Max ((\x. f x + k) ` S) = Max(f ` S) + k" proof - - have "\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: "\x y. max x y + k = max (x+k) (y+k)" + by(simp add: max_def antisym add_right_mono) + have "(\x. f x + k) ` S = (\y. y + k) ` (f ` S)" by auto + also have "Max \ = Max (f ` S) + k" + using assms hom_Max_commute [of "\y. y+k" "f ` S", OF m, symmetric] by simp + finally show ?thesis by simp qed end