1.1 --- a/src/HOL/Wellfounded_Relations.ML	Thu Feb 15 16:01:34 2001 +0100
     1.2 +++ b/src/HOL/Wellfounded_Relations.ML	Thu Feb 15 16:01:47 2001 +0100
     1.3 @@ -7,9 +7,7 @@
     1.4  *)
     1.5  
     1.6  
     1.7 -(*----------------------------------------------------------------------------
     1.8 - * "Less than" on the natural numbers
     1.9 - *---------------------------------------------------------------------------*)
    1.10 +section "`Less than' on the natural numbers";
    1.11  
    1.12  Goalw [less_than_def] "wf less_than"; 
    1.13  by (rtac (wf_pred_nat RS wf_trancl) 1);
    1.14 @@ -47,12 +45,6 @@
    1.15  qed "wf_inv_image";
    1.16  AddSIs [wf_inv_image];
    1.17  
    1.18 -Goalw [trans_def,inv_image_def]
    1.19 -    "!!r. trans r ==> trans (inv_image r f)";
    1.20 -by (Simp_tac 1);
    1.21 -by (Blast_tac 1);
    1.22 -qed "trans_inv_image";
    1.23 -
    1.24  
    1.25  (*----------------------------------------------------------------------------
    1.26   * All measures are wellfounded.
    1.27 @@ -224,3 +216,37 @@
    1.28   by(Blast_tac 1);
    1.29  by(blast_tac (claset() addIs prems) 1);
    1.30  qed "wf_same_fst";
    1.31 +
    1.32 +
    1.33 +
    1.34 +(* ### see also LEAST and wellorderings in Wellfounded_Recursion.ML *)
    1.35 +
    1.36 +Goal "wf r ==> !x y. ((x,y):r^+) = ((y,x)~:r^*) ==> \
    1.37 +\ P k ==> ? x. P x & (!y. P y --> (m x,m y):r^*)";
    1.38 +by (dtac (wf_trancl RS (wf_eq_minimal RS iffD1)) 1);
    1.39 +by (dres_inst_tac [("x","m`Collect P")] spec 1);
    1.40 +by (Force_tac 1);
    1.41 +qed "wf_linord_ex_has_least";
    1.42 +
    1.43 +(* successor of obsolete nonempty_has_least *)
    1.44 +Goal "P k ==> ? x. P x & (!y. P y --> m x <= (m y::nat))";
    1.45 +by (simp_tac (HOL_basic_ss addsimps [le_eq RS sym]) 1);
    1.46 +by (rtac (wf_pred_nat RS wf_linord_ex_has_least) 1);
    1.47 +by (simp_tac (simpset() addsimps [less_eq,not_le_iff_less,le_eq]) 1);
    1.48 +by (atac 1);
    1.49 +qed "ex_has_least_nat";
    1.50 +
    1.51 +Goalw [thm "LeastM_def"] 
    1.52 +  "P k ==> P (LeastM m P) & (!y. P y --> m (LeastM m P) <= (m y::nat))";
    1.53 +by (rtac someI_ex 1);
    1.54 +by (etac ex_has_least_nat 1);
    1.55 +qed "LeastM_nat_lemma";
    1.56 +
    1.57 +bind_thm ("LeastM_natI", LeastM_nat_lemma RS conjunct1);
    1.58 +
    1.59 +Goal "P x ==> m (LeastM m P) <= (m x::nat)";
    1.60 +by (rtac (LeastM_nat_lemma RS conjunct2 RS spec RS mp) 1);
    1.61 +by (atac 1);
    1.62 +by (atac 1);
    1.63 +qed "LeastM_nat_le";
    1.64 +