1.1 --- a/src/HOL/Library/Code_Index.thy	Mon Jan 28 22:27:29 2008 +0100
     1.2 +++ b/src/HOL/Library/Code_Index.thy	Tue Jan 29 10:19:56 2008 +0100
     1.3 @@ -180,6 +180,36 @@
     1.4  *}
     1.5  
     1.6  
     1.7 +subsection {* Specialized @{term "op - \<Colon> index \<Rightarrow> index \<Rightarrow> index"},
     1.8 +  @{term "op div \<Colon> index \<Rightarrow> index \<Rightarrow> index"} and @{term "op mod \<Colon> index \<Rightarrow> index \<Rightarrow> index"}
     1.9 +  operations *}
    1.10 +
    1.11 +definition
    1.12 +  minus_index_aux :: "index \<Rightarrow> index \<Rightarrow> index"
    1.13 +where
    1.14 +  [code func del]: "minus_index_aux = op -"
    1.15 +
    1.16 +lemma [code func]: "op - = minus_index_aux"
    1.17 +  using minus_index_aux_def ..
    1.18 +
    1.19 +definition
    1.20 +  div_mod_index ::  "index \<Rightarrow> index \<Rightarrow> index \<times> index"
    1.21 +where
    1.22 +  [code func del]: "div_mod_index n m = (n div m, n mod m)"
    1.23 +
    1.24 +lemma [code func]:
    1.25 +  "div_mod_index n m = (if m = 0 then (0, n) else (n div m, n mod m))"
    1.26 +  unfolding div_mod_index_def by auto
    1.27 +
    1.28 +lemma [code func]:
    1.29 +  "n div m = fst (div_mod_index n m)"
    1.30 +  unfolding div_mod_index_def by simp
    1.31 +
    1.32 +lemma [code func]:
    1.33 +  "n mod m = snd (div_mod_index n m)"
    1.34 +  unfolding div_mod_index_def by simp
    1.35 +
    1.36 +
    1.37  subsection {* Code serialization *}
    1.38  
    1.39  text {* Implementation of indices by bounded integers *}
    1.40 @@ -205,7 +235,7 @@
    1.41    (OCaml "Pervasives.( + )")
    1.42    (Haskell infixl 6 "+")
    1.43  
    1.44 -code_const "op - \<Colon> index \<Rightarrow> index \<Rightarrow> index"
    1.45 +code_const "minus_index_aux \<Colon> index \<Rightarrow> index \<Rightarrow> index"
    1.46    (SML "Int.max/ (_/ -/ _,/ 0 : int)")
    1.47    (OCaml "Pervasives.max/ (_/ -/ _)/ (0 : int) ")
    1.48    (Haskell "max/ (_/ -/ _)/ (0 :: Int)")
    1.49 @@ -215,15 +245,10 @@
    1.50    (OCaml "Pervasives.( * )")
    1.51    (Haskell infixl 7 "*")
    1.52  
    1.53 -code_const "op div \<Colon> index \<Rightarrow> index \<Rightarrow> index"
    1.54 -  (SML "Int.div/ ((_),/ (_))")
    1.55 -  (OCaml "Pervasives.( / )")
    1.56 -  (Haskell "div")
    1.57 -
    1.58 -code_const "op mod \<Colon> index \<Rightarrow> index \<Rightarrow> index"
    1.59 -  (SML "Int.mod/ ((_),/ (_))")
    1.60 -  (OCaml "Pervasives.( mod )")
    1.61 -  (Haskell "mod")
    1.62 +code_const div_mod_index
    1.63 +  (SML "(fn n => fn m =>/ (n div m, n mod m))")
    1.64 +  (OCaml "(fun n -> fun m ->/ (n '/ m, n mod m))")
    1.65 +  (Haskell "divMod")
    1.66  
    1.67  code_const "op = \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
    1.68    (SML "!((_ : Int.int) = _)")

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

     3.1 --- a/src/HOL/Library/Efficient_Nat.thy	Mon Jan 28 22:27:29 2008 +0100
     3.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Tue Jan 29 10:19:56 2008 +0100
     3.3 @@ -53,13 +53,21 @@
     3.4    "n * m = nat (of_nat n * of_nat m)"
     3.5    unfolding of_nat_mult [symmetric] by simp
     3.6  
     3.7 -lemma div_nat_code [code]:
     3.8 -  "n div m = nat (of_nat n div of_nat m)"
     3.9 -  unfolding zdiv_int [symmetric] by simp
    3.10 +text {* Specialized @{term "op div \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"} 
    3.11 +  and @{term "op mod \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"} operations. *}
    3.12  
    3.13 -lemma mod_nat_code [code]:
    3.14 -  "n mod m = nat (of_nat n mod of_nat m)"
    3.15 -  unfolding zmod_int [symmetric] by simp
    3.16 +definition
    3.17 +  div_mod_nat_aux ::  "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat"
    3.18 +where
    3.19 +  [code func del]: "div_mod_nat_aux = Divides.divmod"
    3.20 +
    3.21 +lemma [code func]:
    3.22 +  "Divides.divmod n m = (if m = 0 then (0, n) else div_mod_nat_aux n m)"
    3.23 +  unfolding div_mod_nat_aux_def divmod_def by simp
    3.24 +
    3.25 +lemma div_mod_aux_code [code]:
    3.26 +  "div_mod_nat_aux n m = (nat (of_nat n div of_nat m), nat (of_nat n mod of_nat m))"
    3.27 +  unfolding div_mod_nat_aux_def divmod_def zdiv_int [symmetric] zmod_int [symmetric] by simp
    3.28  
    3.29  lemma eq_nat_code [code]:
    3.30    "n = m \<longleftrightarrow> (of_nat n \<Colon> int) = of_nat m"
    3.31 @@ -380,15 +388,10 @@
    3.32    (OCaml "Big'_int.mult'_big'_int")
    3.33    (Haskell infixl 7 "*")
    3.34  
    3.35 -code_const "op div \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"
    3.36 -  (SML "IntInf.div/ ((_),/ (_))")
    3.37 -  (OCaml "Big'_int.div'_big'_int")
    3.38 -  (Haskell "div")
    3.39 -
    3.40 -code_const "op mod \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"
    3.41 -  (SML "IntInf.mod/ ((_),/ (_))")
    3.42 -  (OCaml "Big'_int.mod'_big'_int")
    3.43 -  (Haskell "mod")
    3.44 +code_const div_mod_nat_aux
    3.45 +  (SML "IntInf.divMod/ ((_),/ (_))")
    3.46 +  (OCaml "Big'_int.quomod'_big'_int")
    3.47 +  (Haskell "divMod")
    3.48  
    3.49  code_const "op = \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
    3.50    (SML "!((_ : IntInf.int) = _)")
    3.51 @@ -410,8 +413,6 @@
    3.52    Suc                          ("(_ +/ 1)")
    3.53    "op + \<Colon>  nat \<Rightarrow> nat \<Rightarrow> nat"   ("(_ +/ _)")
    3.54    "op * \<Colon>  nat \<Rightarrow> nat \<Rightarrow> nat"   ("(_ */ _)")
    3.55 -  "op div \<Colon>  nat \<Rightarrow> nat \<Rightarrow> nat" ("(_ div/ _)")
    3.56 -  "op mod \<Colon>  nat \<Rightarrow> nat \<Rightarrow> nat" ("(_ mod/ _)")
    3.57    "op \<le> \<Colon>  nat \<Rightarrow> nat \<Rightarrow> bool"  ("(_ <=/ _)")
    3.58    "op < \<Colon>  nat \<Rightarrow> nat \<Rightarrow> bool"  ("(_ </ _)")
    3.59