# HG changeset patch
# User oheimb
# Date 982249307 -3600
# Node ID 42181d7cd7b201b63001d799fc847d1344f55c55
# Parent  0d4ca3b3741f4264d2c8a4353df2f5054f70d458
moved inv_image to Relation
nonempty_has_least of Nat.ML -> ex_has_least_nat of Wellfounded_Relations.ML
added wf_linord_ex_has_least,LeastM_nat_lemma,LeastM_natI,LeastM_nat_le

diff -r 0d4ca3b3741f -r 42181d7cd7b2 src/HOL/Wellfounded_Relations.ML
--- a/src/HOL/Wellfounded_Relations.ML	Thu Feb 15 16:01:34 2001 +0100
+++ b/src/HOL/Wellfounded_Relations.ML	Thu Feb 15 16:01:47 2001 +0100
@@ -7,9 +7,7 @@
 *)
 
 
-(*----------------------------------------------------------------------------
- * "Less than" on the natural numbers
- *---------------------------------------------------------------------------*)
+section "`Less than' on the natural numbers";
 
 Goalw [less_than_def] "wf less_than"; 
 by (rtac (wf_pred_nat RS wf_trancl) 1);
@@ -47,12 +45,6 @@
 qed "wf_inv_image";
 AddSIs [wf_inv_image];
 
-Goalw [trans_def,inv_image_def]
-    "!!r. trans r ==> trans (inv_image r f)";
-by (Simp_tac 1);
-by (Blast_tac 1);
-qed "trans_inv_image";
-
 
 (*----------------------------------------------------------------------------
  * All measures are wellfounded.
@@ -224,3 +216,37 @@
  by(Blast_tac 1);
 by(blast_tac (claset() addIs prems) 1);
 qed "wf_same_fst";
+
+
+
+(* ### see also LEAST and wellorderings in Wellfounded_Recursion.ML *)
+
+Goal "wf r ==> !x y. ((x,y):r^+) = ((y,x)~:r^*) ==> \
+\ P k ==> ? x. P x & (!y. P y --> (m x,m y):r^*)";
+by (dtac (wf_trancl RS (wf_eq_minimal RS iffD1)) 1);
+by (dres_inst_tac [("x","m`Collect P")] spec 1);
+by (Force_tac 1);
+qed "wf_linord_ex_has_least";
+
+(* successor of obsolete nonempty_has_least *)
+Goal "P k ==> ? x. P x & (!y. P y --> m x <= (m y::nat))";
+by (simp_tac (HOL_basic_ss addsimps [le_eq RS sym]) 1);
+by (rtac (wf_pred_nat RS wf_linord_ex_has_least) 1);
+by (simp_tac (simpset() addsimps [less_eq,not_le_iff_less,le_eq]) 1);
+by (atac 1);
+qed "ex_has_least_nat";
+
+Goalw [thm "LeastM_def"] 
+  "P k ==> P (LeastM m P) & (!y. P y --> m (LeastM m P) <= (m y::nat))";
+by (rtac someI_ex 1);
+by (etac ex_has_least_nat 1);
+qed "LeastM_nat_lemma";
+
+bind_thm ("LeastM_natI", LeastM_nat_lemma RS conjunct1);
+
+Goal "P x ==> m (LeastM m P) <= (m x::nat)";
+by (rtac (LeastM_nat_lemma RS conjunct2 RS spec RS mp) 1);
+by (atac 1);
+by (atac 1);
+qed "LeastM_nat_le";
+