--- 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";