# HG changeset patch
# User haftmann
# Date 1213104658 -7200
# Node ID 4a7415c670636e76dfb9525ccfebfad4fa5360e6
# Parent  ff27dc6e7d05ebd6e31651763f0e31dac17b2fb6
localized Least in Orderings.thy

diff -r ff27dc6e7d05 -r 4a7415c67063 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Jun 10 15:30:56 2008 +0200
+++ b/src/HOL/HOL.thy	Tue Jun 10 15:30:58 2008 +0200
@@ -29,7 +29,6 @@
   "~~/src/Tools/code/code_funcgr.ML"
   "~~/src/Tools/code/code_thingol.ML"
   "~~/src/Tools/code/code_target.ML"
-  "~~/src/Tools/code/code_package.ML"
   "~~/src/Tools/nbe.ML"
 begin
 
@@ -279,10 +278,6 @@
   greater  (infix ">" 50) where
   "x > y \<equiv> y < x"
 
-definition
-  Least :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" (binder "LEAST " 10) where
-  "Least P == (THE x. P x \<and> (\<forall>y. P y \<longrightarrow> less_eq x y))"
-
 end
 
 syntax
diff -r ff27dc6e7d05 -r 4a7415c67063 src/HOL/Orderings.thy
--- 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)