header {* Implementation of integer numbers by target-language integers *}
theory Code_Target_Int
imports Main
begin
code_datatype int_of_integer
lemma [code, code del]:
"integer_of_int = integer_of_int" ..
lemma [code]:
"integer_of_int (int_of_integer k) = k"
by transfer rule
lemma [code]:
"Int.Pos = int_of_integer o integer_of_num"
by transfer (simp add: fun_eq_iff)
lemma [code]:
"Int.Neg = int_of_integer o uminus o integer_of_num"
by transfer (simp add: fun_eq_iff)
lemma [code_abbrev]:
"int_of_integer (numeral k) = Int.Pos k"
by transfer simp
lemma [code_abbrev]:
"int_of_integer (neg_numeral k) = Int.Neg k"
by transfer simp
lemma [code, symmetric, code_post]:
"0 = int_of_integer 0"
by transfer simp
lemma [code, symmetric, code_post]:
"1 = int_of_integer 1"
by transfer simp
lemma [code]:
"k + l = int_of_integer (of_int k + of_int l)"
by transfer simp
lemma [code]:
"- k = int_of_integer (- of_int k)"
by transfer simp
lemma [code]:
"k - l = int_of_integer (of_int k - of_int l)"
by transfer simp
lemma [code]:
"Int.dup k = int_of_integer (Code_Numeral.dup (of_int k))"
by transfer simp
lemma [code, code del]:
"Int.sub = Int.sub" ..
lemma [code]:
"k * l = int_of_integer (of_int k * of_int l)"
by simp
lemma [code]:
"pdivmod k l = map_pair int_of_integer int_of_integer
(Code_Numeral.divmod_abs (of_int k) (of_int l))"
by (simp add: prod_eq_iff pdivmod_def)
lemma [code]:
"k div l = int_of_integer (of_int k div of_int l)"
by simp
lemma [code]:
"k mod l = int_of_integer (of_int k mod of_int l)"
by simp
lemma [code]:
"HOL.equal k l = HOL.equal (of_int k :: integer) (of_int l)"
by transfer (simp add: equal)
lemma [code]:
"k ≤ l <-> (of_int k :: integer) ≤ of_int l"
by transfer rule
lemma [code]:
"k < l <-> (of_int k :: integer) < of_int l"
by transfer rule
lemma (in ring_1) of_int_code:
"of_int k = (if k = 0 then 0
else if k < 0 then - of_int (- k)
else let
(l, j) = divmod_int k 2;
l' = 2 * of_int l
in if j = 0 then l' else l' + 1)"
proof -
from mod_div_equality have *: "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp
show ?thesis
by (simp add: Let_def divmod_int_mod_div mod_2_not_eq_zero_eq_one_int
of_int_add [symmetric]) (simp add: * mult_commute)
qed
declare of_int_code [code]
lemma [code]:
"nat = nat_of_integer o of_int"
by transfer (simp add: fun_eq_iff)
code_modulename SML
Code_Target_Int Arith
code_modulename OCaml
Code_Target_Int Arith
code_modulename Haskell
Code_Target_Int Arith
end