--- a/src/HOL/Nat.thy Fri Jul 01 13:54:57 2005 +0200
+++ b/src/HOL/Nat.thy Fri Jul 01 13:56:34 2005 +0200
@@ -286,7 +286,7 @@
lemma Suc_less_SucD: "Suc m < Suc n ==> m < n"
by (blast elim: lessE dest: Suc_lessD)
-lemma Suc_less_eq [iff]: "(Suc m < Suc n) = (m < n)"
+lemma Suc_less_eq [iff, code]: "(Suc m < Suc n) = (m < n)"
apply (rule iffI)
apply (erule Suc_less_SucD)
apply (erule Suc_mono)
@@ -300,6 +300,9 @@
apply (blast dest: Suc_lessD)
done
+lemma [code]: "((n::nat) < 0) = False" by simp
+lemma [code]: "(0 < Suc n) = True" by simp
+
text {* Can be used with @{text less_Suc_eq} to get @{term "n = m | n < m"} *}
lemma not_less_eq: "(~ m < n) = (n < Suc m)"
by (rule_tac m = m and n = n in diff_induct, simp_all)