1.1 --- a/src/HOL/Wellfounded_Recursion.ML	Thu Feb 15 16:01:22 2001 +0100
     1.2 +++ b/src/HOL/Wellfounded_Recursion.ML	Thu Feb 15 16:01:34 2001 +0100
     1.3 @@ -123,8 +123,7 @@
     1.4  by Safe_tac;
     1.5  by (EVERY1[rtac allE, assume_tac, etac impE, Blast_tac]);
     1.6  by (etac bexE 1);
     1.7 -by (rename_tac "a" 1);
     1.8 -by (case_tac "a = x" 1);
     1.9 +by (rename_tac "a" 1 THEN case_tac "a = x" 1);
    1.10   by (res_inst_tac [("x","a")]bexI 2);
    1.11    by (assume_tac 3);
    1.12   by (Blast_tac 2);
    1.13 @@ -163,8 +162,7 @@
    1.14  \     |] ==> wf(UN i:I. r i)";
    1.15  by (asm_full_simp_tac (HOL_basic_ss addsimps [wf_eq_minimal]) 1);
    1.16  by (Clarify_tac 1);
    1.17 -by (rename_tac "A a" 1);
    1.18 -by (case_tac "EX i:I. EX a:A. EX b:A. (b,a) : r i" 1);
    1.19 +by (rename_tac "A a" 1 THEN case_tac "EX i:I. EX a:A. EX b:A. (b,a) : r i" 1);
    1.20   by (Asm_full_simp_tac 2);
    1.21   by (Best_tac 2);  (*much faster than Blast_tac*)
    1.22  by (Clarify_tac 1);
    1.23 @@ -368,3 +366,24 @@
    1.24  by (Clarify_tac 1);
    1.25  by (etac wfrec 1);
    1.26  qed "tfl_wfrec";
    1.27 +
    1.28 +(*LEAST and wellorderings*)
    1.29 +(* ### see also wf_linord_ex_has_least and its consequences in Wellfounded_Relations.ML *)
    1.30 +
    1.31 +Goal "P (k::'a::wellorder) --> P (LEAST x. P(x)) & (LEAST x. P(x)) <= k";
    1.32 +by (res_inst_tac [("a","k")] (wf RS wf_induct) 1);
    1.33 +by (rtac impI 1);
    1.34 +by (rtac classical 1);
    1.35 +by (res_inst_tac [("s","x")] (Least_equality RS ssubst) 1);
    1.36 +by Auto_tac;
    1.37 +by (auto_tac (claset(), simpset() addsimps [linorder_not_less RS sym]));  
    1.38 +by (blast_tac (claset() addIs [order_less_trans]) 1);
    1.39 +bind_thm("wellorder_LeastI",   result() RS mp RS conjunct1);
    1.40 +bind_thm("wellorder_Least_le", result() RS mp RS conjunct2);
    1.41 +
    1.42 +Goal "[| k < (LEAST x. P x) |] ==> ~P (k::'a::wellorder)";
    1.43 +by (full_simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1);
    1.44 +by (etac contrapos_nn 1);
    1.45 +by (etac wellorder_Least_le 1);
    1.46 +qed "wellorder_not_less_Least";
    1.47 +