--- 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 \<in> A"
using assms by (auto simp add: max_def Max.closed)
+lemma Min_insert2:
+ assumes "finite A" and min: "\<And>b. b \<in> A \<Longrightarrow> a \<le> 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 \<noteq> {}` min have "a \<le> Min A" by simp
+ ultimately show ?thesis by (simp add: min.absorb1)
+qed
+
+lemma Max_insert2:
+ assumes "finite A" and max: "\<And>b. b \<in> A \<Longrightarrow> b \<le> 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 \<noteq> {}` max have "Max A \<le> a" by simp
+ ultimately show ?thesis by (simp add: max.absorb1)
+qed
+
lemma Min_le [simp]:
assumes "finite A" and "x \<in> A"
shows "Min A \<le> x"
--- a/src/HOL/Library/Tree.thy Fri Sep 26 19:38:26 2014 +0200
+++ b/src/HOL/Library/Tree.thy Sun Sep 28 20:27:46 2014 +0200
@@ -107,12 +107,8 @@
by (fastforce simp add: ball_Un)
qed simp_all
-(* should be moved but metis not available in much of Main *)
-lemma Max_insert1: "\<lbrakk> finite A; \<forall>a\<in>A. a \<le> x \<rbrakk> \<Longrightarrow> Max(insert x A) = x"
-by (metis Max_in Max_insert Max_singleton antisym max_def)
-
lemma del_rightmost_Max:
"\<lbrakk> del_rightmost t = (t',x); bst t; t \<noteq> \<langle>\<rangle> \<rbrakk> \<Longrightarrow> x = Max(set_tree t)"
-by (metis Max_insert1 del_rightmost_greater del_rightmost_set_tree finite_set_tree less_le_not_le)
+by (metis Max_insert2 del_rightmost_greater del_rightmost_set_tree finite_set_tree less_le_not_le)
end