--- a/src/HOL/Library/EfficientNat.thy Wed Jun 14 12:13:12 2006 +0200
+++ b/src/HOL/Library/EfficientNat.thy Wed Jun 14 12:14:13 2006 +0200
@@ -51,17 +51,20 @@
*}
int ("(_)")
-code_syntax_tyco nat
- ml (target_atom "{* int *}")
- haskell (target_atom "{* int *}")
+code_typapp nat
+ ml (target_atom "IntInf.int")
+ haskell (target_atom "Integer")
+
+definition
+ "nat_of_int (k::int) = (if k < 0 then - k else k)"
-code_syntax_const
- "0 :: nat"
- ml (target_atom "{* 0 :: int *}")
- haskell (target_atom "{* 0 :: int *}")
- Suc
- ml (target_atom "(__ + 1)")
- haskell (target_atom "(__ + 1)")
+lemma
+ "nat_of_int = abs"
+by (simp add: expand_fun_eq nat_of_int_def zabs_def)
+
+code_generate (ml, haskell) "abs :: int \<Rightarrow> int"
+
+code_constapp
nat
ml ("{* abs :: int \<Rightarrow> int *}")
haskell ("{* abs :: int \<Rightarrow> int *}")
@@ -70,6 +73,18 @@
haskell ("_")
text {*
+ Eliminate @{const "0::nat"} and @{const "Suc"}
+ by unfolding in place.
+*}
+
+lemma [code unfolt]:
+ "0 = nat 0"
+ "Suc = (op +) 1"
+by (simp_all add: expand_fun_eq)
+
+declare elim_one_nat [code nofold]
+
+text {*
Case analysis on natural numbers is rephrased using a conditional
expression:
*}
@@ -98,9 +113,8 @@
lemma [code]: "(m < n) = (int m < int n)"
by simp
lemma [code fun]:
- "((0::nat) = 0) = True"
"(m = n) = (int m = int n)"
- by simp_all
+ by simp
subsection {* Preprocessors *}