Theory Divmod_Int

(*  
    Author:      René Thiemann 
                 Akihisa Yamada
    License:     BSD
*)
section ‹Divmod-Int›

text ‹We provide the divmod-operation on type int for efficiency reasons.›

theory Divmod_Int
imports Main
begin

definition divmod_int :: "int ⇒ int ⇒ int × int" where
  "divmod_int n m = (n div m, n mod m)"

text ‹We implement @{const divmod_int} via @{const divmod_integer}
  instead of invoking both division and modulo separately.›

context
includes integer.lifting
begin

lemma divmod_int_code[code]: "divmod_int m n = map_prod int_of_integer int_of_integer 
  (divmod_integer (integer_of_int m) (integer_of_int n))"
  unfolding divmod_int_def divmod_integer_def map_prod_def split prod.simps
proof 
  show "m div n = int_of_integer
     (integer_of_int m div integer_of_int n)"
    by (transfer, simp)
  show "m mod n = int_of_integer
     (integer_of_int m mod integer_of_int n)"
    by (transfer, simp)
qed
end

end