New lemmas by Stefan Merz.

--- a/src/HOL/NatDef.ML	Thu Jul 22 20:53:54 1999 +0200
+++ b/src/HOL/NatDef.ML	Fri Jul 23 12:10:42 1999 +0200
@@ -519,3 +519,12 @@
 
 (* [| m ~= n; m < n ==> P; n < m ==> P |] ==> P *)
 bind_thm("nat_neqE", nat_neq_iff RS iffD1 RS disjE);
+
+Goal "(S::nat set) ~= {} ==> ? x:S. ! y:S. x <= y";
+by (cut_facts_tac [wf_pred_nat RS wf_trancl RS (wf_eq_minimal RS iffD1)] 1);
+by (dres_inst_tac [("x","S")] spec 1);
+by (Asm_full_simp_tac 1);
+by (etac impE 1);
+by (Force_tac 1);
+by (force_tac (claset(), simpset() addsimps [less_eq,not_le_iff_less]) 1);
+qed "nonempty_has_least";

--- a/src/HOL/mono.ML	Thu Jul 22 20:53:54 1999 +0200
+++ b/src/HOL/mono.ML	Fri Jul 23 12:10:42 1999 +0200
@@ -105,3 +105,14 @@
 val basic_monos = [subset_refl, imp_refl, disj_mono, conj_mono, 
                    ex_mono, Collect_mono, in_mono];
 
+(* Courtesy of Stefan Merz *)
+Goalw [Least_def,mono_def]
+  "[| mono (f::'a::order => 'b::order); ? x:S. ! y:S. x <= y |] \
+\  ==> (LEAST y. y : f``S) = f(LEAST x. x : S)";
+by (etac bexE 1);
+by (rtac selectI2 1);
+by (Force_tac 1);
+by (rtac select_equality 1);
+by (Force_tac 1);
+by (force_tac (claset() addSIs [order_antisym], simpset()) 1);
+qed "Least_mono";