diff -r dde28333367f -r 6a3da58f7233 src/HOL/Lattices_Big.thy --- a/src/HOL/Lattices_Big.thy Fri Sep 26 19:38:26 2014 +0200 +++ b/src/HOL/Lattices_Big.thy Sun Sep 28 20:27:46 2014 +0200 @@ -560,6 +560,30 @@ shows "Max A \ A" using assms by (auto simp add: max_def Max.closed) +lemma Min_insert2: + assumes "finite A" and min: "\b. b \ A \ a \ b" + shows "Min (insert a A) = a" +proof (cases "A = {}") + case True then show ?thesis by simp +next + case False with `finite A` have "Min (insert a A) = min a (Min A)" + by simp + moreover from `finite A` `A \ {}` min have "a \ Min A" by simp + ultimately show ?thesis by (simp add: min.absorb1) +qed + +lemma Max_insert2: + assumes "finite A" and max: "\b. b \ A \ b \ a" + shows "Max (insert a A) = a" +proof (cases "A = {}") + case True then show ?thesis by simp +next + case False with `finite A` have "Max (insert a A) = max a (Max A)" + by simp + moreover from `finite A` `A \ {}` max have "Max A \ a" by simp + ultimately show ?thesis by (simp add: max.absorb1) +qed + lemma Min_le [simp]: assumes "finite A" and "x \ A" shows "Min A \ x"