adjusted code lemmas
authorhaftmann
Fri Feb 23 08:39:21 2007 +0100 (2007-02-23)
changeset 22348ab505d281015
parent 22347 ddbf185a3be0
child 22349 a4e82dd93202
adjusted code lemmas
src/HOL/Nat.thy
src/HOL/Orderings.thy
     1.1 --- a/src/HOL/Nat.thy	Fri Feb 23 08:39:20 2007 +0100
     1.2 +++ b/src/HOL/Nat.thy	Fri Feb 23 08:39:21 2007 +0100
     1.3 @@ -1068,23 +1068,25 @@
     1.4  
     1.5  subsection {* Code generator setup *}
     1.6  
     1.7 -lemma one_is_suc_zero [code inline]:
     1.8 +lemma one_is_Suc_zero [code inline]:
     1.9    "1 = Suc 0"
    1.10    by simp
    1.11  
    1.12  instance nat :: eq ..
    1.13  
    1.14  lemma [code func]:
    1.15 -  "(0\<Colon>nat) = 0 \<longleftrightarrow> True" by auto
    1.16 +  "(0\<Colon>nat) = 0 \<longleftrightarrow> True"
    1.17 +  "Suc n = Suc m \<longleftrightarrow> n = m"
    1.18 +  "Suc n = 0 \<longleftrightarrow> False"
    1.19 +  "0 = Suc m \<longleftrightarrow> False"
    1.20 +  by auto
    1.21  
    1.22  lemma [code func]:
    1.23 -  "Suc n = Suc m \<longleftrightarrow> n = m" by auto
    1.24 -
    1.25 -lemma [code func]:
    1.26 -  "Suc n = 0 \<longleftrightarrow> False" by auto
    1.27 -
    1.28 -lemma [code func]:
    1.29 -  "0 = Suc m \<longleftrightarrow> False" by auto
    1.30 +  "(0\<Colon>nat) \<le> m \<longleftrightarrow> True"
    1.31 +  "Suc (n\<Colon>nat) \<le> m \<longleftrightarrow> n < m"
    1.32 +  "(n\<Colon>nat) < 0 \<longleftrightarrow> False"  
    1.33 +  "(n\<Colon>nat) < Suc m \<longleftrightarrow> n \<le> m"
    1.34 +  using Suc_le_eq less_Suc_eq_le by simp_all
    1.35  
    1.36  
    1.37  subsection {* Further Arithmetic Facts Concerning the Natural Numbers *}
     2.1 --- a/src/HOL/Orderings.thy	Fri Feb 23 08:39:20 2007 +0100
     2.2 +++ b/src/HOL/Orderings.thy	Fri Feb 23 08:39:21 2007 +0100
     2.3 @@ -124,8 +124,6 @@
     2.4  
     2.5  class order = preorder + 
     2.6    assumes antisym: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> x \<Longrightarrow> x = y"
     2.7 -
     2.8 -context order
     2.9  begin
    2.10  
    2.11  text {* Asymmetry. *}
    2.12 @@ -815,6 +813,13 @@
    2.13  lemma le_boolD: "P \<le> Q \<Longrightarrow> P \<longrightarrow> Q"
    2.14    by (simp add: le_bool_def)
    2.15  
    2.16 +lemma [code func]:
    2.17 +  "False \<le> b \<longleftrightarrow> True"
    2.18 +  "True \<le> b \<longleftrightarrow> b"
    2.19 +  "False < b \<longleftrightarrow> b"
    2.20 +  "True < b \<longleftrightarrow> False"
    2.21 +  unfolding le_bool_def less_bool_def by simp_all
    2.22 +
    2.23  subsection {* Monotonicity, syntactic least value operator and min/max *}
    2.24  
    2.25  locale mono =