localized Least in Orderings.thy
authorhaftmann
Tue Jun 10 15:30:58 2008 +0200 (2008-06-10)
changeset 271074a7415c67063
parent 27106 ff27dc6e7d05
child 27108 e447b3107696
localized Least in Orderings.thy
src/HOL/HOL.thy
src/HOL/Orderings.thy
     1.1 --- a/src/HOL/HOL.thy	Tue Jun 10 15:30:56 2008 +0200
     1.2 +++ b/src/HOL/HOL.thy	Tue Jun 10 15:30:58 2008 +0200
     1.3 @@ -29,7 +29,6 @@
     1.4    "~~/src/Tools/code/code_funcgr.ML"
     1.5    "~~/src/Tools/code/code_thingol.ML"
     1.6    "~~/src/Tools/code/code_target.ML"
     1.7 -  "~~/src/Tools/code/code_package.ML"
     1.8    "~~/src/Tools/nbe.ML"
     1.9  begin
    1.10  
    1.11 @@ -279,10 +278,6 @@
    1.12    greater  (infix ">" 50) where
    1.13    "x > y \<equiv> y < x"
    1.14  
    1.15 -definition
    1.16 -  Least :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" (binder "LEAST " 10) where
    1.17 -  "Least P == (THE x. P x \<and> (\<forall>y. P y \<longrightarrow> less_eq x y))"
    1.18 -
    1.19  end
    1.20  
    1.21  syntax
     2.1 --- a/src/HOL/Orderings.thy	Tue Jun 10 15:30:56 2008 +0200
     2.2 +++ b/src/HOL/Orderings.thy	Tue Jun 10 15:30:58 2008 +0200
     2.3 @@ -103,6 +103,28 @@
     2.4  by (rule less_asym)
     2.5  
     2.6  
     2.7 +text {* Least value operator *}
     2.8 +
     2.9 +definition
    2.10 +  Least :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" (binder "LEAST " 10) where
    2.11 +  "Least P = (THE x. P x \<and> (\<forall>y. P y \<longrightarrow> x \<le> y))"
    2.12 +
    2.13 +lemma Least_equality:
    2.14 +  assumes "P x"
    2.15 +    and "\<And>y. P y \<Longrightarrow> x \<le> y"
    2.16 +  shows "Least P = x"
    2.17 +unfolding Least_def by (rule the_equality)
    2.18 +  (blast intro: assms antisym)+
    2.19 +
    2.20 +lemma LeastI2_order:
    2.21 +  assumes "P x"
    2.22 +    and "\<And>y. P y \<Longrightarrow> x \<le> y"
    2.23 +    and "\<And>x. P x \<Longrightarrow> \<forall>y. P y \<longrightarrow> x \<le> y \<Longrightarrow> Q x"
    2.24 +  shows "Q (Least P)"
    2.25 +unfolding Least_def by (rule theI2)
    2.26 +  (blast intro: assms antisym)+
    2.27 +
    2.28 +
    2.29  text {* Dual order *}
    2.30  
    2.31  lemma dual_order:
    2.32 @@ -1052,16 +1074,6 @@
    2.33  
    2.34  end
    2.35  
    2.36 -lemma LeastI2_order:
    2.37 -  "[| P (x::'a::order);
    2.38 -      !!y. P y ==> x <= y;
    2.39 -      !!x. [| P x; ALL y. P y --> x \<le> y |] ==> Q x |]
    2.40 -   ==> Q (Least P)"
    2.41 -apply (unfold Least_def)
    2.42 -apply (rule theI2)
    2.43 -  apply (blast intro: order_antisym)+
    2.44 -done
    2.45 -
    2.46  lemma min_leastL: "(!!x. least <= x) ==> min least x = least"
    2.47  by (simp add: min_def)
    2.48