--- a/src/HOL/Integ/IntArith.thy Tue Aug 08 08:19:39 2006 +0200
+++ b/src/HOL/Integ/IntArith.thy Tue Aug 08 08:19:44 2006 +0200
@@ -361,6 +361,96 @@
apply (frule pos_zmult_eq_1_iff_lemma, auto)
done
+
+subsection {* code generator setup *}
+
+code_alias
+ "Numeral.bin" "IntDef.bin"
+ "Numeral.bit" "IntDef.bit"
+ "Numeral.Pls" "IntDef.Pls"
+ "Numeral.Min" "IntDef.Min"
+ "Numeral.Bit" "IntDef.Bit"
+ "Numeral.Abs_Bin" "IntDef.Bin"
+ "Numeral.Rep_Bin" "IntDef.int_of_bin"
+ "Numeral.B0" "IntDef.B0"
+ "Numeral.B1" "IntDef.B1"
+
+lemma
+ number_of_is_rep_bin [code inline]: "number_of = Rep_Bin"
+proof
+ fix b
+ show "number_of b = Rep_Bin b"
+ unfolding int_number_of_def by simp
+qed
+
+lemma zero_is_num_zero [code, code inline]:
+ "(0::int) = Rep_Bin Numeral.Pls"
+ unfolding Pls_def Abs_Bin_inverse' ..
+
+lemma one_is_num_one [code, code inline]:
+ "(1::int) = Rep_Bin (Numeral.Pls BIT bit.B1)"
+ unfolding Pls_def Bit_def Abs_Bin_inverse' by simp
+
+lemma negate_bin_minus:
+ "(Rep_Bin b :: int) = - Rep_Bin (bin_minus b)"
+ unfolding bin_minus_def Abs_Bin_inverse' by simp
+
+lemmas [code inline] =
+ bin_minus_Pls bin_minus_Min bin_minus_1 bin_minus_0
+ bin_pred_Pls bin_pred_Min bin_pred_1 bin_pred_0
+
+ML {*
+structure Numeral =
+struct
+
+val negate_bin_minus_thm = eq_reflection OF [thm "negate_bin_minus"];
+val number_of_is_rep_bin_thm = eq_reflection OF [thm "number_of_is_rep_bin"];
+
+fun int_of_numeral thy num = HOLogic.dest_binum num
+ handle TERM _
+ => error ("not a number: " ^ Sign.string_of_term thy num);
+
+fun elim_negate thy thms =
+ let
+ val thms' = map (rewrite_rule [number_of_is_rep_bin_thm]) thms;
+ 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.Rep_Bin", _), [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] negate_bin_minus_thm;
+ val rewrites =
+ []
+ |> fold (bins_of o prop_of) thms'
+ |> filter is_negative
+ |> map instantiate_with
+ in if null rewrites then thms' else
+ thms'
+ |> map (rewrite_rule rewrites)
+ end;
+
+end;
+*}
+
+setup {*
+ CodegenTheorems.add_preproc Numeral.elim_negate
+ #> CodegenPackage.add_appconst ("Numeral.Rep_Bin", CodegenPackage.appgen_rep_bin Numeral.int_of_numeral)
+*}
+
+
subsection {* legacy ML bindings *}
ML
--- a/src/HOL/Integ/IntDef.thy Tue Aug 08 08:19:39 2006 +0200
+++ b/src/HOL/Integ/IntDef.thy Tue Aug 08 08:19:44 2006 +0200
@@ -924,23 +924,6 @@
haskell (infix 4 "<=")
ML {*
-fun mk_int_to_nat bin =
- Const ("IntDef.nat", HOLogic.intT --> HOLogic.natT)
- $ (Const ("Numeral.number_of", HOLogic.binT --> HOLogic.intT) $ bin);
-
-fun bin_to_int thy bin = HOLogic.dest_binum bin
- handle TERM _
- => error ("not a number: " ^ Sign.string_of_term thy bin);
-
-fun appgen_number thy tabs (app as ((_, ty), _)) =
- let
- val _ = case strip_type ty
- of (_, Type (ty', [])) => if ty' = "IntDef.int" then ()
- else error ("not integer type: " ^ quote ty');
- in
- CodegenPackage.appgen_number_of bin_to_int thy tabs app
- end;
-
fun number_of_codegen thy defs gr dep module b (Const ("Numeral.number_of",
Type ("fun", [_, T as Type ("IntDef.int", [])])) $ bin) =
(SOME (fst (Codegen.invoke_tycodegen thy defs dep module false (gr, T)),
@@ -951,12 +934,10 @@
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
- (* #> CodegenPackage.add_appconst ("Numeral.number_of", appgen_number) *)
*}
quickcheck_params [default_type = int]
--- a/src/HOL/Integ/NatBin.thy Tue Aug 08 08:19:39 2006 +0200
+++ b/src/HOL/Integ/NatBin.thy Tue Aug 08 08:19:44 2006 +0200
@@ -776,71 +776,13 @@
"(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 elim_nat [code inline]:
- "(number_of n :: nat) = nat (number_of n)"
- by simp
-
-lemma elim_zero [code inline]:
- "(0::int) = number_of (Numeral.Pls)"
- by simp
-
-lemma elim_one [code inline]:
- "(1::int) = number_of (Numeral.Pls BIT bit.B1)"
- by simp
-
-lemma elim_one_nat [code inline]:
- "1 = Suc 0"
- by simp
-
-lemmas [code inline] =
- 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)
+lemma number_of_is_nat_rep_bin [code inline]:
+ "(number_of b :: nat) = nat (Rep_Bin b)"
+ unfolding nat_number_of_def int_number_of_def by simp
-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 *}
--- a/src/HOL/Integ/Numeral.thy Tue Aug 08 08:19:39 2006 +0200
+++ b/src/HOL/Integ/Numeral.thy Tue Aug 08 08:19:44 2006 +0200
@@ -27,7 +27,6 @@
bin = "UNIV::int set"
by (auto)
-
text{*This datatype avoids the use of type @{typ bool}, which would make
all of the rewrite rules higher-order. If the use of datatype causes
problems, this two-element type can easily be formalized using typedef.*}
@@ -87,6 +86,9 @@
bin_mult :: "[bin,bin]=>bin"
"bin_mult v w == Abs_Bin(Rep_Bin v * Rep_Bin w)"
+lemma Abs_Bin_inverse':
+ "Rep_Bin (Abs_Bin x) = x"
+by (rule Abs_Bin_inverse) (auto simp add: Bin_def)
lemmas Bin_simps =
bin_succ_def bin_pred_def bin_minus_def bin_add_def bin_mult_def
--- a/src/HOL/List.thy Tue Aug 08 08:19:39 2006 +0200
+++ b/src/HOL/List.thy Tue Aug 08 08:19:44 2006 +0200
@@ -2726,7 +2726,6 @@
val list_codegen_setup =
Codegen.add_codegen "list_codegen" list_codegen
#> Codegen.add_codegen "char_codegen" char_codegen
- #> CodegenPackage.add_appconst ("Numeral.number_of", appgen_number)
#> fold (CodegenPackage.add_pretty_list "Nil" "Cons") [
("ml", (7, "::")),
("haskell", (5, ":"))
--- a/src/HOL/Nat.thy Tue Aug 08 08:19:39 2006 +0200
+++ b/src/HOL/Nat.thy Tue Aug 08 08:19:44 2006 +0200
@@ -1043,6 +1043,10 @@
subsection {* Code generator setup *}
+lemma one_is_suc_zero [code inline]:
+ "1 = Suc 0"
+ by simp
+
code_alias
"nat" "Nat.nat"
"0" "Nat.Zero"