1.1 --- a/src/HOL/Orderings.thy	Mon Aug 23 19:35:57 2010 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Tue Aug 24 14:41:37 2010 +0200
     1.3 @@ -1154,7 +1154,7 @@
     1.4        have "\<And>y. P y \<Longrightarrow> x \<le> y"
     1.5        proof (rule classical)
     1.6          fix y
     1.7 -        assume "P y" and "\<not> x \<le> y" 
     1.8 +        assume "P y" and "\<not> x \<le> y"
     1.9          with less have "P (LEAST a. P a)" and "(LEAST a. P a) \<le> y"
    1.10            by (auto simp add: not_le)
    1.11          with assm have "x < (LEAST a. P a)" and "(LEAST a. P a) \<le> y"
    1.12 @@ -1181,13 +1181,25 @@
    1.13    "\<exists>a. P a \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> Q (Least P)"
    1.14    by (blast intro: LeastI_ex)
    1.15  
    1.16 +lemma LeastI2_wellorder:
    1.17 +  assumes "P a"
    1.18 +  and "\<And>a. \<lbrakk> P a; \<forall>b. P b \<longrightarrow> a \<le> b \<rbrakk> \<Longrightarrow> Q a"
    1.19 +  shows "Q (Least P)"
    1.20 +proof (rule LeastI2_order)
    1.21 +  show "P (Least P)" using `P a` by (rule LeastI)
    1.22 +next
    1.23 +  fix y assume "P y" thus "Least P \<le> y" by (rule Least_le)
    1.24 +next
    1.25 +  fix x assume "P x" "\<forall>y. P y \<longrightarrow> x \<le> y" thus "Q x" by (rule assms(2))
    1.26 +qed
    1.27 +
    1.28  lemma not_less_Least: "k < (LEAST x. P x) \<Longrightarrow> \<not> P k"
    1.29  apply (simp (no_asm_use) add: not_le [symmetric])
    1.30  apply (erule contrapos_nn)
    1.31  apply (erule Least_le)
    1.32  done
    1.33  
    1.34 -end  
    1.35 +end
    1.36  
    1.37  
    1.38  subsection {* Order on bool *}