--- a/src/HOL/Ord.thy Wed Jul 25 13:44:32 2001 +0200
+++ b/src/HOL/Ord.thy Wed Jul 25 17:58:26 2001 +0200
@@ -173,6 +173,16 @@
Least :: "('a::ord => bool) => 'a" (binder "LEAST " 10)
"Least P == THE x. P x & (ALL y. P y --> x <= y)"
+lemma LeastI2:
+ "[| P (x::'a::order);
+ !!y. P y ==> x <= y;
+ !!x. [| P x; \\<forall>y. P y --> x \\<le> y |] ==> Q x |]
+ ==> Q (Least P)";
+apply (unfold Least_def)
+apply (rule theI2)
+ apply (blast intro: order_antisym)+
+done
+
lemma Least_equality:
"[| P (k::'a::order); !!x. P x ==> k <= x |] ==> (LEAST x. P x) = k";
apply (simp add: Least_def)
@@ -180,7 +190,6 @@
apply (auto intro!: order_antisym)
done
-
section "Linear/Total Orders"
axclass linorder < order