# HG changeset patch
# User berghofe
# Date 1120219733 -7200
# Node ID 849ec3962b55c97454a20ae95e8cd8c2e8c3be15
# Parent  fce796ad9c2baf66ff5f6eed9f0ee7fa83895d67
Moved code generator setup from NatBin to IntDef.

diff -r fce796ad9c2b -r 849ec3962b55 src/HOL/Integ/IntDef.thy
--- a/src/HOL/Integ/IntDef.thy	Fri Jul 01 14:06:57 2005 +0200
+++ b/src/HOL/Integ/IntDef.thy	Fri Jul 01 14:08:53 2005 +0200
@@ -853,6 +853,65 @@
 done
 
 
+subsection {* Configuration of the code generator *}
+
+ML {*
+infix 7 `*;
+infix 6 `+;
+
+val op `* = op * : int * int -> int;
+val op `+ = op + : int * int -> int;
+val `~ = ~ : int -> int;
+*}
+
+types_code
+  "int" ("int")
+
+constdefs
+  int_aux :: "int \<Rightarrow> nat \<Rightarrow> int"
+  "int_aux i n == (i + int n)"
+  nat_aux :: "nat \<Rightarrow> int \<Rightarrow> nat"
+  "nat_aux n i == (n + nat i)"
+
+lemma [code]:
+  "int_aux i 0 = i"
+  "int_aux i (Suc n) = int_aux (i + 1) n" -- {* tail recursive *}
+  "int n = int_aux 0 n"
+  by (simp add: int_aux_def)+
+
+lemma [code]: "nat_aux n i = (if i <= 0 then n else nat_aux (Suc n) (i - 1))"
+  -- {* tail recursive *}
+  by (auto simp add: nat_aux_def nat_eq_iff linorder_not_le order_less_imp_le
+    dest: zless_imp_add1_zle)
+lemma [code]: "nat i = nat_aux 0 i"
+  by (simp add: nat_aux_def)
+
+consts_code
+  "0" :: "int"                  ("0")
+  "1" :: "int"                  ("1")
+  "uminus" :: "int => int"      ("`~")
+  "op +" :: "int => int => int" ("(_ `+/ _)")
+  "op *" :: "int => int => int" ("(_ `*/ _)")
+  "op <" :: "int => int => bool" ("(_ </ _)")
+  "op <=" :: "int => int => bool" ("(_ <=/ _)")
+  "neg"                         ("(_ < 0)")
+
+ML {*
+fun number_of_codegen thy defs gr s thyname b (Const ("Numeral.number_of",
+      Type ("fun", [_, Type ("IntDef.int", [])])) $ bin) =
+        (SOME (gr, Pretty.str (IntInf.toString (HOLogic.dest_binum bin)))
+        handle TERM _ => NONE)
+  | number_of_codegen thy defs gr s thyname b (Const ("Numeral.number_of",
+      Type ("fun", [_, Type ("nat", [])])) $ bin) =
+        SOME (Codegen.invoke_codegen thy defs s thyname b (gr,
+          Const ("IntDef.nat", HOLogic.intT --> HOLogic.natT) $
+            (Const ("Numeral.number_of", HOLogic.binT --> HOLogic.intT) $ bin)))
+  | number_of_codegen _ _ _ _ _ _ _ = NONE;
+*}
+
+setup {* [Codegen.add_codegen "number_of_codegen" number_of_codegen] *}
+
+
 (*Legacy ML bindings, but no longer the structure Int.*)
 ML
 {*
diff -r fce796ad9c2b -r 849ec3962b55 src/HOL/Integ/NatBin.thy
--- a/src/HOL/Integ/NatBin.thy	Fri Jul 01 14:06:57 2005 +0200
+++ b/src/HOL/Integ/NatBin.thy	Fri Jul 01 14:08:53 2005 +0200
@@ -818,65 +818,4 @@
 val zero_le_even_power = thm"zero_le_even_power";
 *}
 
-
-subsection {* Configuration of the code generator *}
-
-ML {*
-infix 7 `*;
-infix 6 `+;
-
-val op `* = op * : int * int -> int;
-val op `+ = op + : int * int -> int;
-val `~ = ~ : int -> int;
-*}
-
-types_code
-  "int" ("int")
-
-constdefs
-  int_aux :: "int \<Rightarrow> nat \<Rightarrow> int"
-  "int_aux i n == (i + int n)"
-  nat_aux :: "nat \<Rightarrow> int \<Rightarrow> nat"
-  "nat_aux n i == (n + nat i)"
-
-lemma [code]:
-  "int_aux i 0 = i"
-  "int_aux i (Suc n) = int_aux (i + 1) n" -- {* tail recursive *}
-  "int n = int_aux 0 n"
-  by (simp add: int_aux_def)+
-
-lemma [code]: "nat_aux n i = (if i <= 0 then n else nat_aux (Suc n) (i - 1))"
-  by (simp add: nat_aux_def Suc_nat_eq_nat_zadd1) -- {* tail recursive *}
-lemma [code]: "nat i = nat_aux 0 i"
-  by (simp add: nat_aux_def)
-
-consts_code
-  "0" :: "int"                  ("0")
-  "1" :: "int"                  ("1")
-  "uminus" :: "int => int"      ("`~")
-  "op +" :: "int => int => int" ("(_ `+/ _)")
-  "op *" :: "int => int => int" ("(_ `*/ _)")
-(* Fails for 0:
-  "op div" :: "int => int => int" ("(_ div/ _)")
-  "op mod" :: "int => int => int" ("(_ mod/ _)")
-*)
-  "op <" :: "int => int => bool" ("(_ </ _)")
-  "op <=" :: "int => int => bool" ("(_ <=/ _)")
-  "neg"                         ("(_ < 0)")
-
-ML {*
-fun number_of_codegen thy gr s b (Const ("Numeral.number_of",
-      Type ("fun", [_, Type ("IntDef.int", [])])) $ bin) =
-        (SOME (gr, Pretty.str (IntInf.toString (HOLogic.dest_binum bin)))
-        handle TERM _ => NONE)
-  | number_of_codegen thy gr s b (Const ("Numeral.number_of",
-      Type ("fun", [_, Type ("nat", [])])) $ bin) =
-        SOME (Codegen.invoke_codegen thy s b (gr,
-          Const ("IntDef.nat", HOLogic.intT --> HOLogic.natT) $
-            (Const ("Numeral.number_of", HOLogic.binT --> HOLogic.intT) $ bin)))
-  | number_of_codegen _ _ _ _ _ = NONE;
-*}
-
-setup {* [Codegen.add_codegen "number_of_codegen" number_of_codegen] *}
-
 end