# HG changeset patch
# User haftmann
# Date 1172846603 -3600
# Node ID 35f54980d4cc28974fed10b17f974edb2276830e
# Parent  56861fe9c22c71629c3b84b527f44a90322f1ebf
tuned code theorems

diff -r 56861fe9c22c -r 35f54980d4cc src/HOL/Integ/IntDef.thy
--- a/src/HOL/Integ/IntDef.thy	Fri Mar 02 15:43:22 2007 +0100
+++ b/src/HOL/Integ/IntDef.thy	Fri Mar 02 15:43:23 2007 +0100
@@ -263,14 +263,10 @@
 lemma zle_anti_sym: "[| z \<le> w; w \<le> z |] ==> z = (w::int)"
 by (cases w, cases z, simp add: le)
 
-(* Axiom 'order_less_le' of class 'order': *)
-lemma zless_le [code func]: "((w::int) < z) = (w \<le> z & w \<noteq> z)"
-by (simp add: less_int_def)
-
 instance int :: order
   by intro_classes
     (assumption |
-      rule zle_refl zle_trans zle_anti_sym zless_le)+
+      rule zle_refl zle_trans zle_anti_sym less_int_def [THEN meta_eq_to_obj_eq])+
 
 (* Axiom 'linorder_linear' of class 'linorder': *)
 lemma zle_linear: "(z::int) \<le> w | w \<le> z"
@@ -855,6 +851,7 @@
 apply (simp_all add: not_zle_0_negative del: int_Suc)
 done
 
+lemmas zless_le = less_int_def [THEN meta_eq_to_obj_eq]
 
 subsection {* Configuration of the code generator *}
 
@@ -891,12 +888,12 @@
   by (simp add: nat_aux_def)
 
 lemma [code inline]:
-  "neg k = (k < 0)"
+  "neg k \<longleftrightarrow> k < 0"
   unfolding neg_def ..
 
 lemma [code func]:
-  "\<bar>k\<Colon>int\<bar> = (if k \<le> 0 then - k else k)"
-  unfolding zabs_def by auto
+  "\<bar>k\<Colon>int\<bar> = (if k < 0 then - k else k)"
+  unfolding zabs_def ..
 
 consts_code
   "HOL.zero" :: "int"                ("0")