# HG changeset patch
# User haftmann
# Date 1190715372 -7200
# Node ID 291665d063e4a88c6ad2e55fb42065d8a9d08ca3
# Parent  c6674504103f65c716bba8120b88951cfb616eec
added conversions for natural numbers

diff -r c6674504103f -r 291665d063e4 src/HOL/Library/ML_Int.thy
--- a/src/HOL/Library/ML_Int.thy	Tue Sep 25 12:16:08 2007 +0200
+++ b/src/HOL/Library/ML_Int.thy	Tue Sep 25 12:16:12 2007 +0200
@@ -131,16 +131,16 @@
   "\<bar>k\<bar> \<equiv> if k < 0 then -k else k" ..
 
 
-subsection {* Conversion to @{typ nat} *}
+subsection {* Conversion to and from @{typ nat} *}
 
 definition
   nat_of_ml_int :: "ml_int \<Rightarrow> nat"
 where
-  "nat_of_ml_int = nat o int_of_ml_int"
+  [code func del]: "nat_of_ml_int = nat o int_of_ml_int"
 
 definition
   nat_of_ml_int_aux :: "ml_int \<Rightarrow> nat \<Rightarrow> nat" where
-  "nat_of_ml_int_aux i n = nat_of_ml_int i + n"
+  [code func del]: "nat_of_ml_int_aux i n = nat_of_ml_int i + n"
 
 lemma nat_of_ml_int_aux_code [code]:
   "nat_of_ml_int_aux i n = (if i \<le> 0 then n else nat_of_ml_int_aux (i - 1) (Suc n))"
@@ -150,6 +150,21 @@
   "nat_of_ml_int i = nat_of_ml_int_aux i 0"
   by (simp add: nat_of_ml_int_aux_def)
 
+definition
+  ml_int_of_nat :: "nat \<Rightarrow> ml_int"
+where
+  [code func del]: "ml_int_of_nat = ml_int_of_int o of_nat"
+
+lemma ml_int_of_nat [code func]:
+  "ml_int_of_nat 0 = 0"
+  "ml_int_of_nat (Suc n) = ml_int_of_nat n + 1"
+  unfolding ml_int_of_nat_def by simp_all
+
+lemma ml_int_nat_id [simp]:
+  "nat_of_ml_int (ml_int_of_nat n) = n"
+  "ml_int_of_nat (nat_of_ml_int i) = (if i \<le> 0 then 0 else i)"
+  unfolding ml_int_of_nat_def nat_of_ml_int_def by simp_all
+
 
 subsection {* ML interface *}
 
@@ -170,7 +185,7 @@
 
 setup {*
   CodeTarget.add_pretty_numeral "SML" false
-    @{const_name ml_int_of_int}
+    @{const_name number_ml_int_inst.number_of_ml_int}
     @{const_name Numeral.B0} @{const_name Numeral.B1}
     @{const_name Numeral.Pls} @{const_name Numeral.Min}
     @{const_name Numeral.Bit}
@@ -200,5 +215,3 @@
   (SML "Int.< ((_), (_))")
 
 end
-
-