treating division by zero properly

--- a/src/HOL/Library/Code_Index.thy	Mon Jan 28 22:27:29 2008 +0100
+++ b/src/HOL/Library/Code_Index.thy	Tue Jan 29 10:19:56 2008 +0100
@@ -180,6 +180,36 @@
 *}
 
 
+subsection {* Specialized @{term "op - \<Colon> index \<Rightarrow> index \<Rightarrow> index"},
+  @{term "op div \<Colon> index \<Rightarrow> index \<Rightarrow> index"} and @{term "op mod \<Colon> index \<Rightarrow> index \<Rightarrow> index"}
+  operations *}
+
+definition
+  minus_index_aux :: "index \<Rightarrow> index \<Rightarrow> index"
+where
+  [code func del]: "minus_index_aux = op -"
+
+lemma [code func]: "op - = minus_index_aux"
+  using minus_index_aux_def ..
+
+definition
+  div_mod_index ::  "index \<Rightarrow> index \<Rightarrow> index \<times> index"
+where
+  [code func del]: "div_mod_index n m = (n div m, n mod m)"
+
+lemma [code func]:
+  "div_mod_index n m = (if m = 0 then (0, n) else (n div m, n mod m))"
+  unfolding div_mod_index_def by auto
+
+lemma [code func]:
+  "n div m = fst (div_mod_index n m)"
+  unfolding div_mod_index_def by simp
+
+lemma [code func]:
+  "n mod m = snd (div_mod_index n m)"
+  unfolding div_mod_index_def by simp
+
+
 subsection {* Code serialization *}
 
 text {* Implementation of indices by bounded integers *}
@@ -205,7 +235,7 @@
   (OCaml "Pervasives.( + )")
   (Haskell infixl 6 "+")
 
-code_const "op - \<Colon> index \<Rightarrow> index \<Rightarrow> index"
+code_const "minus_index_aux \<Colon> index \<Rightarrow> index \<Rightarrow> index"
   (SML "Int.max/ (_/ -/ _,/ 0 : int)")
   (OCaml "Pervasives.max/ (_/ -/ _)/ (0 : int) ")
   (Haskell "max/ (_/ -/ _)/ (0 :: Int)")
@@ -215,15 +245,10 @@
   (OCaml "Pervasives.( * )")
   (Haskell infixl 7 "*")
 
-code_const "op div \<Colon> index \<Rightarrow> index \<Rightarrow> index"
-  (SML "Int.div/ ((_),/ (_))")
-  (OCaml "Pervasives.( / )")
-  (Haskell "div")
-
-code_const "op mod \<Colon> index \<Rightarrow> index \<Rightarrow> index"
-  (SML "Int.mod/ ((_),/ (_))")
-  (OCaml "Pervasives.( mod )")
-  (Haskell "mod")
+code_const div_mod_index
+  (SML "(fn n => fn m =>/ (n div m, n mod m))")
+  (OCaml "(fun n -> fun m ->/ (n '/ m, n mod m))")
+  (Haskell "divMod")
 
 code_const "op = \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
   (SML "!((_ : Int.int) = _)")

--- a/src/HOL/Library/Code_Integer.thy	Mon Jan 28 22:27:29 2008 +0100
+++ b/src/HOL/Library/Code_Integer.thy	Tue Jan 29 10:19:56 2008 +0100
@@ -6,7 +6,7 @@
 header {* Pretty integer literals for code generation *}
 
 theory Code_Integer
-imports Int
+imports Presburger
 begin
 
 text {*

--- a/src/HOL/Library/Efficient_Nat.thy	Mon Jan 28 22:27:29 2008 +0100
+++ b/src/HOL/Library/Efficient_Nat.thy	Tue Jan 29 10:19:56 2008 +0100
@@ -53,13 +53,21 @@
   "n * m = nat (of_nat n * of_nat m)"
   unfolding of_nat_mult [symmetric] by simp
 
-lemma div_nat_code [code]:
-  "n div m = nat (of_nat n div of_nat m)"
-  unfolding zdiv_int [symmetric] by simp
+text {* Specialized @{term "op div \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"} 
+  and @{term "op mod \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"} operations. *}
+
+definition
+  div_mod_nat_aux ::  "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat"
+where
+  [code func del]: "div_mod_nat_aux = Divides.divmod"
 
-lemma mod_nat_code [code]:
-  "n mod m = nat (of_nat n mod of_nat m)"
-  unfolding zmod_int [symmetric] by simp
+lemma [code func]:
+  "Divides.divmod n m = (if m = 0 then (0, n) else div_mod_nat_aux n m)"
+  unfolding div_mod_nat_aux_def divmod_def by simp
+
+lemma div_mod_aux_code [code]:
+  "div_mod_nat_aux n m = (nat (of_nat n div of_nat m), nat (of_nat n mod of_nat m))"
+  unfolding div_mod_nat_aux_def divmod_def zdiv_int [symmetric] zmod_int [symmetric] by simp
 
 lemma eq_nat_code [code]:
   "n = m \<longleftrightarrow> (of_nat n \<Colon> int) = of_nat m"
@@ -380,15 +388,10 @@
   (OCaml "Big'_int.mult'_big'_int")
   (Haskell infixl 7 "*")
 
-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")
+code_const div_mod_nat_aux
+  (SML "IntInf.divMod/ ((_),/ (_))")
+  (OCaml "Big'_int.quomod'_big'_int")
+  (Haskell "divMod")
 
 code_const "op = \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
   (SML "!((_ : IntInf.int) = _)")
@@ -410,8 +413,6 @@
   Suc                          ("(_ +/ 1)")
   "op + \<Colon>  nat \<Rightarrow> nat \<Rightarrow> nat"   ("(_ +/ _)")
   "op * \<Colon>  nat \<Rightarrow> nat \<Rightarrow> nat"   ("(_ */ _)")
-  "op div \<Colon>  nat \<Rightarrow> nat \<Rightarrow> nat" ("(_ div/ _)")
-  "op mod \<Colon>  nat \<Rightarrow> nat \<Rightarrow> nat" ("(_ mod/ _)")
   "op \<le> \<Colon>  nat \<Rightarrow> nat \<Rightarrow> bool"  ("(_ <=/ _)")
   "op < \<Colon>  nat \<Rightarrow> nat \<Rightarrow> bool"  ("(_ </ _)")