# HG changeset patch
# User haftmann
# Date 1411928866 -7200
# Node ID 6a3da58f72331accf67c5df29a1fdbb8d781175f
# Parent  dde28333367ff5da6e6e4790b5584f2c33dec5bc
moved to HOL and generalized

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 \<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"
diff -r dde28333367f -r 6a3da58f7233 src/HOL/Library/Tree.thy
--- 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