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