src/HOL/NatDef.ML
changeset 3143 d60e49b86c6a
parent 3085 f45074fab9c7
child 3236 882e125ed7da
     1.1 --- a/src/HOL/NatDef.ML	Thu May 08 10:20:37 1997 +0200
     1.2 +++ b/src/HOL/NatDef.ML	Thu May 08 11:44:59 1997 +0200
     1.3 @@ -556,7 +556,19 @@
     1.4  
     1.5  (** LEAST -- the least number operator **)
     1.6  
     1.7 -val [prem1,prem2] = goalw thy [Least_def]
     1.8 +goal thy "(! m::nat. P m --> n <= m) = (! m. m < n --> ~ P m)";
     1.9 +by(blast_tac (!claset addIs [leI] addEs [leE]) 1);
    1.10 +val lemma = result();
    1.11 +
    1.12 +(* This is an old def of Least for nat, which is derived for compatibility *)
    1.13 +goalw thy [Least_def]
    1.14 +  "(LEAST n::nat. P n) == (@n. P(n) & (ALL m. m < n --> ~P(m)))";
    1.15 +by(simp_tac (!simpset addsimps [lemma]) 1);
    1.16 +br eq_reflection 1;
    1.17 +br refl 1;
    1.18 +qed "Least_nat_def";
    1.19 +
    1.20 +val [prem1,prem2] = goalw thy [Least_nat_def]
    1.21      "[| P(k::nat);  !!x. x<k ==> ~P(x) |] ==> (LEAST x.P(x)) = k";
    1.22  by (rtac select_equality 1);
    1.23  by (blast_tac (!claset addSIs [prem1,prem2]) 1);
    1.24 @@ -593,11 +605,11 @@
    1.25  by (rtac prem 1);
    1.26  qed "not_less_Least";
    1.27  
    1.28 -qed_goalw "Least_Suc" thy [Least_def]
    1.29 +qed_goalw "Least_Suc" thy [Least_nat_def]
    1.30   "!!P. [| ? n. P(Suc n); ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"
    1.31   (fn _ => [
    1.32          rtac select_equality 1,
    1.33 -        fold_goals_tac [Least_def],
    1.34 +        fold_goals_tac [Least_nat_def],
    1.35          safe_tac (!claset addSEs [LeastI]),
    1.36          rename_tac "j" 1,
    1.37          res_inst_tac [("n","j")] natE 1,
    1.38 @@ -607,7 +619,7 @@
    1.39          res_inst_tac [("n","k")] natE 1,
    1.40          Blast_tac 1,
    1.41          hyp_subst_tac 1,
    1.42 -        rewtac Least_def,
    1.43 +        rewtac Least_nat_def,
    1.44          rtac (select_equality RS arg_cong RS sym) 1,
    1.45          safe_tac (!claset),
    1.46          dtac Suc_mono 1,