# HG changeset patch
# User paulson
# Date 864643197 -7200
# Node ID 45986997f1fe9515d5f18c63496d2101a55c0aca
# Parent  ec3b55fcb165628c42285ec0908f365af6b21fb8
Renamed lessD to Suc_leI

diff -r ec3b55fcb165 -r 45986997f1fe src/HOL/Hoare/Arith2.ML
--- a/src/HOL/Hoare/Arith2.ML	Mon May 26 12:38:29 1997 +0200
+++ b/src/HOL/Hoare/Arith2.ML	Mon May 26 12:39:57 1997 +0200
@@ -68,7 +68,7 @@
 by (rtac (Suc_diff_n RS sym) 1);
 by (rtac le_less_trans 1);
 by (etac (not_less_eq RS subst) 2);
-by (rtac (hd ([diff_less_Suc RS lessD] RL [Suc_le_mono RS subst])) 1);
+by (rtac (hd ([diff_less_Suc RS Suc_leI] RL [Suc_le_mono RS subst])) 1);
 qed "diff_add_not_assoc";
 
 val prems=goal Arith.thy "~n<k ==> (m + n) - k = m + ((n - k)::nat)";
diff -r ec3b55fcb165 -r 45986997f1fe src/HOL/NatDef.ML
--- a/src/HOL/NatDef.ML	Mon May 26 12:38:29 1997 +0200
+++ b/src/HOL/NatDef.ML	Mon May 26 12:39:57 1997 +0200
@@ -402,6 +402,9 @@
 by (rtac not_less_eq 1);
 qed "le_eq_less_Suc";
 
+(*  m<=n ==> m < Suc n  *)
+bind_thm ("le_imp_less_Suc", le_eq_less_Suc RS iffD1);
+
 goalw thy [le_def] "0 <= n";
 by (rtac not_less0 1);
 qed "le0";
@@ -464,7 +467,7 @@
 goalw thy [le_def] "!!m. m < n ==> Suc(m) <= n";
 by (simp_tac (!simpset addsimps [less_Suc_eq]) 1);
 by (blast_tac (!claset addSEs [less_irrefl,less_asym]) 1);
-qed "lessD";
+qed "Suc_leI";  (*formerly called lessD*)
 
 goalw thy [le_def] "!!m. Suc(m) <= n ==> m <= n";
 by (asm_full_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
@@ -479,7 +482,7 @@
 qed "Suc_le_lessD";
 
 goal thy "(Suc m <= n) = (m < n)";
-by (blast_tac (!claset addIs [lessD, Suc_le_lessD]) 1);
+by (blast_tac (!claset addIs [Suc_leI, Suc_le_lessD]) 1);
 qed "Suc_le_eq";
 
 goalw thy [le_def] "!!m. m <= n ==> m <= Suc n";
@@ -493,6 +496,8 @@
 by (blast_tac (!claset addEs [less_asym]) 1);
 qed "less_imp_le";
 
+(** Equivalence of m<=n and  m<n | m=n **)
+
 goalw thy [le_def] "!!m. m <= n ==> m < n | m=(n::nat)";
 by (cut_facts_tac [less_linear] 1);
 by (blast_tac (!claset addEs [less_irrefl,less_asym]) 1);
@@ -503,7 +508,7 @@
 by (blast_tac (!claset addSEs [less_irrefl] addEs [less_asym]) 1);
 qed "less_or_eq_imp_le";
 
-goal thy "(x <= (y::nat)) = (x < y | x=y)";
+goal thy "(m <= (n::nat)) = (m < n | m=n)";
 by (REPEAT(ares_tac [iffI,less_or_eq_imp_le,le_imp_less_or_eq] 1));
 qed "le_eq_less_or_eq";
 
@@ -642,7 +647,7 @@
 val less_incr_rhs = Suc_mono RS Suc_lessD;
 val less_decr_lhs = Suc_lessD;
 val less_trans_Suc = less_trans_Suc;
-val leI = lessD RS (Suc_le_mono RS iffD1);
+val leI = Suc_leI RS (Suc_le_mono RS iffD1);
 val not_lessI = leI RS leD
 val not_leI = prove_goal thy "!!m::nat. n < m ==> ~ m <= n"
   (fn _ => [etac swap2 1, etac leD 1]);