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"