--- a/src/HOL/Nat.thy Fri Feb 23 08:39:20 2007 +0100
+++ b/src/HOL/Nat.thy Fri Feb 23 08:39:21 2007 +0100
@@ -1068,23 +1068,25 @@
subsection {* Code generator setup *}
-lemma one_is_suc_zero [code inline]:
+lemma one_is_Suc_zero [code inline]:
"1 = Suc 0"
by simp
instance nat :: eq ..
lemma [code func]:
- "(0\<Colon>nat) = 0 \<longleftrightarrow> True" by auto
+ "(0\<Colon>nat) = 0 \<longleftrightarrow> True"
+ "Suc n = Suc m \<longleftrightarrow> n = m"
+ "Suc n = 0 \<longleftrightarrow> False"
+ "0 = Suc m \<longleftrightarrow> False"
+ by auto
lemma [code func]:
- "Suc n = Suc m \<longleftrightarrow> n = m" by auto
-
-lemma [code func]:
- "Suc n = 0 \<longleftrightarrow> False" by auto
-
-lemma [code func]:
- "0 = Suc m \<longleftrightarrow> False" by auto
+ "(0\<Colon>nat) \<le> m \<longleftrightarrow> True"
+ "Suc (n\<Colon>nat) \<le> m \<longleftrightarrow> n < m"
+ "(n\<Colon>nat) < 0 \<longleftrightarrow> False"
+ "(n\<Colon>nat) < Suc m \<longleftrightarrow> n \<le> m"
+ using Suc_le_eq less_Suc_eq_le by simp_all
subsection {* Further Arithmetic Facts Concerning the Natural Numbers *}