--- a/src/HOL/Orderings.thy Tue Jun 10 15:30:56 2008 +0200
+++ b/src/HOL/Orderings.thy Tue Jun 10 15:30:58 2008 +0200
@@ -103,6 +103,28 @@
by (rule less_asym)
+text {* Least value operator *}
+
+definition
+ Least :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" (binder "LEAST " 10) where
+ "Least P = (THE x. P x \<and> (\<forall>y. P y \<longrightarrow> x \<le> y))"
+
+lemma Least_equality:
+ assumes "P x"
+ and "\<And>y. P y \<Longrightarrow> x \<le> y"
+ shows "Least P = x"
+unfolding Least_def by (rule the_equality)
+ (blast intro: assms antisym)+
+
+lemma LeastI2_order:
+ assumes "P x"
+ and "\<And>y. P y \<Longrightarrow> x \<le> y"
+ and "\<And>x. P x \<Longrightarrow> \<forall>y. P y \<longrightarrow> x \<le> y \<Longrightarrow> Q x"
+ shows "Q (Least P)"
+unfolding Least_def by (rule theI2)
+ (blast intro: assms antisym)+
+
+
text {* Dual order *}
lemma dual_order:
@@ -1052,16 +1074,6 @@
end
-lemma LeastI2_order:
- "[| P (x::'a::order);
- !!y. P y ==> x <= y;
- !!x. [| P x; ALL 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 min_leastL: "(!!x. least <= x) ==> min least x = least"
by (simp add: min_def)