# HG changeset patch
# User haftmann
# Date 1147162228 -7200
# Node ID 299d4cd2ef518604a16ca7bbf6432c26d458f1fe
# Parent  2d969d9a233bcfe7288a1aeb88b01553f7e83c56
added codegen preprocessors for numerals

diff -r 2d969d9a233b -r 299d4cd2ef51 src/HOL/Integ/IntArith.thy
--- a/src/HOL/Integ/IntArith.thy	Tue May 09 10:10:12 2006 +0200
+++ b/src/HOL/Integ/IntArith.thy	Tue May 09 10:10:28 2006 +0200
@@ -364,6 +364,8 @@
  apply (frule pos_zmult_eq_1_iff_lemma, auto) 
 done
 
+subsection {* legacy ML bindings *}
+
 ML
 {*
 val zle_diff1_eq = thm "zle_diff1_eq";
diff -r 2d969d9a233b -r 299d4cd2ef51 src/HOL/Integ/IntDef.thy
--- a/src/HOL/Integ/IntDef.thy	Tue May 09 10:10:12 2006 +0200
+++ b/src/HOL/Integ/IntDef.thy	Tue May 09 10:10:28 2006 +0200
@@ -890,6 +890,10 @@
 lemma [code]: "nat i = nat_aux 0 i"
   by (simp add: nat_aux_def)
 
+lemma [code unfolt]:
+  "neg k = (k < 0)"
+  unfolding neg_def ..
+
 consts_code
   "0" :: "int"                       ("0")
   "1" :: "int"                       ("1")
@@ -908,9 +912,6 @@
   "0 :: int"
     ml (target_atom "(0:IntInf.int)")
     haskell (target_atom "0")
-  "1 :: int"
-    ml (target_atom "(1:IntInf.int)")
-    haskell (target_atom "1")
   "op + :: int \<Rightarrow> int \<Rightarrow> int"
     ml (infixl 8 "+")
     haskell (infixl 6 "+")
@@ -929,9 +930,6 @@
   "op <= :: int \<Rightarrow> int \<Rightarrow> bool"
     ml (infix 6 "<=")
     haskell (infix 4 "<=")
-  "neg :: int \<Rightarrow> bool"
-    ml ("_/ </ 0")
-    haskell ("_/ </ 0")
 
 ML {*
 fun mk_int_to_nat bin =
@@ -956,10 +954,11 @@
 *}
 
 setup {*
-  Codegen.add_codegen "number_of_codegen" number_of_codegen #>
-  CodegenPackage.add_appconst
-    ("Numeral.number_of", ((1, 1), CodegenPackage.appgen_number_of mk_int_to_nat bin_to_int "IntDef.int" "nat")) #>
-  CodegenPackage.set_int_tyco "IntDef.int"
+  Codegen.add_codegen "number_of_codegen" number_of_codegen
+  #> CodegenPackage.add_appconst
+       ("Numeral.number_of", ((1, 1),
+          CodegenPackage.appgen_number_of bin_to_int))
+  #> CodegenPackage.set_int_tyco "IntDef.int"
 *}
 
 quickcheck_params [default_type = int]
diff -r 2d969d9a233b -r 299d4cd2ef51 src/HOL/Integ/NatBin.thy
--- a/src/HOL/Integ/NatBin.thy	Tue May 09 10:10:12 2006 +0200
+++ b/src/HOL/Integ/NatBin.thy	Tue May 09 10:10:28 2006 +0200
@@ -781,6 +781,77 @@
      "(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)"
 by (simp add: nat_mult_div_cancel1)
 
+subsection {* code generator setup *}
+
+lemma number_of_eval [code fun]:
+  "number_of Numeral.Pls = (0::int)"
+  and "number_of Numeral.Min = uminus (1::int)"
+  and "number_of (n BIT bit.B0) = (2::int) * number_of n"
+  and "number_of (n BIT bit.B1) = (2::int) * number_of n + 1"
+  by simp_all
+
+lemma elim_nat [code unfolt]:
+  "(number_of n :: nat) = nat (number_of n)"
+  by simp
+
+lemma elim_zero [code unfolt]:
+  "(0::int) = number_of (Numeral.Pls)" 
+  by simp
+
+lemma elim_one [code unfolt]:
+  "(1::int) = number_of (Numeral.Pls BIT bit.B1)" 
+  by simp
+
+lemmas [code unfolt] =
+  bin_minus_Pls bin_minus_Min bin_minus_1 bin_minus_0
+  bin_pred_Pls  bin_pred_Min  bin_pred_1  bin_pred_0
+
+lemma elim_negate:
+  "(number_of n :: int) == - number_of (bin_minus n)"
+  unfolding number_of_minus IntDef.zminus_zminus by (rule reflexive)
+
+ML {*
+local
+  val elim_negate_thm = thm "elim_negate";
+in fun elim_negate thy thms =
+  let
+    fun bins_of (Const _) =
+          I
+      | bins_of (Var _) =
+          I
+      | bins_of (Free _) =
+          I
+      | bins_of (Bound _) =
+          I
+      | bins_of (Abs (_, _, t)) =
+          bins_of t
+      | bins_of (t as _ $ _) =
+          case strip_comb t
+           of (Const ("Numeral.number_of", _), [bin]) => cons bin
+            | (t', ts) => bins_of t' #> fold bins_of ts;
+    fun is_negative bin = case try HOLogic.dest_binum bin
+     of SOME i => i < 0
+      | _ => false;
+    fun instantiate_with bin =
+      Drule.instantiate' [] [(SOME o cterm_of thy) bin] elim_negate_thm;
+    val rewrites  =
+      []
+      |> fold (bins_of o prop_of) thms
+      |> filter is_negative
+      |> map instantiate_with
+  in
+    thms
+    |> map (rewrite_rule rewrites)
+  end;
+end; (*local*)
+*}
+
+setup {*
+  CodegenTheorems.add_preproc elim_negate
+*}
+
+subsection {* legacy ML bindings *}
+
 ML
 {*
 val eq_nat_nat_iff = thm"eq_nat_nat_iff";