Theory HOL-Library.Code_Target_Int

(*  Title:      HOL/Library/Code_Target_Int.thy
    Author:     Florian Haftmann, TU Muenchen
*)

section ‹Implementation of integer numbers by target-language integers›

theory Code_Target_Int
imports Main
begin

code_datatype int_of_integer

declare [[code drop: integer_of_int]]

context
includes integer.lifting
begin

lemma [code]:
  "integer_of_int (int_of_integer k) = k"
  by transfer rule

lemma [code]:
  "Int.Pos = int_of_integer ∘ integer_of_num"
  by transfer (simp add: fun_eq_iff)

lemma [code]:
  "Int.Neg = int_of_integer ∘ uminus ∘ 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 (- numeral k) = Int.Neg k"
  by transfer simp

context
begin

qualified definition positive :: "num ⇒ int"
  where [simp]: "positive = numeral"

qualified definition negative :: "num ⇒ int"
  where [simp]: "negative = uminus ∘ numeral"

lemma [code_computation_unfold]:
  "numeral = positive"
  "Int.Pos = positive"
  "Int.Neg = negative"
  by (simp_all add: fun_eq_iff)

end

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_post]:
  "int_of_integer (- 1) = - 1"
  by 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

declare [[code drop: Int.sub]]

lemma [code]:
  "k * l = int_of_integer (of_int k * of_int l)"
  by simp

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]:
  "divmod m n = map_prod int_of_integer int_of_integer (divmod m n)"
  unfolding prod_eq_iff divmod_def map_prod_def case_prod_beta fst_conv snd_conv
  by transfer 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

declare [[code drop: "gcd :: int ⇒ _" "lcm :: int ⇒ _"]]

lemma gcd_int_of_integer [code]:
  "gcd (int_of_integer x) (int_of_integer y) = int_of_integer (gcd x y)"
  by transfer rule

lemma lcm_int_of_integer [code]:
  "lcm (int_of_integer x) (int_of_integer y) = int_of_integer (lcm x y)"
  by transfer rule

end

lemma (in ring_1) of_int_code_if:
  "of_int k = (if k = 0 then 0
     else if k < 0 then - of_int (- k)
     else let
       l = 2 * of_int (k div 2);
       j = k mod 2
     in if j = 0 then l else l + 1)"
proof -
  from div_mult_mod_eq have *: "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp
  show ?thesis
    by (simp add: Let_def of_int_add [symmetric]) (simp add: * mult.commute)
qed

declare of_int_code_if [code]

lemma [code]:
  "nat = nat_of_integer ∘ of_int"
  including integer.lifting by transfer (simp add: fun_eq_iff)

definition char_of_int :: "int ⇒ char"
  where [code_abbrev]: "char_of_int = char_of"

definition int_of_char :: "char ⇒ int"
  where [code_abbrev]: "int_of_char = of_char"

lemma [code]:
  "char_of_int = char_of_integer ∘ integer_of_int"
  including integer.lifting unfolding char_of_integer_def char_of_int_def
  by transfer (simp add: fun_eq_iff)

lemma [code]:
  "int_of_char = int_of_integer ∘ integer_of_char"
  including integer.lifting unfolding integer_of_char_def int_of_char_def
  by transfer (simp add: fun_eq_iff)

context
  includes integer.lifting bit_operations_syntax
begin

declare [[code drop: ‹bit :: int ⇒ _› ‹not :: int ⇒ _›
  ‹and :: int ⇒ _› ‹or :: int ⇒ _› ‹xor :: int ⇒ _›
  ‹push_bit :: _ ⇒ _ ⇒ int› ‹drop_bit :: _ ⇒ _ ⇒ int› ‹take_bit :: _ ⇒ _ ⇒ int›]]

lemma [code]:
  ‹bit (int_of_integer k) n ⟷ bit k n›
  by transfer rule

lemma [code]:
  ‹NOT (int_of_integer k) = int_of_integer (NOT k)›
  by transfer rule

lemma [code]:
  ‹int_of_integer k AND int_of_integer l = int_of_integer (k AND l)›
  by transfer rule

lemma [code]:
  ‹int_of_integer k OR int_of_integer l = int_of_integer (k OR l)›
  by transfer rule

lemma [code]:
  ‹int_of_integer k XOR int_of_integer l = int_of_integer (k XOR l)›
  by transfer rule

lemma [code]:
  ‹push_bit n (int_of_integer k) = int_of_integer (push_bit n k)›
  by transfer rule

lemma [code]:
  ‹drop_bit n (int_of_integer k) = int_of_integer (drop_bit n k)›
  by transfer rule

lemma [code]:
  ‹take_bit n (int_of_integer k) = int_of_integer (take_bit n k)›
  by transfer rule

lemma [code]:
  ‹mask n = int_of_integer (mask n)›
  by transfer rule

lemma [code]:
  ‹set_bit n (int_of_integer k) = int_of_integer (set_bit n k)›
  by transfer rule

lemma [code]:
  ‹unset_bit n (int_of_integer k) = int_of_integer (unset_bit n k)›
  by transfer rule

lemma [code]:
  ‹flip_bit n (int_of_integer k) = int_of_integer (flip_bit n k)›
  by transfer rule

end

code_identifier
  code_module Code_Target_Int ⇀
    (SML) Arith and (OCaml) Arith and (Haskell) Arith

end