# HG changeset patch
# User haftmann
# Date 1200901407 -3600
# Node ID 042e877d984142250b56eca9d82ed6c0cad47788
# Parent  9c544dac6269e9a687210efa869e0706a58acdd2
tuned code setup

diff -r 9c544dac6269 -r 042e877d9841 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Fri Jan 18 20:34:28 2008 +0100
+++ b/src/HOL/Int.thy	Mon Jan 21 08:43:27 2008 +0100
@@ -1610,8 +1610,8 @@
   with ge show ?thesis by fast
 qed
 
-                     (* `set:int': dummy construction *)
-theorem int_gr_induct[case_names base step,induct set:int]:
+(* `set:int': dummy construction *)
+theorem int_gr_induct [case_names base step, induct set: int]:
   assumes gr: "k < (i::int)" and
         base: "P(k+1)" and
         step: "\<And>i. \<lbrakk>k < i; P i\<rbrakk> \<Longrightarrow> P(i+1)"
@@ -1737,16 +1737,13 @@
 
 definition
   int_aux :: "nat \<Rightarrow> int \<Rightarrow> int" where
-  "int_aux n i = int n + i"
+  [code func del]: "int_aux = of_nat_aux"
 
-lemma [code]:
-  "int_aux 0 i  = i"
-  "int_aux (Suc n) i = int_aux n (i + 1)" -- {* tail recursive *}
-  by (simp add: int_aux_def)+
+lemmas int_aux_code = of_nat_aux_code [where ?'a = int, simplified int_aux_def [symmetric], code]
 
 lemma [code, code unfold, code inline del]:
-  "int n = int_aux n 0"
-  by (simp add: int_aux_def)
+  "of_nat n = int_aux n 0"
+  by (simp add: int_aux_def of_nat_aux_def)
 
 definition
   nat_aux :: "int \<Rightarrow> nat \<Rightarrow> nat" where
@@ -1760,6 +1757,8 @@
 lemma [code]: "nat i = nat_aux i 0"
   by (simp add: nat_aux_def)
 
+hide (open) const int_aux nat_aux
+
 lemma zero_is_num_zero [code func, code inline, symmetric, code post]:
   "(0\<Colon>int) = Numeral0" 
   by simp
@@ -1769,22 +1768,13 @@
   by simp 
 
 code_modulename SML
-  IntDef Integer
+  Int Integer
 
 code_modulename OCaml
-  IntDef Integer
+  Int Integer
 
 code_modulename Haskell
-  IntDef Integer
-
-code_modulename SML
-  Numeral Integer
-
-code_modulename OCaml
-  Numeral Integer
-
-code_modulename Haskell
-  Numeral Integer
+  Int Integer
 
 types_code
   "int" ("int")
diff -r 9c544dac6269 -r 042e877d9841 src/HOL/Library/Code_Index.thy
--- a/src/HOL/Library/Code_Index.thy	Fri Jan 18 20:34:28 2008 +0100
+++ b/src/HOL/Library/Code_Index.thy	Mon Jan 21 08:43:27 2008 +0100
@@ -133,7 +133,7 @@
 
 end
 
-lemma index_of_nat_code [code func]:
+lemma index_of_nat_code [code]:
   "index_of_nat = of_nat"
 proof
   fix n :: nat
@@ -143,9 +143,21 @@
     by (rule sym)
 qed
 
-lemma nat_of_index_code [code func]:
-  "nat_of_index n = (if n = 0 then 0 else Suc (nat_of_index (n - 1)))"
-  by (induct n) simp
+lemma index_not_eq_zero: "i \<noteq> index_of_nat 0 \<longleftrightarrow> i \<ge> 1"
+  by (cases i) auto
+
+definition
+  nat_of_index_aux :: "index \<Rightarrow> nat \<Rightarrow> nat"
+where
+  "nat_of_index_aux i n = nat_of_index i + n"
+
+lemma nat_of_index_aux_code [code]:
+  "nat_of_index_aux i n = (if i = 0 then n else nat_of_index_aux (i - 1) (Suc n))"
+  by (auto simp add: nat_of_index_aux_def index_not_eq_zero)
+
+lemma nat_of_index_code [code]:
+  "nat_of_index i = nat_of_index_aux i 0"
+  by (simp add: nat_of_index_aux_def)
 
 
 subsection {* ML interface *}
@@ -154,7 +166,7 @@
 structure Index =
 struct
 
-fun mk k = @{term index_of_nat} $ HOLogic.mk_number @{typ index} k;
+fun mk k = HOLogic.mk_number @{typ index} k;
 
 end;
 *}
@@ -173,19 +185,15 @@
   (Haskell -)
 
 setup {*
-  fold (fn target => CodeTarget.add_pretty_numeral target false
-    @{const_name number_index_inst.number_of_index}
-    @{const_name Int.B0} @{const_name Int.B1}
-    @{const_name Int.Pls} @{const_name Int.Min}
-    @{const_name Int.Bit}
-  ) ["SML", "OCaml", "Haskell"]
+  fold (Numeral.add_code @{const_name number_index_inst.number_of_index}
+    false false) ["SML", "OCaml", "Haskell"]
 *}
 
 code_reserved SML Int int
 code_reserved OCaml Pervasives int
 
 code_const "op + \<Colon> index \<Rightarrow> index \<Rightarrow> index"
-  (SML "Int.+ ((_), (_))")
+  (SML "Int.+/ ((_),/ (_))")
   (OCaml "Pervasives.+")
   (Haskell infixl 6 "+")
 
@@ -195,33 +203,33 @@
   (Haskell "max/ (_/ -/ _)/ (0 :: Int)")
 
 code_const "op * \<Colon> index \<Rightarrow> index \<Rightarrow> index"
-  (SML "Int.* ((_), (_))")
+  (SML "Int.*/ ((_),/ (_))")
   (OCaml "Pervasives.*")
   (Haskell infixl 7 "*")
 
+code_const "op div \<Colon> index \<Rightarrow> index \<Rightarrow> index"
+  (SML "Int.div/ ((_),/ (_))")
+  (OCaml "Pervasives.div")
+  (Haskell "div")
+
+code_const "op mod \<Colon> index \<Rightarrow> index \<Rightarrow> index"
+  (SML "Int.mod/ ((_),/ (_))")
+  (OCaml "Pervasives.mod")
+  (Haskell "mod")
+
 code_const "op = \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
   (SML "!((_ : Int.int) = _)")
   (OCaml "!((_ : Pervasives.int) = _)")
   (Haskell infixl 4 "==")
 
 code_const "op \<le> \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
-  (SML "Int.<= ((_), (_))")
+  (SML "Int.<=/ ((_),/ (_))")
   (OCaml "!((_ : Pervasives.int) <= _)")
   (Haskell infix 4 "<=")
 
 code_const "op < \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
-  (SML "Int.< ((_), (_))")
+  (SML "Int.</ ((_),/ (_))")
   (OCaml "!((_ : Pervasives.int) < _)")
   (Haskell infix 4 "<")
 
-code_const "op div \<Colon> index \<Rightarrow> index \<Rightarrow> index"
-  (SML "IntInf.div ((_), (_))")
-  (OCaml "Big'_int.div'_big'_int")
-  (Haskell "div")
-
-code_const "op mod \<Colon> index \<Rightarrow> index \<Rightarrow> index"
-  (SML "IntInf.mod ((_), (_))")
-  (OCaml "Big'_int.mod'_big'_int")
-  (Haskell "mod")
-
 end
diff -r 9c544dac6269 -r 042e877d9841 src/HOL/Library/Code_Integer.thy
--- a/src/HOL/Library/Code_Integer.thy	Fri Jan 18 20:34:28 2008 +0100
+++ b/src/HOL/Library/Code_Integer.thy	Mon Jan 21 08:43:27 2008 +0100
@@ -24,12 +24,8 @@
   (Haskell -)
 
 setup {*
-  fold (fn target => CodeTarget.add_pretty_numeral target true
-    @{const_name number_int_inst.number_of_int}
-    @{const_name Int.B0} @{const_name Int.B1}
-    @{const_name Int.Pls} @{const_name Int.Min}
-    @{const_name Int.Bit}
-  ) ["SML", "OCaml", "Haskell"]
+  fold (Numeral.add_code @{const_name number_int_inst.number_of_int}
+    true true) ["SML", "OCaml", "Haskell"]
 *}
 
 code_const "Int.Pls" and "Int.Min" and "Int.Bit"
diff -r 9c544dac6269 -r 042e877d9841 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Fri Jan 18 20:34:28 2008 +0100
+++ b/src/HOL/Nat.thy	Mon Jan 21 08:43:27 2008 +0100
@@ -1176,6 +1176,20 @@
 lemma of_nat_mult: "of_nat (m * n) = of_nat m * of_nat n"
   by (induct m) (simp_all add: add_ac left_distrib)
 
+definition
+  of_nat_aux :: "nat \<Rightarrow> 'a \<Rightarrow> 'a"
+where
+  [code func del]: "of_nat_aux n i = of_nat n + i"
+
+lemma of_nat_aux_code [code]:
+  "of_nat_aux 0 i = i"
+  "of_nat_aux (Suc n) i = of_nat_aux n (i + 1)" -- {* tail recursive *}
+  by (simp_all add: of_nat_aux_def add_ac)
+
+lemma of_nat_code [code]:
+  "of_nat n = of_nat_aux n 0"
+  by (simp add: of_nat_aux_def)
+
 end
 
 context ordered_semidom