src/HOL/Nat.ML
changeset 1817 3994d37b16ae
parent 1786 8a31d85d27b8
child 1823 e1458e1a9f80
     1.1 --- a/src/HOL/Nat.ML	Tue Jun 18 16:38:48 1996 +0200
     1.2 +++ b/src/HOL/Nat.ML	Thu Jun 20 10:26:13 1996 +0200
     1.3 @@ -242,7 +242,7 @@
     1.4  by (etac (wf_pred_nat RS wf_trancl RS wf_irrefl) 1);
     1.5  qed "less_not_refl";
     1.6  
     1.7 -(* n(n ==> R *)
     1.8 +(* n<n ==> R *)
     1.9  bind_thm ("less_irrefl", (less_not_refl RS notE));
    1.10  
    1.11  goal Nat.thy "!!m. n<m ==> m ~= (n::nat)";
    1.12 @@ -457,6 +457,18 @@
    1.13  by (Fast_tac 1);
    1.14  qed "Suc_leD";
    1.15  
    1.16 +(* stronger version of Suc_leD *)
    1.17 +goalw Nat.thy [le_def] 
    1.18 +        "!!m. Suc m <= n ==> m < n";
    1.19 +by (asm_full_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
    1.20 +by (cut_facts_tac [less_linear] 1);
    1.21 +by (fast_tac HOL_cs 1);
    1.22 +qed "Suc_le_lessD";
    1.23 +
    1.24 +goal Nat.thy "(Suc m <= n) = (m < n)";
    1.25 +by (fast_tac (!claset addIs [lessD, Suc_le_lessD]) 1);
    1.26 +qed "Suc_le_eq";
    1.27 +
    1.28  goalw Nat.thy [le_def] "!!m. m <= n ==> m <= Suc n";
    1.29  by (fast_tac (!claset addDs [Suc_lessD]) 1);
    1.30  qed "le_SucI";