# HG changeset patch
# User haftmann
# Date 1197526143 -3600
# Node ID b337edd55a079b7413a44799fa650f47ecc49fc4
# Parent  0b8baa94b866c02c99bb9866fe5ac2a15881c3d4
target language div and mod

diff -r 0b8baa94b866 -r b337edd55a07 src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Thu Dec 13 07:09:02 2007 +0100
+++ b/src/HOL/Library/Efficient_Nat.thy	Thu Dec 13 07:09:03 2007 +0100
@@ -74,7 +74,7 @@
 *}
 
 lemma [code unfold, code inline del]:
-  "nat_case \<equiv> (\<lambda>f g n. if n = 0 then f else g (n - 1))"
+  "nat_case = (\<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 -
@@ -82,7 +82,7 @@
     show "nat_case f g n = (if n = 0 then f else g (n - 1))"
       by (cases n) simp_all
   qed
-  show "nat_case \<equiv> (\<lambda>f g n. if n = 0 then f else g (n - 1))"
+  show "nat_case = (\<lambda>f g n. if n = 0 then f else g (n - 1))"
     by (rule eq_reflection ext rewrite)+ 
 qed
 
@@ -140,10 +140,10 @@
   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)"
+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)"
+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"
@@ -226,6 +226,18 @@
   (OCaml "_")
   (Haskell "_")
 
+text {* Using target language div and mod *}
+
+code_const "op div \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"
+  (SML "IntInf.div ((_), (_))")
+  (OCaml "Big'_int.div'_big'_int")
+  (Haskell "div")
+
+code_const "op mod \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"
+  (SML "IntInf.mod ((_), (_))")
+  (OCaml "Big'_int.mod'_big'_int")
+  (Haskell "mod")
+
 
 subsection {* Preprocessors *}