src/HOL/NatDef.ML
changeset 3343 45986997f1fe
parent 3308 da002cef7090
child 3355 0d955bcf8e0a
     1.1 --- a/src/HOL/NatDef.ML	Mon May 26 12:38:29 1997 +0200
     1.2 +++ b/src/HOL/NatDef.ML	Mon May 26 12:39:57 1997 +0200
     1.3 @@ -402,6 +402,9 @@
     1.4  by (rtac not_less_eq 1);
     1.5  qed "le_eq_less_Suc";
     1.6  
     1.7 +(*  m<=n ==> m < Suc n  *)
     1.8 +bind_thm ("le_imp_less_Suc", le_eq_less_Suc RS iffD1);
     1.9 +
    1.10  goalw thy [le_def] "0 <= n";
    1.11  by (rtac not_less0 1);
    1.12  qed "le0";
    1.13 @@ -464,7 +467,7 @@
    1.14  goalw thy [le_def] "!!m. m < n ==> Suc(m) <= n";
    1.15  by (simp_tac (!simpset addsimps [less_Suc_eq]) 1);
    1.16  by (blast_tac (!claset addSEs [less_irrefl,less_asym]) 1);
    1.17 -qed "lessD";
    1.18 +qed "Suc_leI";  (*formerly called lessD*)
    1.19  
    1.20  goalw thy [le_def] "!!m. Suc(m) <= n ==> m <= n";
    1.21  by (asm_full_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
    1.22 @@ -479,7 +482,7 @@
    1.23  qed "Suc_le_lessD";
    1.24  
    1.25  goal thy "(Suc m <= n) = (m < n)";
    1.26 -by (blast_tac (!claset addIs [lessD, Suc_le_lessD]) 1);
    1.27 +by (blast_tac (!claset addIs [Suc_leI, Suc_le_lessD]) 1);
    1.28  qed "Suc_le_eq";
    1.29  
    1.30  goalw thy [le_def] "!!m. m <= n ==> m <= Suc n";
    1.31 @@ -493,6 +496,8 @@
    1.32  by (blast_tac (!claset addEs [less_asym]) 1);
    1.33  qed "less_imp_le";
    1.34  
    1.35 +(** Equivalence of m<=n and  m<n | m=n **)
    1.36 +
    1.37  goalw thy [le_def] "!!m. m <= n ==> m < n | m=(n::nat)";
    1.38  by (cut_facts_tac [less_linear] 1);
    1.39  by (blast_tac (!claset addEs [less_irrefl,less_asym]) 1);
    1.40 @@ -503,7 +508,7 @@
    1.41  by (blast_tac (!claset addSEs [less_irrefl] addEs [less_asym]) 1);
    1.42  qed "less_or_eq_imp_le";
    1.43  
    1.44 -goal thy "(x <= (y::nat)) = (x < y | x=y)";
    1.45 +goal thy "(m <= (n::nat)) = (m < n | m=n)";
    1.46  by (REPEAT(ares_tac [iffI,less_or_eq_imp_le,le_imp_less_or_eq] 1));
    1.47  qed "le_eq_less_or_eq";
    1.48  
    1.49 @@ -642,7 +647,7 @@
    1.50  val less_incr_rhs = Suc_mono RS Suc_lessD;
    1.51  val less_decr_lhs = Suc_lessD;
    1.52  val less_trans_Suc = less_trans_Suc;
    1.53 -val leI = lessD RS (Suc_le_mono RS iffD1);
    1.54 +val leI = Suc_leI RS (Suc_le_mono RS iffD1);
    1.55  val not_lessI = leI RS leD
    1.56  val not_leI = prove_goal thy "!!m::nat. n < m ==> ~ m <= n"
    1.57    (fn _ => [etac swap2 1, etac leD 1]);