author haftmann Mon, 02 Oct 2006 23:00:57 +0200 changeset 20839 ed49d8709959 parent 20838 e115ea078a30 child 20840 5e92606245b6
improvements for code_gen
--- a/src/HOL/Library/EfficientNat.thy	Mon Oct 02 23:00:56 2006 +0200
+++ b/src/HOL/Library/EfficientNat.thy	Mon Oct 02 23:00:57 2006 +0200
@@ -28,6 +28,10 @@
nat_of_int :: "int \<Rightarrow> nat"
"k \<ge> 0 \<Longrightarrow> nat_of_int k = nat k"

+lemma nat_of_int_int:
+  "nat_of_int (int n) = n"
+  using zero_zle_int nat_of_int_def by simp
+
code_constname
nat_of_int "IntDef.nat_of_int"

@@ -36,7 +40,7 @@
expression:
*}

-lemma [code unfold]: "nat_case \<equiv> (\<lambda>f g n. if n = 0 then f else g (n - 1))"
+lemma [code unfold, code noinline]: "nat_case \<equiv> (\<lambda>f g n. if n = 0 then f else g (n - 1))"
proof -
have rewrite: "\<And>f g n. nat_case f g n = (if n = 0 then f else g (n - 1))"
proof -
@@ -48,6 +52,10 @@
by (rule eq_reflection ext rewrite)+
qed

+lemma [code inline]:
+  "nat_case f g n = (if OperationalEquality.eq n 0 then f else g (nat_of_int (int n - 1)))"
+  by (cases n) (simp_all add: eq_def nat_of_int_int)
+
text {*
Most standard arithmetic functions on natural numbers are implemented
using their counterparts on the integers:
@@ -120,6 +128,14 @@
@{typ nat} is no longer a datatype but embedded into the integers.
*}

+code_const "0::nat"
+  (SML target_atom "(0 : IntInf.int)")