# HG changeset patch
# User haftmann
# Date 1172216361 -3600
# Node ID ab505d2810154458a40c5a13dfccfcdffdeab6de
# Parent  ddbf185a3be017b9fefd64008bd6d72ca351d47c
adjusted code lemmas

diff -r ddbf185a3be0 -r ab505d281015 src/HOL/Nat.thy
--- 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 *}
diff -r ddbf185a3be0 -r ab505d281015 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Fri Feb 23 08:39:20 2007 +0100
+++ b/src/HOL/Orderings.thy	Fri Feb 23 08:39:21 2007 +0100
@@ -124,8 +124,6 @@
 
 class order = preorder + 
   assumes antisym: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> x \<Longrightarrow> x = y"
-
-context order
 begin
 
 text {* Asymmetry. *}
@@ -815,6 +813,13 @@
 lemma le_boolD: "P \<le> Q \<Longrightarrow> P \<longrightarrow> Q"
   by (simp add: le_bool_def)
 
+lemma [code func]:
+  "False \<le> b \<longleftrightarrow> True"
+  "True \<le> b \<longleftrightarrow> b"
+  "False < b \<longleftrightarrow> b"
+  "True < b \<longleftrightarrow> False"
+  unfolding le_bool_def less_bool_def by simp_all
+
 subsection {* Monotonicity, syntactic least value operator and min/max *}
 
 locale mono =