Efficient_Nat and Pretty_Int integrated with ML_Int

--- a/src/HOL/Lambda/WeakNorm.thy	Tue Sep 25 17:06:19 2007 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy	Tue Sep 25 21:08:34 2007 +0200
@@ -419,14 +419,14 @@
 *}
 
 definition
-  int :: "nat \<Rightarrow> int" where
-  "int \<equiv> of_nat"
+  int_of_nat :: "nat \<Rightarrow> int" where
+  "int_of_nat = of_nat"
 
-export_code type_NF nat int in SML module_name Norm
+export_code type_NF nat int_of_nat in SML module_name Norm
 
 ML {*
 val nat_of_int = Norm.nat;
-val int_of_nat = Norm.int;
+val int_of_nat = Norm.int_of_nat;
 
 fun dBtype_of_typ (Type ("fun", [T, U])) =
       Norm.Fun (dBtype_of_typ T, dBtype_of_typ U)

--- a/src/HOL/Library/Efficient_Nat.thy	Tue Sep 25 17:06:19 2007 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy	Tue Sep 25 21:08:34 2007 +0200
@@ -32,17 +32,20 @@
   "k \<ge> 0 \<Longrightarrow> nat_of_int k = nat k"
 
 definition
-  int' :: "nat \<Rightarrow> int" where
-  "int' n = of_nat n"
+  int_of_nat :: "nat \<Rightarrow> int" where
+  "int_of_nat n = of_nat n"
 
-lemma int'_Suc [simp]: "int' (Suc n) = 1 + int' n"
-unfolding int'_def by simp
+lemma int_of_nat_Suc [simp]:
+  "int_of_nat (Suc n) = 1 + int_of_nat n"
+  unfolding int_of_nat_def by simp
 
-lemma int'_add: "int' (m + n) = int' m + int' n"
-unfolding int'_def by (rule of_nat_add)
+lemma int_of_nat_add:
+  "int_of_nat (m + n) = int_of_nat m + int_of_nat n"
+  unfolding int_of_nat_def by (rule of_nat_add)
 
-lemma int'_mult: "int' (m * n) = int' m * int' n"
-unfolding int'_def by (rule of_nat_mult)
+lemma int_of_nat_mult:
+  "int_of_nat (m * n) = int_of_nat m * int_of_nat n"
+  unfolding int_of_nat_def by (rule of_nat_mult)
 
 lemma nat_of_int_of_number_of:
   fixes k
@@ -57,10 +60,10 @@
   using assms unfolding Pls_def by simp
 
 lemma nat_of_int_int:
-  "nat_of_int (int' n) = n"
-  using nat_of_int_def int'_def by simp
+  "nat_of_int (int_of_nat n) = n"
+  using nat_of_int_def int_of_nat_def by simp
 
-lemma eq_nat_of_int: "int' n = x \<Longrightarrow> n = nat_of_int x"
+lemma eq_nat_of_int: "int_of_nat n = x \<Longrightarrow> n = nat_of_int x"
 by (erule subst, simp only: nat_of_int_int)
 
 code_datatype nat_of_int
@@ -84,10 +87,10 @@
 qed
 
 lemma [code inline]:
-  "nat_case = (\<lambda>f g n. if n = 0 then f else g (nat_of_int (int' n - 1)))"
+  "nat_case = (\<lambda>f g n. if n = 0 then f else g (nat_of_int (int_of_nat n - 1)))"
 proof (rule ext)+
   fix f g n
-  show "nat_case f g n = (if n = 0 then f else g (nat_of_int (int' n - 1)))"
+  show "nat_case f g n = (if n = 0 then f else g (nat_of_int (int_of_nat n - 1)))"
   by (cases n) (simp_all add: nat_of_int_int)
 qed
 
@@ -98,63 +101,77 @@
 
 lemma [code func]: "0 = nat_of_int 0"
   by (simp add: nat_of_int_def)
+
 lemma [code func, code inline]:  "1 = nat_of_int 1"
   by (simp add: nat_of_int_def)
-lemma [code func]: "Suc n = nat_of_int (int' n + 1)"
+
+lemma [code func]: "Suc n = nat_of_int (int_of_nat n + 1)"
   by (simp add: eq_nat_of_int)
-lemma [code]: "m + n = nat (int' m + int' n)"
-  by (simp add: int'_def nat_eq_iff2)
-lemma [code func, code inline]: "m + n = nat_of_int (int' m + int' n)"
-  by (simp add: eq_nat_of_int int'_add)
-lemma [code, code inline]: "m - n = nat (int' m - int' n)"
-  by (simp add: int'_def nat_eq_iff2 of_nat_diff)
-lemma [code]: "m * n = nat (int' m * int' n)"
-  unfolding int'_def
+
+lemma [code]: "m + n = nat (int_of_nat m + int_of_nat n)"
+  by (simp add: int_of_nat_def nat_eq_iff2)
+
+lemma [code func, code inline]: "m + n = nat_of_int (int_of_nat m + int_of_nat n)"
+  by (simp add: eq_nat_of_int int_of_nat_add)
+
+lemma [code, code inline]: "m - n = nat (int_of_nat m - int_of_nat n)"
+  by (simp add: int_of_nat_def nat_eq_iff2 of_nat_diff)
+
+lemma [code]: "m * n = nat (int_of_nat m * int_of_nat n)"
+  unfolding int_of_nat_def
   by (simp add: of_nat_mult [symmetric] del: of_nat_mult)
-lemma [code func, code inline]: "m * n = nat_of_int (int' m * int' n)"
-  by (simp add: eq_nat_of_int int'_mult)
-lemma [code]: "m div n = nat (int' m div int' n)"
-  unfolding int'_def zdiv_int [symmetric] by simp
-lemma [code func]: "m div n = fst (Divides.divmod m n)"
-  unfolding divmod_def by simp
-lemma [code]: "m mod n = nat (int' m mod int' n)"
-  unfolding int'_def zmod_int [symmetric] by simp
-lemma [code func]: "m mod n = snd (Divides.divmod m n)"
-  unfolding divmod_def by simp
-lemma [code, code inline]: "(m < n) \<longleftrightarrow> (int' m < int' n)"
-  unfolding int'_def by simp
-lemma [code func, code inline]: "(m \<le> n) \<longleftrightarrow> (int' m \<le> int' n)"
-  unfolding int'_def by simp
-lemma [code func, code inline]: "m = n \<longleftrightarrow> int' m = int' n"
-  unfolding int'_def by simp
+
+lemma [code func, code inline]: "m * n = nat_of_int (int_of_nat m * int_of_nat n)"
+  by (simp add: eq_nat_of_int int_of_nat_mult)
+
+lemma [code]: "m div n = nat (int_of_nat m div int_of_nat n)"
+  unfolding int_of_nat_def zdiv_int [symmetric] by simp
+
+lemma div_nat_code [code func]:
+  "m div k = nat_of_int (fst (divAlg (int_of_nat m, int_of_nat k)))"
+  unfolding div_def [symmetric] int_of_nat_def zdiv_int [symmetric]
+  unfolding int_of_nat_def [symmetric] nat_of_int_int ..
+
+lemma [code]: "m mod n = nat (int_of_nat m mod int_of_nat n)"
+  unfolding int_of_nat_def zmod_int [symmetric] by simp
+
+lemma mod_nat_code [code func]:
+  "m mod k = nat_of_int (snd (divAlg (int_of_nat m, int_of_nat k)))"
+  unfolding mod_def [symmetric] int_of_nat_def zmod_int [symmetric]
+  unfolding int_of_nat_def [symmetric] nat_of_int_int ..
+
+lemma [code, code inline]: "(m < n) \<longleftrightarrow> (int_of_nat m < int_of_nat n)"
+  unfolding int_of_nat_def by simp
+
+lemma [code func, code inline]: "(m \<le> n) \<longleftrightarrow> (int_of_nat m \<le> int_of_nat n)"
+  unfolding int_of_nat_def by simp
+
+lemma [code func, code inline]: "m = n \<longleftrightarrow> int_of_nat m = int_of_nat n"
+  unfolding int_of_nat_def by simp
+
 lemma [code func]: "nat k = (if k < 0 then 0 else nat_of_int k)"
-proof (cases "k < 0")
-  case True then show ?thesis by simp
-next
-  case False then show ?thesis by (simp add: nat_of_int_def)
-qed
+  by (cases "k < 0") (simp, simp add: nat_of_int_def)
+
 lemma [code func]:
-  "int_aux n i = (if int' n = 0 then i else int_aux (nat_of_int (int' n - 1)) (i + 1))"
+  "int_aux n i = (if int_of_nat n = 0 then i else int_aux (nat_of_int (int_of_nat n - 1)) (i + 1))"
 proof -
-  have "0 < n \<Longrightarrow> int' n = 1 + int' (nat_of_int (int' n - 1))"
+  have "0 < n \<Longrightarrow> int_of_nat n = 1 + int_of_nat (nat_of_int (int_of_nat n - 1))"
   proof -
     assume prem: "n > 0"
-    then have "int' n - 1 \<ge> 0" unfolding int'_def by auto
-    then have "nat_of_int (int' n - 1) = nat (int' n - 1)" by (simp add: nat_of_int_def)
-    with prem show "int' n = 1 + int' (nat_of_int (int' n - 1))" unfolding int'_def by simp
+    then have "int_of_nat n - 1 \<ge> 0" unfolding int_of_nat_def by auto
+    then have "nat_of_int (int_of_nat n - 1) = nat (int_of_nat n - 1)" by (simp add: nat_of_int_def)
+    with prem show "int_of_nat n = 1 + int_of_nat (nat_of_int (int_of_nat n - 1))" unfolding int_of_nat_def by simp
   qed
-  then show ?thesis unfolding int_aux_def int'_def by auto
+  then show ?thesis unfolding int_aux_def int_of_nat_def by auto
 qed
 
-lemma div_nat_code [code func]:
-  "m div k = nat_of_int (fst (divAlg (int' m, int' k)))"
-  unfolding div_def [symmetric] int'_def zdiv_int [symmetric]
-  unfolding int'_def [symmetric] nat_of_int_int ..
+lemma ml_int_of_nat_code [code func, code inline]:
+  "ml_int_of_nat n = ml_int_of_int (int_of_nat n)"
+  unfolding ml_int_of_nat_def int_of_nat_def by simp
 
-lemma mod_nat_code [code func]:
-  "m mod k = nat_of_int (snd (divAlg (int' m, int' k)))"
-  unfolding mod_def [symmetric] int'_def zmod_int [symmetric]
-  unfolding int'_def [symmetric] nat_of_int_int ..
+lemma nat_of_mlt_int_code [code func, code inline]:
+  "nat_of_ml_int k = nat (int_of_ml_int k)"
+  unfolding nat_of_ml_int_def by simp
 
 
 subsection {* Code generator setup for basic functions *}
@@ -193,13 +210,13 @@
 *}
 
 consts_code
-  int' ("(_)")
+  int_of_nat ("(_)")
   nat ("\<module>nat")
 attach {*
 fun nat i = if i < 0 then 0 else i;
 *}
 
-code_const int'
+code_const int_of_nat
   (SML "_")
   (OCaml "_")
   (Haskell "_")
@@ -395,6 +412,6 @@
   Divides Integer
   Efficient_Nat Integer
 
-hide const nat_of_int int'
+hide const nat_of_int int_of_nat
 
 end

--- a/src/HOL/Library/Pretty_Int.thy	Tue Sep 25 17:06:19 2007 +0200
+++ b/src/HOL/Library/Pretty_Int.thy	Tue Sep 25 21:08:34 2007 +0200
@@ -6,7 +6,7 @@
 header {* Pretty integer literals for code generation *}
 
 theory Pretty_Int
-imports IntArith
+imports IntArith ML_Int
 begin
 
 text {*
@@ -88,6 +88,11 @@
   (OCaml "Big'_int.lt'_big'_int")
   (Haskell infix 4 "<")
 
+code_const ml_int_of_int and int_of_ml_int
+  (SML "IntInf.toInt" and "IntInf.fromInt")
+  (OCaml "Big'_int.int'_of'_big'_int" and "Big'_int.big'_int'_of'_int")
+  (Haskell "_" and "_")
+
 code_reserved SML IntInf
 code_reserved OCaml Big_int