1.1 --- a/src/HOL/Orderings.thy	Tue Jun 10 15:30:56 2008 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Tue Jun 10 15:30:58 2008 +0200
     1.3 @@ -103,6 +103,28 @@
     1.4  by (rule less_asym)
     1.5  
     1.6  
     1.7 +text {* Least value operator *}
     1.8 +
     1.9 +definition
    1.10 +  Least :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" (binder "LEAST " 10) where
    1.11 +  "Least P = (THE x. P x \<and> (\<forall>y. P y \<longrightarrow> x \<le> y))"
    1.12 +
    1.13 +lemma Least_equality:
    1.14 +  assumes "P x"
    1.15 +    and "\<And>y. P y \<Longrightarrow> x \<le> y"
    1.16 +  shows "Least P = x"
    1.17 +unfolding Least_def by (rule the_equality)
    1.18 +  (blast intro: assms antisym)+
    1.19 +
    1.20 +lemma LeastI2_order:
    1.21 +  assumes "P x"
    1.22 +    and "\<And>y. P y \<Longrightarrow> x \<le> y"
    1.23 +    and "\<And>x. P x \<Longrightarrow> \<forall>y. P y \<longrightarrow> x \<le> y \<Longrightarrow> Q x"
    1.24 +  shows "Q (Least P)"
    1.25 +unfolding Least_def by (rule theI2)
    1.26 +  (blast intro: assms antisym)+
    1.27 +
    1.28 +
    1.29  text {* Dual order *}
    1.30  
    1.31  lemma dual_order:
    1.32 @@ -1052,16 +1074,6 @@
    1.33  
    1.34  end
    1.35  
    1.36 -lemma LeastI2_order:
    1.37 -  "[| P (x::'a::order);
    1.38 -      !!y. P y ==> x <= y;
    1.39 -      !!x. [| P x; ALL y. P y --> x \<le> y |] ==> Q x |]
    1.40 -   ==> Q (Least P)"
    1.41 -apply (unfold Least_def)
    1.42 -apply (rule theI2)
    1.43 -  apply (blast intro: order_antisym)+
    1.44 -done
    1.45 -
    1.46  lemma min_leastL: "(!!x. least <= x) ==> min least x = least"
    1.47  by (simp add: min_def)
    1.48