# HG changeset patch
# User nipkow
# Date 863084699 -7200
# Node ID d60e49b86c6a2a4e8cf1f9d305971552e91211f1
# Parent  a6f73a02c619496178168c2b1e83f87fdeeecc49
Modified def of Least, which, as Markus correctly complained, looked like
Minimal. Derived the old def for nat in NatDef as Least_nat_def.

diff -r a6f73a02c619 -r d60e49b86c6a src/HOL/NatDef.ML
--- a/src/HOL/NatDef.ML	Thu May 08 10:20:37 1997 +0200
+++ b/src/HOL/NatDef.ML	Thu May 08 11:44:59 1997 +0200
@@ -556,7 +556,19 @@
 
 (** LEAST -- the least number operator **)
 
-val [prem1,prem2] = goalw thy [Least_def]
+goal thy "(! m::nat. P m --> n <= m) = (! m. m < n --> ~ P m)";
+by(blast_tac (!claset addIs [leI] addEs [leE]) 1);
+val lemma = result();
+
+(* This is an old def of Least for nat, which is derived for compatibility *)
+goalw thy [Least_def]
+  "(LEAST n::nat. P n) == (@n. P(n) & (ALL m. m < n --> ~P(m)))";
+by(simp_tac (!simpset addsimps [lemma]) 1);
+br eq_reflection 1;
+br refl 1;
+qed "Least_nat_def";
+
+val [prem1,prem2] = goalw thy [Least_nat_def]
     "[| P(k::nat);  !!x. x<k ==> ~P(x) |] ==> (LEAST x.P(x)) = k";
 by (rtac select_equality 1);
 by (blast_tac (!claset addSIs [prem1,prem2]) 1);
@@ -593,11 +605,11 @@
 by (rtac prem 1);
 qed "not_less_Least";
 
-qed_goalw "Least_Suc" thy [Least_def]
+qed_goalw "Least_Suc" thy [Least_nat_def]
  "!!P. [| ? n. P(Suc n); ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"
  (fn _ => [
         rtac select_equality 1,
-        fold_goals_tac [Least_def],
+        fold_goals_tac [Least_nat_def],
         safe_tac (!claset addSEs [LeastI]),
         rename_tac "j" 1,
         res_inst_tac [("n","j")] natE 1,
@@ -607,7 +619,7 @@
         res_inst_tac [("n","k")] natE 1,
         Blast_tac 1,
         hyp_subst_tac 1,
-        rewtac Least_def,
+        rewtac Least_nat_def,
         rtac (select_equality RS arg_cong RS sym) 1,
         safe_tac (!claset),
         dtac Suc_mono 1,
diff -r a6f73a02c619 -r d60e49b86c6a src/HOL/Ord.thy
--- a/src/HOL/Ord.thy	Thu May 08 10:20:37 1997 +0200
+++ b/src/HOL/Ord.thy	Thu May 08 11:44:59 1997 +0200
@@ -31,7 +31,7 @@
   mono_def      "mono(f) == (!A B. A <= B --> f(A) <= f(B))"
   min_def       "min a b == (if a <= b then a else b)"
   max_def       "max a b == (if a <= b then b else a)"
-  Least_def     "Least P == @x. P(x) & (ALL y. y<x --> ~P(y))"
+  Least_def     "Least P == @x. P(x) & (ALL y. P(y) --> x <= y)"
 
 
 axclass order < ord