New theorem le_Suc_eq
authorpaulson
Tue May 27 13:23:53 1997 +0200 (1997-05-27)
changeset 33550d955bcf8e0a
parent 3354 3dac85693547
child 3356 9b899eb8a036
New theorem le_Suc_eq
src/HOL/NatDef.ML
     1.1 --- a/src/HOL/NatDef.ML	Tue May 27 13:23:27 1997 +0200
     1.2 +++ b/src/HOL/NatDef.ML	Tue May 27 13:23:53 1997 +0200
     1.3 @@ -423,6 +423,11 @@
     1.4            n_not_Suc_n, Suc_n_not_n,
     1.5            nat_case_0, nat_case_Suc, nat_rec_0, nat_rec_Suc];
     1.6  
     1.7 +goal thy "!!m. (m <= Suc(n)) = (m<=n | m = Suc n)";
     1.8 +by (simp_tac (!simpset addsimps [le_eq_less_Suc]) 1);
     1.9 +by (blast_tac (!claset addSEs [less_SucE] addIs [less_SucI]) 1);
    1.10 +qed "le_Suc_eq";
    1.11 +
    1.12  (*
    1.13  goal thy "(Suc m < n | Suc m = n) = (m < n)";
    1.14  by (stac (less_Suc_eq RS sym) 1);