Session Native_Word

Theory More_Bits_Int

(*  Title:      Bits_Int.thy
    Author:     Andreas Lochbihler, ETH Zurich
*)

chapter ‹More bit operations on integers›

theory More_Bits_Int
imports
  "Word_Lib.Bits_Int"
  "Word_Lib.Bit_Comprehension"
begin

text ‹Preliminaries›

declare hd_Nil_eq_last [simp]

lemma nat_LEAST_True: "(LEAST _ :: nat. True) = 0"
  by (rule Least_equality) simp_all

text ‹
  Use this function to convert numeral @{typ integer}s quickly into @{typ int}s.
  By default, it works only for symbolic evaluation; normally generated code raises
  an exception at run-time. If theory Code_Target_Bits_Int› is imported,
  it works again, because then @{typ int} is implemented in terms of @{typ integer}
  even for symbolic evaluation.
›

definition int_of_integer_symbolic :: "integer  int"
  where "int_of_integer_symbolic = int_of_integer"

lemma int_of_integer_symbolic_aux_code [code nbe]:
  "int_of_integer_symbolic 0 = 0"
  "int_of_integer_symbolic (Code_Numeral.Pos n) = Int.Pos n"
  "int_of_integer_symbolic (Code_Numeral.Neg n) = Int.Neg n"
  by (simp_all add: int_of_integer_symbolic_def)


section ‹Symbolic bit operations on numerals and @{typ int}s›

fun bitOR_num :: "num  num  num"
where
  "bitOR_num num.One num.One = num.One"
| "bitOR_num num.One (num.Bit0 n) = num.Bit1 n"
| "bitOR_num num.One (num.Bit1 n) = num.Bit1 n"
| "bitOR_num (num.Bit0 m) num.One = num.Bit1 m"
| "bitOR_num (num.Bit0 m) (num.Bit0 n) = num.Bit0 (bitOR_num m n)"
| "bitOR_num (num.Bit0 m) (num.Bit1 n) = num.Bit1 (bitOR_num m n)"
| "bitOR_num (num.Bit1 m) num.One = num.Bit1 m"
| "bitOR_num (num.Bit1 m) (num.Bit0 n) = num.Bit1 (bitOR_num m n)"
| "bitOR_num (num.Bit1 m) (num.Bit1 n) = num.Bit1 (bitOR_num m n)"

fun bitAND_num :: "num  num  num option"
where
  "bitAND_num num.One num.One = Some num.One"
| "bitAND_num num.One (num.Bit0 n) = None"
| "bitAND_num num.One (num.Bit1 n) = Some num.One"
| "bitAND_num (num.Bit0 m) num.One = None"
| "bitAND_num (num.Bit0 m) (num.Bit0 n) = map_option num.Bit0 (bitAND_num m n)"
| "bitAND_num (num.Bit0 m) (num.Bit1 n) = map_option num.Bit0 (bitAND_num m n)"
| "bitAND_num (num.Bit1 m) num.One = Some num.One"
| "bitAND_num (num.Bit1 m) (num.Bit0 n) = map_option num.Bit0 (bitAND_num m n)"
| "bitAND_num (num.Bit1 m) (num.Bit1 n) = (case bitAND_num m n of None  Some num.One | Some n'  Some (num.Bit1 n'))"

fun bitXOR_num :: "num  num  num option"
where
  "bitXOR_num num.One num.One = None"
| "bitXOR_num num.One (num.Bit0 n) = Some (num.Bit1 n)"
| "bitXOR_num num.One (num.Bit1 n) = Some (num.Bit0 n)"
| "bitXOR_num (num.Bit0 m) num.One = Some (num.Bit1 m)"
| "bitXOR_num (num.Bit0 m) (num.Bit0 n) = map_option num.Bit0 (bitXOR_num m n)"
| "bitXOR_num (num.Bit0 m) (num.Bit1 n) = Some (case bitXOR_num m n of None  num.One | Some n'  num.Bit1 n')"
| "bitXOR_num (num.Bit1 m) num.One = Some (num.Bit0 m)"
| "bitXOR_num (num.Bit1 m) (num.Bit0 n) = Some (case bitXOR_num m n of None  num.One | Some n'  num.Bit1 n')"
| "bitXOR_num (num.Bit1 m) (num.Bit1 n) = map_option num.Bit0 (bitXOR_num m n)"

fun bitORN_num :: "num  num  num"
where
  "bitORN_num num.One num.One = num.One"
| "bitORN_num num.One (num.Bit0 m) = num.Bit1 m"
| "bitORN_num num.One (num.Bit1 m) = num.Bit1 m"
| "bitORN_num (num.Bit0 n) num.One = num.Bit0 num.One"
| "bitORN_num (num.Bit0 n) (num.Bit0 m) = Num.BitM (bitORN_num n m)"
| "bitORN_num (num.Bit0 n) (num.Bit1 m) = num.Bit0 (bitORN_num n m)"
| "bitORN_num (num.Bit1 n) num.One = num.One"
| "bitORN_num (num.Bit1 n) (num.Bit0 m) = Num.BitM (bitORN_num n m)"
| "bitORN_num (num.Bit1 n) (num.Bit1 m) = Num.BitM (bitORN_num n m)"

fun bitANDN_num :: "num  num  num option"
where
  "bitANDN_num num.One num.One = None"
| "bitANDN_num num.One (num.Bit0 n) = Some num.One"
| "bitANDN_num num.One (num.Bit1 n) = None"
| "bitANDN_num (num.Bit0 m) num.One = Some (num.Bit0 m)"
| "bitANDN_num (num.Bit0 m) (num.Bit0 n) = map_option num.Bit0 (bitANDN_num m n)"
| "bitANDN_num (num.Bit0 m) (num.Bit1 n) = map_option num.Bit0 (bitANDN_num m n)"
| "bitANDN_num (num.Bit1 m) num.One = Some (num.Bit0 m)"
| "bitANDN_num (num.Bit1 m) (num.Bit0 n) = (case bitANDN_num m n of None  Some num.One | Some n'  Some (num.Bit1 n'))"
| "bitANDN_num (num.Bit1 m) (num.Bit1 n) = map_option num.Bit0 (bitANDN_num m n)"

lemma int_numeral_bitOR_num: "numeral n OR numeral m = (numeral (bitOR_num n m) :: int)"
by(induct n m rule: bitOR_num.induct) simp_all

lemma int_numeral_bitAND_num: "numeral n AND numeral m = (case bitAND_num n m of None  0 :: int | Some n'  numeral n')"
by(induct n m rule: bitAND_num.induct)(simp_all split: option.split)

lemma int_numeral_bitXOR_num:
  "numeral m XOR numeral n = (case bitXOR_num m n of None  0 :: int | Some n'  numeral n')"
by(induct m n rule: bitXOR_num.induct)(simp_all split: option.split)

lemma int_or_not_bitORN_num:
  "numeral n OR NOT (numeral m) = (- numeral (bitORN_num n m) :: int)"
  by (induction n m rule: bitORN_num.induct) (simp_all add: add_One BitM_inc_eq)

lemma int_and_not_bitANDN_num:
  "numeral n AND NOT (numeral m) = (case bitANDN_num n m of None  0 :: int | Some n'  numeral n')"
  by (induction n m rule: bitANDN_num.induct) (simp_all add: add_One BitM_inc_eq split: option.split)

lemma int_not_and_bitANDN_num:
  "NOT (numeral m) AND numeral n = (case bitANDN_num n m of None  0 :: int | Some n'  numeral n')"
by(simp add: int_and_not_bitANDN_num[symmetric] int_and_comm)

code_identifier
  code_module More_Bits_Int 
  (SML) Bit_Operations and (OCaml) Bit_Operations and (Haskell) Bit_Operations and (Scala) Bit_Operations

end

Theory Code_Symbolic_Bits_Int

(*  Title:      Code_Symbolic_Bits_Int.thy
    Author:     Andreas Lochbihler, ETH Zurich
*)

chapter ‹Symbolic implementation of bit operations on int›

theory Code_Symbolic_Bits_Int
imports
  "Word_Lib.Generic_set_bit"
  "Word_Lib.Least_significant_bit"
  More_Bits_Int
begin

section ‹Implementations of bit operations on typ‹int› operating on symbolic representation›

lemma test_bit_int_code [code]:
  "bit (0::int)          n = False"
  "bit (Int.Neg num.One) n = True"
  "bit (Int.Pos num.One)      0 = True"
  "bit (Int.Pos (num.Bit0 m)) 0 = False"
  "bit (Int.Pos (num.Bit1 m)) 0 = True"
  "bit (Int.Neg (num.Bit0 m)) 0 = False"
  "bit (Int.Neg (num.Bit1 m)) 0 = True"
  "bit (Int.Pos num.One)      (Suc n) = False"
  "bit (Int.Pos (num.Bit0 m)) (Suc n) = bit (Int.Pos m) n"
  "bit (Int.Pos (num.Bit1 m)) (Suc n) = bit (Int.Pos m) n"
  "bit (Int.Neg (num.Bit0 m)) (Suc n) = bit (Int.Neg m) n"
  "bit (Int.Neg (num.Bit1 m)) (Suc n) = bit (Int.Neg (Num.inc m)) n"
  by (simp_all add: Num.add_One bit_Suc)

lemma int_not_code [code]:
  "NOT (0 :: int) = -1"
  "NOT (Int.Pos n) = Int.Neg (Num.inc n)"
  "NOT (Int.Neg n) = Num.sub n num.One"
by(simp_all add: Num.add_One int_not_def)

lemma int_and_code [code]: fixes i j :: int shows
  "0 AND j = 0"
  "i AND 0 = 0"
  "Int.Pos n AND Int.Pos m = (case bitAND_num n m of None  0 | Some n'  Int.Pos n')"
  "Int.Neg n AND Int.Neg m = NOT (Num.sub n num.One OR Num.sub m num.One)"
  "Int.Pos n AND Int.Neg num.One = Int.Pos n"
  "Int.Pos n AND Int.Neg (num.Bit0 m) = Num.sub (bitORN_num (Num.BitM m) n) num.One"
  "Int.Pos n AND Int.Neg (num.Bit1 m) = Num.sub (bitORN_num (num.Bit0 m) n) num.One"
  "Int.Neg num.One AND Int.Pos m = Int.Pos m"
  "Int.Neg (num.Bit0 n) AND Int.Pos m = Num.sub (bitORN_num (Num.BitM n) m) num.One"
  "Int.Neg (num.Bit1 n) AND Int.Pos m = Num.sub (bitORN_num (num.Bit0 n) m) num.One"
           apply (simp_all add: int_numeral_bitAND_num Num.add_One
              sub_inc_One_eq inc_BitM_eq not_minus_numeral_inc_eq
              flip: int_not_neg_numeral int_or_not_bitORN_num split: option.split)
   apply (simp_all add: ac_simps)
  done

lemma int_or_code [code]: fixes i j :: int shows
  "0 OR j = j"
  "i OR 0 = i"
  "Int.Pos n OR Int.Pos m = Int.Pos (bitOR_num n m)"
  "Int.Neg n OR Int.Neg m = NOT (Num.sub n num.One AND Num.sub m num.One)"
  "Int.Pos n OR Int.Neg num.One = Int.Neg num.One"
  "Int.Pos n OR Int.Neg (num.Bit0 m) = (case bitANDN_num (Num.BitM m) n of None  -1 | Some n'  Int.Neg (Num.inc n'))"
  "Int.Pos n OR Int.Neg (num.Bit1 m) = (case bitANDN_num (num.Bit0 m) n of None  -1 | Some n'  Int.Neg (Num.inc n'))"
  "Int.Neg num.One OR Int.Pos m = Int.Neg num.One"
  "Int.Neg (num.Bit0 n) OR Int.Pos m = (case bitANDN_num (Num.BitM n) m of None  -1 | Some n'  Int.Neg (Num.inc n'))"
  "Int.Neg (num.Bit1 n) OR Int.Pos m = (case bitANDN_num (num.Bit0 n) m of None  -1 | Some n'  Int.Neg (Num.inc n'))"
           apply (simp_all add: int_numeral_bitOR_num flip: int_not_neg_numeral)
     apply (simp_all add: or_int_def int_and_comm int_not_and_bitANDN_num del: int_not_simps(4) split: option.split)
     apply (simp_all add: Num.add_One)
  done

lemma int_xor_code [code]: fixes i j :: int shows
  "0 XOR j = j"
  "i XOR 0 = i"
  "Int.Pos n XOR Int.Pos m = (case bitXOR_num n m of None  0 | Some n'  Int.Pos n')"
  "Int.Neg n XOR Int.Neg m = Num.sub n num.One XOR Num.sub m num.One"
  "Int.Neg n XOR Int.Pos m = NOT (Num.sub n num.One XOR Int.Pos m)"
  "Int.Pos n XOR Int.Neg m = NOT (Int.Pos n XOR Num.sub m num.One)"
  by(fold int_not_neg_numeral)(simp_all add: int_numeral_bitXOR_num int_xor_not cong: option.case_cong)

lemma bin_rest_code: "bin_rest i = i >> 1"
  by (simp add: shiftr_int_def)

lemma set_bits_code [code]: 
  "set_bits = Code.abort (STR ''set_bits is unsupported on type int'') (λ_. set_bits :: _  int)"
by simp

lemma fixes i :: int 
  shows int_set_bit_True_conv_OR [code]: "set_bit i n True = i OR (1 << n)"
  and int_set_bit_False_conv_NAND [code]: "set_bit i n False = i AND NOT (1 << n)"
  and int_set_bit_conv_ops: "set_bit i n b = (if b then i OR (1 << n) else i AND NOT (1 << n))"
by(simp_all add: set_bit_int_def bin_set_conv_OR bin_clr_conv_NAND)

declare [[code drop: ‹drop_bit :: nat  int  int›]]

lemma drop_bit_int_code [code]: fixes i :: int shows
  "drop_bit 0 i = i"
  "drop_bit (Suc n) 0 = (0 :: int)"
  "drop_bit (Suc n) (Int.Pos num.One) = 0"
  "drop_bit (Suc n) (Int.Pos (num.Bit0 m)) = drop_bit n (Int.Pos m)"
  "drop_bit (Suc n) (Int.Pos (num.Bit1 m)) = drop_bit n (Int.Pos m)"
  "drop_bit (Suc n) (Int.Neg num.One) = - 1"
  "drop_bit (Suc n) (Int.Neg (num.Bit0 m)) = drop_bit n (Int.Neg m)"
  "drop_bit (Suc n) (Int.Neg (num.Bit1 m)) = drop_bit n (Int.Neg (Num.inc m))"
  by (simp_all add: shiftr_eq_drop_bit drop_bit_Suc add_One)

declare [[code drop: ‹push_bit :: nat  int  int›]]

lemma push_bit_int_code [code]:
  "push_bit 0 i = i"
  "push_bit (Suc n) i = push_bit n (Int.dup i)"
  by (simp_all add: ac_simps)

lemma int_lsb_code [code]:
  "lsb (0 :: int) = False"
  "lsb (Int.Pos num.One) = True"
  "lsb (Int.Pos (num.Bit0 w)) = False"
  "lsb (Int.Pos (num.Bit1 w)) = True"
  "lsb (Int.Neg num.One) = True"
  "lsb (Int.Neg (num.Bit0 w)) = False"
  "lsb (Int.Neg (num.Bit1 w)) = True"
  by simp_all

end

Theory Bits_Integer

(*  Title:      Bits_Integer.thy
    Author:     Andreas Lochbihler, ETH Zurich
*)

chapter ‹Bit operations for target language integers›

theory Bits_Integer imports
  More_Bits_Int
  Code_Symbolic_Bits_Int
begin

lemmas [transfer_rule] =
  identity_quotient
  fun_quotient
  Quotient_integer[folded integer.pcr_cr_eq]

lemma undefined_transfer:
  assumes "Quotient R Abs Rep T"
  shows "T (Rep undefined) undefined"
using assms unfolding Quotient_alt_def by blast

bundle undefined_transfer = undefined_transfer[transfer_rule]

section ‹More lemmas about @{typ integer}s›

context
includes integer.lifting
begin

lemma bitval_integer_transfer [transfer_rule]:
  "(rel_fun (=) pcr_integer) of_bool of_bool"
by(auto simp add: of_bool_def integer.pcr_cr_eq cr_integer_def)

lemma integer_of_nat_less_0_conv [simp]: "¬ integer_of_nat n < 0"
by(transfer) simp

lemma int_of_integer_pow: "int_of_integer (x ^ n) = int_of_integer x ^ n"
by(induct n) simp_all

lemma pow_integer_transfer [transfer_rule]:
  "(rel_fun pcr_integer (rel_fun (=) pcr_integer)) (^) (^)"
by(auto 4 3 simp add: integer.pcr_cr_eq cr_integer_def int_of_integer_pow)

lemma sub1_lt_0_iff [simp]: "Code_Numeral.sub n num.One < 0  False"
by(cases n)(simp_all add: Code_Numeral.sub_code)

lemma nat_of_integer_numeral [simp]: "nat_of_integer (numeral n) = numeral n"
by transfer simp

lemma nat_of_integer_sub1_conv_pred_numeral [simp]:
  "nat_of_integer (Code_Numeral.sub n num.One) = pred_numeral n"
by(cases n)(simp_all add: Code_Numeral.sub_code)

lemma nat_of_integer_1 [simp]: "nat_of_integer 1 = 1"
by transfer simp

lemma dup_1 [simp]: "Code_Numeral.dup 1 = 2"
by transfer simp


section ‹Bit operations on @{typ integer}

text ‹Bit operations on @{typ integer} are the same as on @{typ int}

lift_definition bin_rest_integer :: "integer  integer" is bin_rest .
lift_definition bin_last_integer :: "integer  bool" is bin_last .
lift_definition Bit_integer :: "integer  bool  integer" is λk b. of_bool b + 2 * k .

end

instance integer :: semiring_bit_syntax ..

context
  includes lifting_syntax integer.lifting
begin

lemma test_bit_integer_transfer [transfer_rule]:
  (pcr_integer ===> (=)) bit (!!)
  unfolding test_bit_eq_bit by transfer_prover

lemma shiftl_integer_transfer [transfer_rule]:
  (pcr_integer ===> (=) ===> pcr_integer) (λk n. push_bit n k) (<<)
  unfolding shiftl_eq_push_bit by transfer_prover

lemma shiftr_integer_transfer [transfer_rule]:
  (pcr_integer ===> (=) ===> pcr_integer) (λk n. drop_bit n k) (>>)
  unfolding shiftr_eq_drop_bit by transfer_prover

end

instantiation integer :: lsb begin
context includes integer.lifting begin

lift_definition lsb_integer :: "integer  bool" is lsb .

instance
  by (standard; transfer) (fact lsb_odd)

end
end

instantiation integer :: msb begin
context includes integer.lifting begin

lift_definition msb_integer :: "integer  bool" is msb .

instance ..

end
end

instantiation integer :: set_bit begin
context includes integer.lifting begin

lift_definition set_bit_integer :: "integer  nat  bool  integer" is set_bit .

instance
  apply standard
  apply transfer
  apply (simp add: bit_simps)
  done

end
end

abbreviation (input) wf_set_bits_integer
where "wf_set_bits_integer  wf_set_bits_int"


section ‹Target language implementations›

text ‹
  Unfortunately, this is not straightforward,
  because these API functions have different signatures and preconditions on the parameters:

  \begin{description}
  \item[Standard ML] Shifts in IntInf are given as word, but not IntInf.
  \item[Haskell] In the Data.Bits.Bits type class, shifts and bit indices are given as Int rather than Integer.
  \end{description}

  Additional constants take only parameters of type @{typ integer} rather than @{typ nat}
  and check the preconditions as far as possible (e.g., being non-negative) in a portable way.
  Manual implementations inside code\_printing perform the remaining range checks and convert
  these @{typ integer}s into the right type.

  For normalisation by evaluation, we derive custom code equations, because NBE
  does not know these code\_printing serialisations and would otherwise loop.
›

code_identifier code_module Bits_Integer 
  (SML) Bits_Int and (OCaml) Bits_Int and (Haskell) Bits_Int and (Scala) Bits_Int

code_printing code_module Bits_Integer  (SML)
‹structure Bits_Integer : sig
  val set_bit : IntInf.int -> IntInf.int -> bool -> IntInf.int
  val shiftl : IntInf.int -> IntInf.int -> IntInf.int
  val shiftr : IntInf.int -> IntInf.int -> IntInf.int
  val test_bit : IntInf.int -> IntInf.int -> bool
end = struct

val maxWord = IntInf.pow (2, Word.wordSize);

fun set_bit x n b =
  if n < maxWord then
    if b then IntInf.orb (x, IntInf.<< (1, Word.fromLargeInt (IntInf.toLarge n)))
    else IntInf.andb (x, IntInf.notb (IntInf.<< (1, Word.fromLargeInt (IntInf.toLarge n))))
  else raise (Fail ("Bit index too large: " ^ IntInf.toString n));

fun shiftl x n =
  if n < maxWord then IntInf.<< (x, Word.fromLargeInt (IntInf.toLarge n))
  else raise (Fail ("Shift operand too large: " ^ IntInf.toString n));

fun shiftr x n =
  if n < maxWord then IntInf.~>> (x, Word.fromLargeInt (IntInf.toLarge n))
  else raise (Fail ("Shift operand too large: " ^ IntInf.toString n));

fun test_bit x n =
  if n < maxWord then IntInf.andb (x, IntInf.<< (1, Word.fromLargeInt (IntInf.toLarge n))) <> 0
  else raise (Fail ("Bit index too large: " ^ IntInf.toString n));

end; (*struct Bits_Integer*)›
code_reserved SML Bits_Integer

code_printing code_module Bits_Integer  (OCaml)
‹module Bits_Integer : sig
  val shiftl : Z.t -> Z.t -> Z.t
  val shiftr : Z.t -> Z.t -> Z.t
  val test_bit : Z.t -> Z.t -> bool
end = struct

(* We do not need an explicit range checks here,
   because Big_int.int_of_big_int raises Failure
   if the argument does not fit into an int. *)
let shiftl x n = Z.shift_left x (Z.to_int n);;

let shiftr x n = Z.shift_right x (Z.to_int n);;

let test_bit x n =  Z.testbit x (Z.to_int n);;

end;; (*struct Bits_Integer*)›
code_reserved OCaml Bits_Integer

code_printing code_module Data_Bits  (Haskell)
‹
module Data_Bits where {

import qualified Data.Bits;

{-
  The ...Bounded functions assume that the Integer argument for the shift
  or bit index fits into an Int, is non-negative and (for types of fixed bit width)
  less than bitSize
-}

infixl 7 .&.;
infixl 6 `xor`;
infixl 5 .|.;

(.&.) :: Data.Bits.Bits a => a -> a -> a;
(.&.) = (Data.Bits..&.);

xor :: Data.Bits.Bits a => a -> a -> a;
xor = Data.Bits.xor;

(.|.) :: Data.Bits.Bits a => a -> a -> a;
(.|.) = (Data.Bits..|.);

complement :: Data.Bits.Bits a => a -> a;
complement = Data.Bits.complement;

testBitUnbounded :: Data.Bits.Bits a => a -> Integer -> Bool;
testBitUnbounded x b
  | b <= toInteger (Prelude.maxBound :: Int) = Data.Bits.testBit x (fromInteger b)
  | otherwise = error ("Bit index too large: " ++ show b)
;

testBitBounded :: Data.Bits.Bits a => a -> Integer -> Bool;
testBitBounded x b = Data.Bits.testBit x (fromInteger b);

setBitUnbounded :: Data.Bits.Bits a => a -> Integer -> Bool -> a;
setBitUnbounded x n b
  | n <= toInteger (Prelude.maxBound :: Int) =
    if b then Data.Bits.setBit x (fromInteger n) else Data.Bits.clearBit x (fromInteger n)
  | otherwise = error ("Bit index too large: " ++ show n)
;

setBitBounded :: Data.Bits.Bits a => a -> Integer -> Bool -> a;
setBitBounded x n True = Data.Bits.setBit x (fromInteger n);
setBitBounded x n False = Data.Bits.clearBit x (fromInteger n);

shiftlUnbounded :: Data.Bits.Bits a => a -> Integer -> a;
shiftlUnbounded x n
  | n <= toInteger (Prelude.maxBound :: Int) = Data.Bits.shiftL x (fromInteger n)
  | otherwise = error ("Shift operand too large: " ++ show n)
;

shiftlBounded :: Data.Bits.Bits a => a -> Integer -> a;
shiftlBounded x n = Data.Bits.shiftL x (fromInteger n);

shiftrUnbounded :: Data.Bits.Bits a => a -> Integer -> a;
shiftrUnbounded x n
  | n <= toInteger (Prelude.maxBound :: Int) = Data.Bits.shiftR x (fromInteger n)
  | otherwise = error ("Shift operand too large: " ++ show n)
;

shiftrBounded :: (Ord a, Data.Bits.Bits a) => a -> Integer -> a;
shiftrBounded x n = Data.Bits.shiftR x (fromInteger n);

}›

  and ― ‹@{theory HOL.Quickcheck_Narrowing} maps @{typ integer} to
            Haskell's Prelude.Int type instead of Integer. For compatibility
            with the Haskell target, we nevertheless provide bounded and
            unbounded functions.›
  (Haskell_Quickcheck)
‹
module Data_Bits where {

import qualified Data.Bits;

{-
  The functions assume that the Int argument for the shift or bit index is
  non-negative and (for types of fixed bit width) less than bitSize
-}

infixl 7 .&.;
infixl 6 `xor`;
infixl 5 .|.;

(.&.) :: Data.Bits.Bits a => a -> a -> a;
(.&.) = (Data.Bits..&.);

xor :: Data.Bits.Bits a => a -> a -> a;
xor = Data.Bits.xor;

(.|.) :: Data.Bits.Bits a => a -> a -> a;
(.|.) = (Data.Bits..|.);

complement :: Data.Bits.Bits a => a -> a;
complement = Data.Bits.complement;

testBitUnbounded :: Data.Bits.Bits a => a -> Prelude.Int -> Bool;
testBitUnbounded = Data.Bits.testBit;

testBitBounded :: Data.Bits.Bits a => a -> Prelude.Int -> Bool;
testBitBounded = Data.Bits.testBit;

setBitUnbounded :: Data.Bits.Bits a => a -> Prelude.Int -> Bool -> a;
setBitUnbounded x n True = Data.Bits.setBit x n;
setBitUnbounded x n False = Data.Bits.clearBit x n;

setBitBounded :: Data.Bits.Bits a => a -> Prelude.Int -> Bool -> a;
setBitBounded x n True = Data.Bits.setBit x n;
setBitBounded x n False = Data.Bits.clearBit x n;

shiftlUnbounded :: Data.Bits.Bits a => a -> Prelude.Int -> a;
shiftlUnbounded = Data.Bits.shiftL;

shiftlBounded :: Data.Bits.Bits a => a -> Prelude.Int -> a;
shiftlBounded = Data.Bits.shiftL;

shiftrUnbounded :: Data.Bits.Bits a => a -> Prelude.Int -> a;
shiftrUnbounded = Data.Bits.shiftR;

shiftrBounded :: (Ord a, Data.Bits.Bits a) => a -> Prelude.Int -> a;
shiftrBounded = Data.Bits.shiftR;

}›
code_reserved Haskell Data_Bits

code_printing code_module Bits_Integer  (Scala)
‹object Bits_Integer {

def setBit(x: BigInt, n: BigInt, b: Boolean) : BigInt =
  if (n.isValidInt)
    if (b)
      x.setBit(n.toInt)
    else
      x.clearBit(n.toInt)
  else
    sys.error("Bit index too large: " + n.toString)

def shiftl(x: BigInt, n: BigInt) : BigInt =
  if (n.isValidInt)
    x << n.toInt
  else
    sys.error("Shift index too large: " + n.toString)

def shiftr(x: BigInt, n: BigInt) : BigInt =
  if (n.isValidInt)
    x << n.toInt
  else
    sys.error("Shift index too large: " + n.toString)

def testBit(x: BigInt, n: BigInt) : Boolean =
  if (n.isValidInt)
    x.testBit(n.toInt)
  else
    sys.error("Bit index too large: " + n.toString)

} /* object Bits_Integer */›

code_printing
  constant "(AND) :: integer  integer  integer" 
  (SML) "IntInf.andb ((_),/ (_))" and
  (OCaml) "Z.logand" and
  (Haskell) "((Data'_Bits..&.) :: Integer -> Integer -> Integer)" and
  (Haskell_Quickcheck) "((Data'_Bits..&.) :: Prelude.Int -> Prelude.Int -> Prelude.Int)" and
  (Scala) infixl 3 "&"
| constant "(OR) :: integer  integer  integer" 
  (SML) "IntInf.orb ((_),/ (_))" and
  (OCaml) "Z.logor" and
  (Haskell) "((Data'_Bits..|.) :: Integer -> Integer -> Integer)" and
  (Haskell_Quickcheck) "((Data'_Bits..|.) :: Prelude.Int -> Prelude.Int -> Prelude.Int)" and
  (Scala) infixl 1 "|"
| constant "(XOR) :: integer  integer  integer" 
  (SML) "IntInf.xorb ((_),/ (_))" and
  (OCaml) "Z.logxor" and
  (Haskell) "(Data'_Bits.xor :: Integer -> Integer -> Integer)" and
  (Haskell_Quickcheck) "(Data'_Bits.xor :: Prelude.Int -> Prelude.Int -> Prelude.Int)" and
  (Scala) infixl 2 "^"
| constant "NOT :: integer  integer" 
  (SML) "IntInf.notb" and
  (OCaml) "Z.lognot" and
  (Haskell) "(Data'_Bits.complement :: Integer -> Integer)" and
  (Haskell_Quickcheck) "(Data'_Bits.complement :: Prelude.Int -> Prelude.Int)" and
  (Scala) "_.unary'_~"

code_printing constant bin_rest_integer 
  (SML) "IntInf.div ((_), 2)" and
  (OCaml) "Z.shift'_right/ _/ 1" and
  (Haskell) "(Data'_Bits.shiftrUnbounded _ 1 :: Integer)" and
  (Haskell_Quickcheck) "(Data'_Bits.shiftrUnbounded _ 1 :: Prelude.Int)" and
  (Scala) "_ >> 1"

context
includes integer.lifting
begin

lemma bitNOT_integer_code [code]:
  fixes i :: integer shows
  "NOT i = - i - 1"
by transfer(simp add: int_not_def)

lemma bin_rest_integer_code [code nbe]:
  "bin_rest_integer i = i div 2"
  by transfer rule

lemma bin_last_integer_code [code]:
  "bin_last_integer i  i AND 1  0"
  by transfer (rule bin_last_conv_AND)

lemma bin_last_integer_nbe [code nbe]:
  "bin_last_integer i  i mod 2  0"
by transfer(simp add: bin_last_def)

lemma bitval_bin_last_integer [code_unfold]:
  "of_bool (bin_last_integer i) = i AND 1"
by transfer(rule bitval_bin_last)

end

definition integer_test_bit :: "integer  integer  bool"
  where "integer_test_bit x n = (if n < 0 then undefined x n else bit x (nat_of_integer n))"

declare [[code drop: ‹bit :: integer  nat  bool›]]

lemma bit_integer_code [code]:
  "bit x n  integer_test_bit x (integer_of_nat n)"
  by (simp add: integer_test_bit_def)

lemma integer_test_bit_code [code]:
  "integer_test_bit x (Code_Numeral.Neg n) = undefined x (Code_Numeral.Neg n)"
  "integer_test_bit 0 0 = False"
  "integer_test_bit 0 (Code_Numeral.Pos n) = False"
  "integer_test_bit (Code_Numeral.Pos num.One)      0 = True"
  "integer_test_bit (Code_Numeral.Pos (num.Bit0 n)) 0 = False"
  "integer_test_bit (Code_Numeral.Pos (num.Bit1 n)) 0 = True"
  "integer_test_bit (Code_Numeral.Pos num.One)      (Code_Numeral.Pos n') = False"
  "integer_test_bit (Code_Numeral.Pos (num.Bit0 n)) (Code_Numeral.Pos n') =
   integer_test_bit (Code_Numeral.Pos n) (Code_Numeral.sub n' num.One)"
  "integer_test_bit (Code_Numeral.Pos (num.Bit1 n)) (Code_Numeral.Pos n') =
   integer_test_bit (Code_Numeral.Pos n) (Code_Numeral.sub n' num.One)"
  "integer_test_bit (Code_Numeral.Neg num.One)      0 = True"
  "integer_test_bit (Code_Numeral.Neg (num.Bit0 n)) 0 = False"
  "integer_test_bit (Code_Numeral.Neg (num.Bit1 n)) 0 = True"
  "integer_test_bit (Code_Numeral.Neg num.One)      (Code_Numeral.Pos n') = True"
  "integer_test_bit (Code_Numeral.Neg (num.Bit0 n)) (Code_Numeral.Pos n') =
   integer_test_bit (Code_Numeral.Neg n) (Code_Numeral.sub n' num.One)"
  "integer_test_bit (Code_Numeral.Neg (num.Bit1 n)) (Code_Numeral.Pos n') =
   integer_test_bit (Code_Numeral.Neg (n + num.One)) (Code_Numeral.sub n' num.One)"
                apply (simp_all add: integer_test_bit_def bit_integer_def)
  using bin_nth_numeral_simps bit_numeral_int_simps(6)
  by presburger

code_printing constant integer_test_bit 
  (SML) "Bits'_Integer.test'_bit" and
  (OCaml) "Bits'_Integer.test'_bit" and
  (Haskell) "(Data'_Bits.testBitUnbounded :: Integer -> Integer -> Bool)" and
  (Haskell_Quickcheck) "(Data'_Bits.testBitUnbounded :: Prelude.Int -> Prelude.Int -> Bool)" and
  (Scala) "Bits'_Integer.testBit"

context
includes integer.lifting
begin

lemma lsb_integer_code [code]:
  fixes x :: integer shows
  "lsb x = bit x 0"
by transfer(simp add: lsb_int_def)

definition integer_set_bit :: "integer  integer  bool  integer"
where [code del]: "integer_set_bit x n b = (if n < 0 then undefined x n b else set_bit x (nat_of_integer n) b)"

lemma set_bit_integer_code [code]:
  "set_bit x i b = integer_set_bit x (integer_of_nat i) b"
by(simp add: integer_set_bit_def)

lemma set_bit_integer_conv_masks:
  fixes x :: integer shows
  "set_bit x i b = (if b then x OR (1 << i) else x AND NOT (1 << i))"
  by transfer (simp add: int_set_bit_False_conv_NAND int_set_bit_True_conv_OR shiftl_eq_push_bit)

end

code_printing constant integer_set_bit 
  (SML) "Bits'_Integer.set'_bit" and
  (Haskell) "(Data'_Bits.setBitUnbounded :: Integer -> Integer -> Bool -> Integer)" and
  (Haskell_Quickcheck) "(Data'_Bits.setBitUnbounded :: Prelude.Int -> Prelude.Int -> Bool -> Prelude.Int)" and
  (Scala) "Bits'_Integer.setBit"

text ‹
  OCaml.Big\_int does not have a method for changing an individual bit, so we emulate that with masks.
  We prefer an Isabelle implementation, because this then takes care of the signs for AND and OR.
›
lemma integer_set_bit_code [code]:
  "integer_set_bit x n b =
  (if n < 0 then undefined x n b else
   if b then x OR (push_bit (nat_of_integer n) 1)
   else x AND NOT (push_bit (nat_of_integer n) 1))"
  by (auto simp add: integer_set_bit_def not_less set_bit_eq set_bit_def unset_bit_def)

definition integer_shiftl :: "integer  integer  integer"
where [code del]: "integer_shiftl x n = (if n < 0 then undefined x n else push_bit (nat_of_integer n) x)"

declare [[code drop: ‹push_bit :: nat  integer  integer›]]

lemma shiftl_integer_code [code]:
  fixes x :: integer shows
  "push_bit n x = integer_shiftl x (integer_of_nat n)"
by(auto simp add: integer_shiftl_def)

context
includes integer.lifting
begin

lemma shiftl_integer_conv_mult_pow2:
  fixes x :: integer shows
  "x << n = x * 2 ^ n"
  by (simp add: push_bit_eq_mult shiftl_eq_push_bit)

lemma integer_shiftl_code [code]:
  "integer_shiftl x (Code_Numeral.Neg n) = undefined x (Code_Numeral.Neg n)"
  "integer_shiftl x 0 = x"
  "integer_shiftl x (Code_Numeral.Pos n) = integer_shiftl (Code_Numeral.dup x) (Code_Numeral.sub n num.One)"
  "integer_shiftl 0 (Code_Numeral.Pos n) = 0"
     apply (simp_all add: integer_shiftl_def numeral_eq_Suc)
  apply transfer
  apply (simp add: ac_simps)
  done

end

code_printing constant integer_shiftl 
  (SML) "Bits'_Integer.shiftl" and
  (OCaml) "Bits'_Integer.shiftl" and
  (Haskell) "(Data'_Bits.shiftlUnbounded :: Integer -> Integer -> Integer)" and
  (Haskell_Quickcheck) "(Data'_Bits.shiftlUnbounded :: Prelude.Int -> Prelude.Int -> Prelude.Int)" and
  (Scala) "Bits'_Integer.shiftl"

definition integer_shiftr :: "integer  integer  integer"
where [code del]: "integer_shiftr x n = (if n < 0 then undefined x n else drop_bit (nat_of_integer n) x)"

declare [[code drop: ‹drop_bit :: nat  integer  integer›]]

lemma shiftr_integer_conv_div_pow2:
  includes integer.lifting fixes x :: integer shows
  "x >> n = x div 2 ^ n"
  by (simp add: drop_bit_eq_div shiftr_eq_drop_bit)

lemma shiftr_integer_code [code]:
  fixes x :: integer shows
  "drop_bit n x = integer_shiftr x (integer_of_nat n)"
by(auto simp add: integer_shiftr_def)

code_printing constant integer_shiftr 
  (SML) "Bits'_Integer.shiftr" and
  (OCaml) "Bits'_Integer.shiftr" and
  (Haskell) "(Data'_Bits.shiftrUnbounded :: Integer -> Integer -> Integer)" and
  (Haskell_Quickcheck) "(Data'_Bits.shiftrUnbounded :: Prelude.Int -> Prelude.Int -> Prelude.Int)" and
  (Scala) "Bits'_Integer.shiftr"

lemma integer_shiftr_code [code]:
  includes integer.lifting
  shows
  "integer_shiftr x (Code_Numeral.Neg n) = undefined x (Code_Numeral.Neg n)"
  "integer_shiftr x 0 = x"
  "integer_shiftr 0 (Code_Numeral.Pos n) = 0"
  "integer_shiftr (Code_Numeral.Pos num.One) (Code_Numeral.Pos n) = 0"
  "integer_shiftr (Code_Numeral.Pos (num.Bit0 n')) (Code_Numeral.Pos n) =
   integer_shiftr (Code_Numeral.Pos n') (Code_Numeral.sub n num.One)"
  "integer_shiftr (Code_Numeral.Pos (num.Bit1 n')) (Code_Numeral.Pos n) =
   integer_shiftr (Code_Numeral.Pos n') (Code_Numeral.sub n num.One)"
  "integer_shiftr (Code_Numeral.Neg num.One) (Code_Numeral.Pos n) = -1"
  "integer_shiftr (Code_Numeral.Neg (num.Bit0 n')) (Code_Numeral.Pos n) =
   integer_shiftr (Code_Numeral.Neg n') (Code_Numeral.sub n num.One)"
  "integer_shiftr (Code_Numeral.Neg (num.Bit1 n')) (Code_Numeral.Pos n) =
   integer_shiftr (Code_Numeral.Neg (Num.inc n')) (Code_Numeral.sub n num.One)"
          apply (simp_all add: integer_shiftr_def numeral_eq_Suc drop_bit_Suc)
    apply transfer apply simp
   apply transfer apply simp
  apply transfer apply (simp add: add_One)
  done

context
includes integer.lifting
begin

lemma Bit_integer_code [code]:
  "Bit_integer i False = push_bit 1 i"
  "Bit_integer i True = (push_bit 1 i) + 1"
  by (transfer; simp add: shiftl_int_def)+

lemma msb_integer_code [code]:
  "msb (x :: integer)  x < 0"
by transfer(simp add: msb_int_def)

end

context
includes integer.lifting natural.lifting
begin

lemma bitAND_integer_unfold [code]:
  "x AND y =
   (if x = 0 then 0
    else if x = - 1 then y
    else Bit_integer (bin_rest_integer x AND bin_rest_integer y) (bin_last_integer x  bin_last_integer y))"
  by transfer
    (auto simp add: algebra_simps
      and_int_rec [of _ _ * 2] and_int_rec [of _ * 2] and_int_rec [of 1 + _ * 2]
      elim!: evenE oddE)

lemma bitOR_integer_unfold [code]:
  "x OR y =
   (if x = 0 then y
    else if x = - 1 then - 1
    else Bit_integer (bin_rest_integer x OR bin_rest_integer y) (bin_last_integer x  bin_last_integer y))"
  by transfer
    (auto simp add: algebra_simps
      or_int_rec [of _ _ * 2] or_int_rec [of _ 1 + _ * 2] or_int_rec [of 1 + _ * 2]
      elim!: evenE oddE)

lemma bitXOR_integer_unfold [code]:
  "x XOR y =
   (if x = 0 then y
    else if x = - 1 then NOT y
    else Bit_integer (bin_rest_integer x XOR bin_rest_integer y)
      (¬ bin_last_integer x  bin_last_integer y))"
  by transfer
    (auto simp add: algebra_simps
      xor_int_rec [of _ _ * 2] xor_int_rec [of _ * 2] xor_int_rec [of 1 + _ * 2]
      elim!: evenE oddE)

end


section ‹Test code generator setup›

definition bit_integer_test :: "bool" where
  "bit_integer_test =
  (([ -1 AND 3, 1 AND -3, 3 AND 5, -3 AND (- 5)
    , -3 OR 1, 1 OR -3, 3 OR 5, -3 OR (- 5)
    , NOT 1, NOT (- 3)
    , -1 XOR 3, 1 XOR (- 3), 3 XOR 5, -5 XOR (- 3)
    , set_bit 5 4 True, set_bit (- 5) 2 True, set_bit 5 0 False, set_bit (- 5) 1 False
    , 1 << 2, -1 << 3
    , 100 >> 3, -100 >> 3] :: integer list)
  = [ 3, 1, 1, -7
    , -3, -3, 7, -1
    , -2, 2
    , -4, -4, 6, 6
    , 21, -1, 4, -7
    , 4, -8
    , 12, -13] 
    [ (5 :: integer) !! 4, (5 :: integer) !! 2, (-5 :: integer) !! 4, (-5 :: integer) !! 2
    , lsb (5 :: integer), lsb (4 :: integer), lsb (-1 :: integer), lsb (-2 :: integer),
      msb (5 :: integer), msb (0 :: integer), msb (-1 :: integer), msb (-2 :: integer)]
  = [ False, True, True, False,
      True, False, True, False,
      False, False, True, True])"

export_code bit_integer_test checking SML Haskell? Haskell_Quickcheck? OCaml? Scala

notepad begin
have bit_integer_test by eval
have bit_integer_test by normalization
have bit_integer_test by code_simp
end
ML_val val true = @{code bit_integer_test}

lemma "x AND y = x OR (y :: integer)"
quickcheck[random, expect=counterexample]
quickcheck[exhaustive, expect=counterexample]
oops

lemma "(x :: integer) AND x = x OR x"
quickcheck[narrowing, expect=no_counterexample]
oops

lemma "(f :: integer  unit) = g"
quickcheck[narrowing, size=3, expect=no_counterexample]
by(simp add: fun_eq_iff)

hide_const bit_integer_test
hide_fact bit_integer_test_def

end

Theory Code_Target_Bits_Int

(*  Title:      Code_Target_Bits_Int.thy
    Author:     Andreas Lochbihler, ETH Zurich
*)

chapter ‹Implementation of bit operations on int by target language operations›

theory Code_Target_Bits_Int
imports
  Bits_Integer
  "HOL-Library.Code_Target_Int"
begin

declare [[code drop:
  "(AND) :: int  _" "(OR) :: int  _" "(XOR) :: int  _" "(NOT) :: int  _"
  "lsb :: int  _" "set_bit :: int  _" "bit :: int  _"
  "push_bit :: _  int  _" "drop_bit :: _  int  _"
  int_of_integer_symbolic
  ]]

declare bitval_bin_last [code_unfold]

lemma [code_unfold]:
  ‹bit x n  x AND (push_bit n 1)  0 for x :: int
  by (fact bit_iff_and_push_bit_not_eq_0)

context
includes integer.lifting
begin

lemma bit_int_code [code]:
  "bit (int_of_integer x) n = bit x n"
  by transfer simp

lemma and_int_code [code]:
  "int_of_integer i AND int_of_integer j = int_of_integer (i AND j)"
  by transfer simp

lemma or_int_code [code]:
  "int_of_integer i OR int_of_integer j = int_of_integer (i OR j)"
  by transfer simp

lemma xor_int_code [code]:
  "int_of_integer i XOR int_of_integer j = int_of_integer (i XOR j)"
  by transfer simp

lemma not_int_code [code]:
  "NOT (int_of_integer i) = int_of_integer (NOT i)"
  by transfer simp

lemma push_bit_int_code [code]:
  ‹push_bit n (int_of_integer x) = int_of_integer (push_bit n x)
  by transfer simp

lemma drop_bit_int_code [code]:
  ‹drop_bit n (int_of_integer x) = int_of_integer (drop_bit n x)
  by transfer simp

lemma take_bit_int_code [code]:
  ‹take_bit n (int_of_integer x) = int_of_integer (take_bit n x)
  by transfer simp

lemma lsb_int_code [code]:
  "lsb (int_of_integer x) = lsb x"
  by transfer simp

lemma set_bit_int_code [code]:
  "set_bit (int_of_integer x) n b = int_of_integer (set_bit x n b)"
  by transfer simp

lemma int_of_integer_symbolic_code [code]:
  "int_of_integer_symbolic = int_of_integer"
  by (simp add: int_of_integer_symbolic_def)

context
begin

qualified definition even :: ‹int  bool›
  where [code_abbrev]: even = Parity.even›

end

lemma [code]:
  ‹Code_Target_Bits_Int.even i  i AND 1 = 0
  by (simp add: Code_Target_Bits_Int.even_def even_iff_mod_2_eq_zero and_one_eq)

lemma bin_rest_code:
  "bin_rest (int_of_integer i) = int_of_integer (bin_rest_integer i)"
  by transfer simp

end

end

Theory Code_Target_Word_Base

(*  Title:      Code_Target_Word_Base.thy
    Author:     Andreas Lochbihler, ETH Zurich
*)

chapter ‹Common base for target language implementations of word types›

theory Code_Target_Word_Base imports
  "HOL-Library.Word"
  "Word_Lib.Signed_Division_Word"
  Bits_Integer
begin

text ‹More lemmas›

lemma div_half_nat:
  fixes x y :: nat
  assumes "y  0"
  shows "(x div y, x mod y) = (let q = 2 * (x div 2 div y); r = x - q * y in if y  r then (q + 1, r - y) else (q, r))"
proof -
  let ?q = "2 * (x div 2 div y)"
  have q: "?q = x div y - x div y mod 2"
    by(metis div_mult2_eq mult.commute minus_mod_eq_mult_div [symmetric])
  let ?r = "x - ?q * y"
  have r: "?r = x mod y + x div y mod 2 * y"
    by(simp add: q diff_mult_distrib minus_mod_eq_div_mult [symmetric])(metis diff_diff_cancel mod_less_eq_dividend mod_mult2_eq add.commute mult.commute)

  show ?thesis
  proof(cases "y  x - ?q * y")
    case True
    with assms q have "x div y mod 2  0" unfolding r
      by (metis Nat.add_0_right diff_0_eq_0 diff_Suc_1 le_div_geq mod2_gr_0 mod_div_trivial mult_0 neq0_conv numeral_1_eq_Suc_0 numerals(1)) 
    hence "x div y = ?q + 1" unfolding q
      by simp
    moreover hence "x mod y = ?r - y"
      by simp(metis minus_div_mult_eq_mod [symmetric] diff_commute diff_diff_left mult_Suc)
    ultimately show ?thesis using True by(simp add: Let_def)
  next
    case False
    hence "x div y mod 2 = 0" unfolding r
      by(simp add: not_le)(metis Nat.add_0_right assms div_less div_mult_self2 mod_div_trivial mult.commute)
    hence "x div y = ?q" unfolding q by simp
    moreover hence "x mod y = ?r" by (metis minus_div_mult_eq_mod [symmetric])
    ultimately show ?thesis using False by(simp add: Let_def)
  qed
qed

lemma div_half_word:
  fixes x y :: "'a :: len word"
  assumes "y  0"
  shows "(x div y, x mod y) = (let q = (x >> 1) div y << 1; r = x - q * y in if y  r then (q + 1, r - y) else (q, r))"
proof -
  obtain n where n: "x = of_nat n" "n < 2 ^ LENGTH('a)"
    by (rule that [of ‹unat x]) simp_all
  moreover obtain m where m: "y = of_nat m" "m < 2 ^ LENGTH('a)"
    by (rule that [of ‹unat y]) simp_all
  ultimately have [simp]: ‹unat (of_nat n :: 'a word) = n ‹unat (of_nat m :: 'a word) = m
    by (transfer, simp add: take_bit_of_nat take_bit_nat_eq_self_iff)+
  let ?q = "(x >> 1) div y << 1"
  let ?q' = "2 * (n div 2 div m)"
  have "n div 2 div m < 2 ^ LENGTH('a)" using n by (metis of_nat_inverse unat_lt2p uno_simps(2))
  hence q: "?q = of_nat ?q'" using n m
    by (auto simp add: shiftr_word_eq drop_bit_eq_div shiftl_t2n word_arith_nat_div uno_simps take_bit_nat_eq_self)
  from assms have "m  0" using m by -(rule notI, simp)

  from n have "2 * (n div 2 div m) < 2 ^ LENGTH('a)"
    by(metis mult.commute div_mult2_eq minus_mod_eq_mult_div [symmetric] less_imp_diff_less of_nat_inverse unat_lt2p uno_simps(2))
  moreover
  have "2 * (n div 2 div m) * m < 2 ^ LENGTH('a)" using n unfolding div_mult2_eq[symmetric]
    by(subst (2) mult.commute)(simp add: minus_mod_eq_div_mult [symmetric] diff_mult_distrib minus_mod_eq_mult_div [symmetric] div_mult2_eq)
  moreover have "2 * (n div 2 div m) * m  n"
    by (simp flip: div_mult2_eq ac_simps)
  ultimately
  have r: "x - ?q * y = of_nat (n - ?q' * m)"
    and "y  x - ?q * y  of_nat (n - ?q' * m) - y = of_nat (n - ?q' * m - m)"
    using n m unfolding q
     apply (simp_all add: of_nat_diff)
    apply (subst of_nat_diff)
    apply (simp_all add: word_le_nat_alt take_bit_nat_eq_self unat_sub_if' unat_word_ariths)
    done
  then show ?thesis using n m div_half_nat [OF m  0, of n] unfolding q
    by (simp add: word_le_nat_alt word_div_def word_mod_def Let_def take_bit_nat_eq_self
      flip: zdiv_int zmod_int
      split del: if_split split: if_split_asm)
qed

lemma word_test_bit_set_bits: "(BITS n. f n :: 'a :: len word) !! n  n < LENGTH('a)  f n"
  by (simp add: test_bit_eq_bit bit_set_bits_word_iff)

lemma word_of_int_conv_set_bits: "word_of_int i = (BITS n. i !! n)"
  by (rule word_eqI) (auto simp add: word_test_bit_set_bits)

lemma word_and_mask_or_conv_and_mask:
  "n !! index  (n AND mask index) OR (1 << index) = n AND mask (index + 1)"
  for n :: 'a::len word›
by(rule word_eqI)(auto simp add: word_ao_nth word_size nth_shiftl simp del: shiftl_1)

lemma uint_and_mask_or_full:
  fixes n :: "'a :: len word"
  assumes "n !! (LENGTH('a) - 1)"
  and "mask1 = mask (LENGTH('a) - 1)"
  and "mask2 = 1 << LENGTH('a) - 1"
  shows "uint (n AND mask1) OR mask2 = uint n"
proof -
  have "mask2 = uint (1 << LENGTH('a) - 1 :: 'a word)" using assms
    by (simp add: uint_shiftl word_size bintrunc_shiftl del: shiftl_1)
  hence "uint (n AND mask1) OR mask2 = uint (n AND mask1 OR (1 << LENGTH('a) - 1 :: 'a word))"
    by(simp add: uint_or)
  also have " = uint (n AND mask (LENGTH('a) - 1 + 1))"
    using assms by(simp only: word_and_mask_or_conv_and_mask)
  also have " = uint n" by simp
  finally show ?thesis .
qed


text ‹Division on @{typ "'a word"} is unsigned, but Scala and OCaml only have signed division and modulus.›

lemmas word_sdiv_def = sdiv_word_def
lemmas word_smod_def = smod_word_def

lemma [code]:
  "x sdiv y =
   (let x' = sint x; y' = sint y;
        negative = (x' < 0)  (y' < 0);
        result = abs x' div abs y'
    in word_of_int (if negative then -result else result))"
  for x y :: 'a::len word›
  by (simp add: sdiv_word_def signed_divide_int_def sgn_if Let_def not_less not_le)

lemma [code]:
  "x smod y =
   (let x' = sint x; y' = sint y;
        negative = (x' < 0);
        result = abs x' mod abs y'
    in word_of_int (if negative then -result else result))"
  for x y :: 'a::len word›
proof -
  have *: k mod l = k - k div l * l for k l :: int
    by (simp add: minus_div_mult_eq_mod)
  show ?thesis
    by (simp add: smod_word_def signed_modulo_int_def signed_divide_int_def * sgn_if Let_def)
qed

text ‹
  This algorithm implements unsigned division in terms of signed division.
  Taken from Hacker's Delight.
›

lemma divmod_via_sdivmod:
  fixes x y :: "'a :: len word"
  assumes "y  0"
  shows
  "(x div y, x mod y) =
  (if 1 << (LENGTH('a) - 1)  y then if x < y then (0, x) else (1, x - y)
   else let q = ((x >> 1) sdiv y) << 1;
            r = x - q * y
        in if r  y then (q + 1, r - y) else (q, r))"
proof(cases "1 << (LENGTH('a) - 1)  y")
  case True
  note y = this
  show ?thesis
  proof(cases "x < y")
    case True
    then have "x mod y = x"
      by transfer simp
    thus ?thesis using True y by(simp add: word_div_lt_eq_0)
  next
    case False
    obtain n where n: "y = of_nat n" "n < 2 ^ LENGTH('a)"
      by (rule that [of ‹unat y]) simp_all
    have "unat x < 2 ^ LENGTH('a)" by(rule unat_lt2p)
    also have " = 2 * 2 ^ (LENGTH('a) - 1)"
      by(metis Suc_pred len_gt_0 power_Suc One_nat_def)
    also have "  2 * n" using y n
      by transfer (simp add: push_bit_of_1 take_bit_eq_mod)
    finally have div: "x div of_nat n = 1" using False n
      by (simp add: word_div_eq_1_iff take_bit_nat_eq_self)
    moreover have "x mod y = x - x div y * y"
      by (simp add: minus_div_mult_eq_mod)
    with div n have "x mod y = x - y" by simp
    ultimately show ?thesis using False y n by simp
  qed
next
  case False
  note y = this
  obtain n where n: "x = of_nat n" "n < 2 ^ LENGTH('a)"
    by (rule that [of ‹unat x]) simp_all
  hence "int n div 2 + 2 ^ (LENGTH('a) - Suc 0) < 2 ^ LENGTH('a)"
    by (cases LENGTH('a))
      (auto dest: less_imp_of_nat_less [where ?'a = int])
  with y n have "sint (x >> 1) = uint (x >> 1)"
    by (simp add: sint_uint sbintrunc_mod2p shiftr_div_2n take_bit_nat_eq_self)
  moreover have "uint y + 2 ^ (LENGTH('a) - Suc 0) < 2 ^ LENGTH('a)"
    using y by (cases "LENGTH('a)")
      (simp_all add: not_le word_2p_lem word_size)
  then have "sint y = uint y"
    by (simp add: sint_uint sbintrunc_mod2p)
  ultimately show ?thesis using y
    apply (subst div_half_word [OF assms])
    apply (simp add: sdiv_word_def signed_divide_int_def flip: uint_div)
    done
qed


text ‹More implementations tailored towards target-language implementations›

context
includes integer.lifting
begin
lift_definition word_of_integer :: "integer  'a :: len word" is word_of_int .

lemma word_of_integer_code [code]: "word_of_integer n = word_of_int (int_of_integer n)"
by(simp add: word_of_integer.rep_eq)
end

lemma word_of_int_code:
  "uint (word_of_int x :: 'a word) = x AND mask (LENGTH('a :: len))"
  by (simp add: take_bit_eq_mask)

context fixes f :: "nat  bool" begin

definition set_bits_aux :: 'a word  nat  'a :: len word›
  where set_bits_aux w n = push_bit n w OR take_bit n (set_bits f)

lemma set_bits_aux_conv:
  ‹set_bits_aux w n = (w << n) OR (set_bits f AND mask n)
  for w :: 'a::len word›
  by (rule bit_word_eqI)
    (auto simp add: set_bits_aux_def shiftl_word_eq bit_and_iff bit_or_iff bit_push_bit_iff bit_take_bit_iff bit_mask_iff bit_set_bits_word_iff)

corollary set_bits_conv_set_bits_aux:
  ‹set_bits f = (set_bits_aux 0 (LENGTH('a)) :: 'a :: len word)
  by (simp add: set_bits_aux_conv)

lemma set_bits_aux_0 [simp]:
  ‹set_bits_aux w 0 = w
  by  (simp add: set_bits_aux_conv)

lemma set_bits_aux_Suc [simp]:
  ‹set_bits_aux w (Suc n) = set_bits_aux ((w << 1) OR (if f n then 1 else 0)) n
  by (simp add: set_bits_aux_def shiftl_word_eq bit_eq_iff bit_or_iff bit_push_bit_iff bit_take_bit_iff bit_set_bits_word_iff)
    (auto simp add: bit_exp_iff not_less bit_1_iff less_Suc_eq_le)

lemma set_bits_aux_simps [code]:
  ‹set_bits_aux w 0 = w
  ‹set_bits_aux w (Suc n) = set_bits_aux ((w << 1) OR (if f n then 1 else 0)) n
  by simp_all

end

lemma word_of_int_via_signed:
  fixes mask
  assumes mask_def: "mask = Bit_Operations.mask (LENGTH('a))"
  and shift_def: "shift = 1 << LENGTH('a)"
  and index_def: "index = LENGTH('a) - 1"
  and overflow_def:"overflow = 1 << (LENGTH('a) - 1)"
  and least_def: "least = - overflow"
  shows
  "(word_of_int i :: 'a :: len word) =
   (let i' = i AND mask
    in if i' !! index then
         if i' - shift < least  overflow  i' - shift then arbitrary1 i' else word_of_int (i' - shift)
       else if i' < least  overflow  i' then arbitrary2 i' else word_of_int i')"
proof -
  define i' where "i' = i AND mask"
  have "shift = mask + 1" unfolding assms by(simp add: bin_mask_p1_conv_shift)
  hence "i' < shift" by(simp add: mask_def i'_def int_and_le)
  show ?thesis
  proof(cases "i' !! index")
    case True
    then have unf: "i' = overflow OR i'"
      apply (simp add: assms i'_def shiftl_eq_push_bit push_bit_of_1 flip: take_bit_eq_mask)
      apply (rule bit_eqI)
      apply (auto simp add: bit_take_bit_iff bit_or_iff bit_exp_iff)
      done
    have "overflow  i'" by(subst unf)(rule le_int_or, simp add: bin_sign_and assms i'_def)
    hence "i' - shift < least  False" unfolding assms
      by(cases "LENGTH('a)")(simp_all add: not_less)
    moreover
    have "overflow  i' - shift  False" using i' < shift unfolding assms
      by(cases "LENGTH('a)")(auto simp add: not_le elim: less_le_trans)
    moreover
    have "word_of_int (i' - shift) = (word_of_int i :: 'a word)" using i' < shift
      by (simp add: i'_def shift_def mask_def shiftl_eq_push_bit push_bit_of_1 word_of_int_eq_iff flip: take_bit_eq_mask)
    ultimately show ?thesis using True by(simp add: Let_def i'_def)
  next
    case False
    hence "i' = i AND Bit_Operations.mask (LENGTH('a) - 1)" unfolding assms i'_def
      by(clarsimp simp add: i'_def bin_nth_ops intro!: bin_eqI)(cases "LENGTH('a)", auto simp add: less_Suc_eq)
    also have "  Bit_Operations.mask (LENGTH('a) - 1)" by(rule int_and_le) simp
    also have " < overflow" unfolding overflow_def
      by(simp add: bin_mask_p1_conv_shift[symmetric])
    also
    have "least  0" unfolding least_def overflow_def by simp
    have "0  i'" by (simp add: i'_def mask_def)
    hence "least  i'" using least  0 by simp
    moreover
    have "word_of_int i' = (word_of_int i :: 'a word)"
      by(rule word_eqI)(auto simp add: i'_def bin_nth_ops mask_def)
    ultimately show ?thesis using False by(simp add: Let_def i'_def)
  qed
qed



text ‹Quickcheck conversion functions›

context
  includes state_combinator_syntax
begin

definition qc_random_cnv ::
  "(natural  'a::term_of)  natural  Random.seed
     ('a × (unit  Code_Evaluation.term)) × Random.seed"
  where "qc_random_cnv a_of_natural i = Random.range (i + 1) ∘→ (λk. Pair (
       let n = a_of_natural k
       in (n, λ_. Code_Evaluation.term_of n)))"

end

definition qc_exhaustive_cnv :: "(natural  'a)  ('a  (bool × term list) option)
   natural  (bool × term list) option"
where
  "qc_exhaustive_cnv a_of_natural f d =
   Quickcheck_Exhaustive.exhaustive (%x. f (a_of_natural x)) d"

definition qc_full_exhaustive_cnv ::
  "(natural  ('a::term_of))  ('a × (unit  term)  (bool × term list) option)
   natural  (bool × term list) option"
where
  "qc_full_exhaustive_cnv a_of_natural f d = Quickcheck_Exhaustive.full_exhaustive
  (%(x, xt). f (a_of_natural x, %_. Code_Evaluation.term_of (a_of_natural x))) d"

declare [[quickcheck_narrowing_ghc_options = "-XTypeSynonymInstances"]]

definition qc_narrowing_drawn_from :: "'a list  integer  _"
where
  "qc_narrowing_drawn_from xs =
   foldr Quickcheck_Narrowing.sum (map Quickcheck_Narrowing.cons (butlast xs)) (Quickcheck_Narrowing.cons (last xs))"

locale quickcheck_narrowing_samples =
  fixes a_of_integer :: "integer  'a × 'a :: {partial_term_of, term_of}"
  and zero :: "'a"
  and tr :: "typerep"
begin

function narrowing_samples :: "integer  'a list"
where
  "narrowing_samples i =
   (if i > 0 then let (a, a') = a_of_integer i in narrowing_samples (i - 1) @ [a, a'] else [zero])"
by pat_completeness auto
termination including integer.lifting
proof(relation "measure nat_of_integer")
  fix i :: integer
  assume "0 < i"
  thus "(i - 1, i)  measure nat_of_integer"
    by simp(transfer, simp)
qed simp

definition partial_term_of_sample :: "integer  'a"
where
  "partial_term_of_sample i =
  (if i < 0 then undefined
   else if i = 0 then zero
   else if i mod 2 = 0 then snd (a_of_integer (i div 2))
   else fst (a_of_integer (i div 2 + 1)))"

lemma partial_term_of_code:
  "partial_term_of (ty :: 'a itself) (Quickcheck_Narrowing.Narrowing_variable p t) 
    Code_Evaluation.Free (STR ''_'') tr"
  "partial_term_of (ty :: 'a itself) (Quickcheck_Narrowing.Narrowing_constructor i []) 
   Code_Evaluation.term_of (partial_term_of_sample i)"
by (rule partial_term_of_anything)+

end

lemmas [code] =
  quickcheck_narrowing_samples.narrowing_samples.simps
  quickcheck_narrowing_samples.partial_term_of_sample_def


text ‹
  The separate code target SML_word› collects setups for the
  code generator that PolyML does not provide.
›

setup Code_Target.add_derived_target ("SML_word", [(Code_ML.target_SML, I)])

code_identifier code_module Code_Target_Word_Base 
  (SML) Word and (Haskell) Word and (OCaml) Word and (Scala) Word

end

Theory Uint64

(*  Title:      Uint64.thy
    Author:     Andreas Lochbihler, ETH Zurich
*)

chapter ‹Unsigned words of 64 bits›

theory Uint64 imports
  Code_Target_Word_Base
begin

text ‹
  PolyML (in version 5.7) provides a Word64 structure only when run in 64-bit mode.
  Therefore, we by default provide an implementation of 64-bit words using \verb$IntInf.int$ and
  masking. The code target \texttt{SML\_word} replaces this implementation and maps the operations
  directly to the \verb$Word64$ structure provided by the Standard ML implementations.

  The \verb$Eval$ target used by @{command value} and @{method eval} dynamically tests at
  runtime for the version of PolyML and uses PolyML's Word64 structure if it detects a 64-bit 
  version which does not suffer from a division bug found in PolyML 5.6.
›

declare prod.Quotient[transfer_rule]

section ‹Type definition and primitive operations›

typedef uint64 = "UNIV :: 64 word set" .. 

setup_lifting type_definition_uint64

text ‹Use an abstract type for code generation to disable pattern matching on @{term Abs_uint64}.›
declare Rep_uint64_inverse[code abstype]

declare Quotient_uint64[transfer_rule]

instantiation uint64 :: comm_ring_1
begin
lift_definition zero_uint64 :: uint64 is "0 :: 64 word" .
lift_definition one_uint64 :: uint64 is "1" .
lift_definition plus_uint64 :: "uint64  uint64  uint64" is "(+) :: 64 word  _" .
lift_definition minus_uint64 :: "uint64  uint64  uint64" is "(-)" .
lift_definition uminus_uint64 :: "uint64  uint64" is uminus .
lift_definition times_uint64 :: "uint64  uint64  uint64" is "(*)" .
instance by (standard; transfer) (simp_all add: algebra_simps)
end

instantiation uint64 :: semiring_modulo
begin
lift_definition divide_uint64 :: "uint64  uint64  uint64" is "(div)" .
lift_definition modulo_uint64 :: "uint64  uint64  uint64" is "(mod)" .
instance by (standard; transfer) (fact word_mod_div_equality)
end

instantiation uint64 :: linorder begin
lift_definition less_uint64 :: "uint64  uint64  bool" is "(<)" .
lift_definition less_eq_uint64 :: "uint64  uint64  bool" is "(≤)" .
instance by (standard; transfer) (simp_all add: less_le_not_le linear)
end

lemmas [code] = less_uint64.rep_eq less_eq_uint64.rep_eq

context
  includes lifting_syntax
  notes
    transfer_rule_of_bool [transfer_rule]
    transfer_rule_numeral [transfer_rule]
begin

lemma [transfer_rule]:
  "((=) ===> cr_uint64) of_bool of_bool"
  by transfer_prover

lemma transfer_rule_numeral_uint [transfer_rule]:
  "((=) ===> cr_uint64) numeral numeral"
  by transfer_prover

lemma [transfer_rule]:
  (cr_uint64 ===> (⟷)) even ((dvd) 2 :: uint64  bool)
  by (unfold dvd_def) transfer_prover

end

instantiation uint64 :: semiring_bits
begin

lift_definition bit_uint64 :: ‹uint64  nat  bool› is bit .

instance
  by (standard; transfer)
    (fact bit_iff_odd even_iff_mod_2_eq_zero odd_iff_mod_2_eq_one odd_one bits_induct
       bits_div_0 bits_div_by_1 bits_mod_div_trivial even_succ_div_2
       even_mask_div_iff exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq
       div_exp_mod_exp_eq even_mult_exp_div_exp_iff)+

end

instantiation uint64 :: semiring_bit_shifts
begin
lift_definition push_bit_uint64 :: ‹nat  uint64  uint64› is push_bit .
lift_definition drop_bit_uint64 :: ‹nat  uint64  uint64› is drop_bit .
lift_definition take_bit_uint64 :: ‹nat  uint64  uint64› is take_bit .
instance by (standard; transfer)
  (fact push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod)+
end

instantiation uint64 :: ring_bit_operations
begin
lift_definition not_uint64 :: ‹uint64  uint64› is NOT .
lift_definition and_uint64 :: ‹uint64  uint64  uint64› is (AND) .
lift_definition or_uint64 :: ‹uint64  uint64  uint64› is (OR) .
lift_definition xor_uint64 :: ‹uint64  uint64  uint64› is (XOR) .
lift_definition mask_uint64 :: ‹nat  uint64› is mask .
instance by (standard; transfer)
  (simp_all add: bit_and_iff bit_or_iff bit_xor_iff bit_not_iff minus_eq_not_minus_1 mask_eq_decr_exp)
end

lemma [code]:
  ‹take_bit n a = a AND mask n for a :: uint64
  by (fact take_bit_eq_mask)

lemma [code]:
  ‹mask (Suc n) = push_bit n (1 :: uint64) OR mask n
  ‹mask 0 = (0 :: uint64)
  by (simp_all add: mask_Suc_exp push_bit_of_1)

instance uint64 :: semiring_bit_syntax ..

context
  includes lifting_syntax
begin

lemma test_bit_uint64_transfer [transfer_rule]:
  (cr_uint64 ===> (=)) bit (!!)
  unfolding test_bit_eq_bit by transfer_prover

lemma shiftl_uint64_transfer [transfer_rule]:
  (cr_uint64 ===> (=) ===> cr_uint64) (λk n. push_bit n k) (<<)
  unfolding shiftl_eq_push_bit by transfer_prover

lemma shiftr_uint64_transfer [transfer_rule]:
  (cr_uint64 ===> (=) ===> cr_uint64) (λk n. drop_bit n k) (>>)
  unfolding shiftr_eq_drop_bit by transfer_prover

end

instantiation uint64 :: lsb
begin
lift_definition lsb_uint64 :: ‹uint64  bool› is lsb .
instance by (standard; transfer)
  (fact lsb_odd)
end

instantiation uint64 :: msb
begin
lift_definition msb_uint64 :: ‹uint64  bool› is msb .
instance ..
end

instantiation uint64 :: set_bit
begin
lift_definition set_bit_uint64 :: ‹uint64  nat  bool  uint64› is set_bit .
instance
  apply standard
  apply transfer
  apply (simp add: bit_simps)
  done
end

instantiation uint64 :: bit_comprehension begin
lift_definition set_bits_uint64 :: "(nat  bool)  uint64" is "set_bits" .
instance by (standard; transfer) (fact set_bits_bit_eq)
end

lemmas [code] = bit_uint64.rep_eq lsb_uint64.rep_eq msb_uint64.rep_eq

instantiation uint64 :: equal begin
lift_definition equal_uint64 :: "uint64  uint64  bool" is "equal_class.equal" .
instance by standard (transfer, simp add: equal_eq)
end

lemmas [code] = equal_uint64.rep_eq

instantiation uint64 :: size begin
lift_definition size_uint64 :: "uint64  nat" is "size" .
instance ..
end

lemmas [code] = size_uint64.rep_eq

lift_definition sshiftr_uint64 :: "uint64  nat  uint64" (infixl ">>>" 55) is λw n. signed_drop_bit n w .

lift_definition uint64_of_int :: "int  uint64" is "word_of_int" .

definition uint64_of_nat :: "nat  uint64"
where "uint64_of_nat = uint64_of_int  int"

lift_definition int_of_uint64 :: "uint64  int" is "uint" .
lift_definition nat_of_uint64 :: "uint64  nat" is "unat" .

definition integer_of_uint64 :: "uint64  integer"
where "integer_of_uint64 = integer_of_int o int_of_uint64"

text ‹Use pretty numerals from integer for pretty printing›

context includes integer.lifting begin

lift_definition Uint64 :: "integer  uint64" is "word_of_int" .

lemma Rep_uint64_numeral [simp]: "Rep_uint64 (numeral n) = numeral n"
by(induction n)(simp_all add: one_uint64_def Abs_uint64_inverse numeral.simps plus_uint64_def)

lemma numeral_uint64_transfer [transfer_rule]:
  "(rel_fun (=) cr_uint64) numeral numeral"
by(auto simp add: cr_uint64_def)

lemma numeral_uint64 [code_unfold]: "numeral n = Uint64 (numeral n)"
by transfer simp

lemma Rep_uint64_neg_numeral [simp]: "Rep_uint64 (- numeral n) = - numeral n"
by(simp only: uminus_uint64_def)(simp add: Abs_uint64_inverse)

lemma neg_numeral_uint64 [code_unfold]: "- numeral n = Uint64 (- numeral n)"
by transfer(simp add: cr_uint64_def)

end

lemma Abs_uint64_numeral [code_post]: "Abs_uint64 (numeral n) = numeral n"
by(induction n)(simp_all add: one_uint64_def numeral.simps plus_uint64_def Abs_uint64_inverse)

lemma Abs_uint64_0 [code_post]: "Abs_uint64 0 = 0"
by(simp add: zero_uint64_def)

lemma Abs_uint64_1 [code_post]: "Abs_uint64 1 = 1"
by(simp add: one_uint64_def)

section ‹Code setup›

text ‹ For SML, we generate an implementation of unsigned 64-bit words using \verb$IntInf.int$.
  If @{ML "LargeWord.wordSize > 63"} of the Isabelle/ML runtime environment holds, then we assume
  that there is also a Word64› structure available and accordingly replace the implementation
  for the target \verb$Eval$.
›
code_printing code_module "Uint64"  (SML) ‹(* Test that words can handle numbers between 0 and 63 *)
val _ = if 6 <= Word.wordSize then () else raise (Fail ("wordSize less than 6"));

structure Uint64 : sig
  eqtype uint64;
  val zero : uint64;
  val one : uint64;
  val fromInt : IntInf.int -> uint64;
  val toInt : uint64 -> IntInf.int;
  val toLarge : uint64 -> LargeWord.word;
  val fromLarge : LargeWord.word -> uint64
  val plus : uint64 -> uint64 -> uint64;
  val minus : uint64 -> uint64 -> uint64;
  val times : uint64 -> uint64 -> uint64;
  val divide : uint64 -> uint64 -> uint64;
  val modulus : uint64 -> uint64 -> uint64;
  val negate : uint64 -> uint64;
  val less_eq : uint64 -> uint64 -> bool;
  val less : uint64 -> uint64 -> bool;
  val notb : uint64 -> uint64;
  val andb : uint64 -> uint64 -> uint64;
  val orb : uint64 -> uint64 -> uint64;
  val xorb : uint64 -> uint64 -> uint64;
  val shiftl : uint64 -> IntInf.int -> uint64;
  val shiftr : uint64 -> IntInf.int -> uint64;
  val shiftr_signed : uint64 -> IntInf.int -> uint64;
  val set_bit : uint64 -> IntInf.int -> bool -> uint64;
  val test_bit : uint64 -> IntInf.int -> bool;
end = struct

type uint64 = IntInf.int;

val mask = 0xFFFFFFFFFFFFFFFF : IntInf.int;

val zero = 0 : IntInf.int;

val one = 1 : IntInf.int;

fun fromInt x = IntInf.andb(x, mask);

fun toInt x = x

fun toLarge x = LargeWord.fromLargeInt (IntInf.toLarge x);

fun fromLarge x = IntInf.fromLarge (LargeWord.toLargeInt x);

fun plus x y = IntInf.andb(IntInf.+(x, y), mask);

fun minus x y = IntInf.andb(IntInf.-(x, y), mask);

fun negate x = IntInf.andb(IntInf.~(x), mask);

fun times x y = IntInf.andb(IntInf.*(x, y), mask);

fun divide x y = IntInf.div(x, y);

fun modulus x y = IntInf.mod(x, y);

fun less_eq x y = IntInf.<=(x, y);

fun less x y = IntInf.<(x, y);

fun notb x = IntInf.andb(IntInf.notb(x), mask);

fun orb x y = IntInf.orb(x, y);

fun andb x y = IntInf.andb(x, y);

fun xorb x y = IntInf.xorb(x, y);

val maxWord = IntInf.pow (2, Word.wordSize);

fun shiftl x n = 
  if n < maxWord then IntInf.andb(IntInf.<< (x, Word.fromLargeInt (IntInf.toLarge n)), mask)
  else 0;

fun shiftr x n =
  if n < maxWord then IntInf.~>> (x, Word.fromLargeInt (IntInf.toLarge n))
  else 0;

val msb_mask = 0x8000000000000000 : IntInf.int;

fun shiftr_signed x i =
  if IntInf.andb(x, msb_mask) = 0 then shiftr x i
  else if i >= 64 then 0xFFFFFFFFFFFFFFFF
  else let
    val x' = shiftr x i
    val m' = IntInf.andb(IntInf.<<(mask, Word.max(0w64 - Word.fromLargeInt (IntInf.toLarge i), 0w0)), mask)
  in IntInf.orb(x', m') end;

fun test_bit x n =
  if n < maxWord then IntInf.andb (x, IntInf.<< (1, Word.fromLargeInt (IntInf.toLarge n))) <> 0
  else false;

fun set_bit x n b =
  if n < 64 then
    if b then IntInf.orb (x, IntInf.<< (1, Word.fromLargeInt (IntInf.toLarge n)))
    else IntInf.andb (x, IntInf.notb (IntInf.<< (1, Word.fromLargeInt (IntInf.toLarge n))))
  else x;

end
›
code_reserved SML Uint64

setup let
  val polyml64 = LargeWord.wordSize > 63;
  (* PolyML 5.6 has bugs in its Word64 implementation. We test for one such bug and refrain
     from using Word64 in that case. Testing is done with dynamic code evaluation such that
     the compiler does not choke on the Word64 structure, which need not be present in a 32bit
     environment. *)
  val error_msg = "Buggy Word64 structure";
  val test_code = 
   "val _ = if Word64.div (0w18446744073709551611 : Word64.word, 0w3) = 0w6148914691236517203 then ()\n" ^
   "else raise (Fail \"" ^ error_msg ^ "\");";
  val f = Exn.interruptible_capture (fn () => ML_Compiler.eval ML_Compiler.flags Position.none (ML_Lex.tokenize test_code))
  val use_Word64 = polyml64 andalso
    (case f () of 
       Exn.Res _ => true
     | Exn.Exn (e as ERROR m) => if String.isSuffix error_msg m then false else Exn.reraise e
     | Exn.Exn e => Exn.reraise e)
    ;

  val newline = "\n";
  val content = 
    "structure Uint64 : sig" ^ newline ^
    "  eqtype uint64;" ^ newline ^
    "  val zero : uint64;" ^ newline ^
    "  val one : uint64;" ^ newline ^
    "  val fromInt : IntInf.int -> uint64;" ^ newline ^
    "  val toInt : uint64 -> IntInf.int;" ^ newline ^
    "  val toLarge : uint64 -> LargeWord.word;" ^ newline ^
    "  val fromLarge : LargeWord.word -> uint64" ^ newline ^
    "  val plus : uint64 -> uint64 -> uint64;" ^ newline ^
    "  val minus : uint64 -> uint64 -> uint64;" ^ newline ^
    "  val times : uint64 -> uint64 -> uint64;" ^ newline ^
    "  val divide : uint64 -> uint64 -> uint64;" ^ newline ^
    "  val modulus : uint64 -> uint64 -> uint64;" ^ newline ^
    "  val negate : uint64 -> uint64;" ^ newline ^
    "  val less_eq : uint64 -> uint64 -> bool;" ^ newline ^
    "  val less : uint64 -> uint64 -> bool;" ^ newline ^
    "  val notb : uint64 -> uint64;" ^ newline ^
    "  val andb : uint64 -> uint64 -> uint64;" ^ newline ^
    "  val orb : uint64 -> uint64 -> uint64;" ^ newline ^
    "  val xorb : uint64 -> uint64 -> uint64;" ^ newline ^
    "  val shiftl : uint64 -> IntInf.int -> uint64;" ^ newline ^
    "  val shiftr : uint64 -> IntInf.int -> uint64;" ^ newline ^
    "  val shiftr_signed : uint64 -> IntInf.int -> uint64;" ^ newline ^
    "  val set_bit : uint64 -> IntInf.int -> bool -> uint64;" ^ newline ^
    "  val test_bit : uint64 -> IntInf.int -> bool;" ^ newline ^
    "end = struct" ^ newline ^
    "" ^ newline ^
    "type uint64 = Word64.word;" ^ newline ^
    "" ^ newline ^
    "val zero = (0wx0 : uint64);" ^ newline ^
    "" ^ newline ^
    "val one = (0wx1 : uint64);" ^ newline ^
    "" ^ newline ^
    "fun fromInt x = Word64.fromLargeInt (IntInf.toLarge x);" ^ newline ^
    "" ^ newline ^
    "fun toInt x = IntInf.fromLarge (Word64.toLargeInt x);"  ^ newline ^
    "" ^ newline ^
    "fun fromLarge x = Word64.fromLarge x;" ^ newline ^
    "" ^ newline ^
    "fun toLarge x = Word64.toLarge x;"  ^ newline ^
    "" ^ newline ^
    "fun plus x y = Word64.+(x, y);" ^ newline ^
    "" ^ newline ^
    "fun minus x y = Word64.-(x, y);" ^ newline ^
    "" ^ newline ^
    "fun negate x = Word64.~(x);" ^ newline ^
    "" ^ newline ^
    "fun times x y = Word64.*(x, y);" ^ newline ^
    "" ^ newline ^
    "fun divide x y = Word64.div(x, y);" ^ newline ^
    "" ^ newline ^
    "fun modulus x y = Word64.mod(x, y);" ^ newline ^
    "" ^ newline ^
    "fun less_eq x y = Word64.<=(x, y);" ^ newline ^
    "" ^ newline ^
    "fun less x y = Word64.<(x, y);" ^ newline ^
    "" ^ newline ^
    "fun set_bit x n b =" ^ newline ^
    "  let val mask = Word64.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))" ^ newline ^
    "  in if b then Word64.orb (x, mask)" ^ newline ^
    "     else Word64.andb (x, Word64.notb mask)" ^ newline ^
    "  end" ^ newline ^
    "" ^ newline ^
    "fun shiftl x n =" ^ newline ^
    "  Word64.<< (x, Word.fromLargeInt (IntInf.toLarge n))" ^ newline ^
    "" ^ newline ^
    "fun shiftr x n =" ^ newline ^
    "  Word64.>> (x, Word.fromLargeInt (IntInf.toLarge n))" ^ newline ^
    "" ^ newline ^
    "fun shiftr_signed x n =" ^ newline ^
    "  Word64.~>> (x, Word.fromLargeInt (IntInf.toLarge n))" ^ newline ^
    "" ^ newline ^
    "fun test_bit x n =" ^ newline ^
    "  Word64.andb (x, Word64.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))) <> Word64.fromInt 0" ^ newline ^
    "" ^ newline ^
    "val notb = Word64.notb" ^ newline ^
    "" ^ newline ^
    "fun andb x y = Word64.andb(x, y);" ^ newline ^
    "" ^ newline ^
    "fun orb x y = Word64.orb(x, y);" ^ newline ^
    "" ^ newline ^
    "fun xorb x y = Word64.xorb(x, y);" ^ newline ^
    "" ^ newline ^
    "end (*struct Uint64*)"
  val target_SML64 = "SML_word";
in
  (if use_Word64 then Code_Target.set_printings (Code_Symbol.Module ("Uint64", [(Code_Runtime.target, SOME (content, []))])) else I)
  #> Code_Target.set_printings (Code_Symbol.Module ("Uint64", [(target_SML64, SOME (content, []))]))
end

code_printing code_module Uint64  (Haskell)
 ‹module Uint64(Int64, Word64) where

  import Data.Int(Int64)
  import Data.Word(Word64)›
code_reserved Haskell Uint64

text ‹
  OCaml and Scala provide only signed 64bit numbers, so we use these and 
  implement sign-sensitive operations like comparisons manually.
›
code_printing code_module "Uint64"  (OCaml)
‹module Uint64 : sig
  val less : int64 -> int64 -> bool
  val less_eq : int64 -> int64 -> bool
  val set_bit : int64 -> Z.t -> bool -> int64
  val shiftl : int64 -> Z.t -> int64
  val shiftr : int64 -> Z.t -> int64
  val shiftr_signed : int64 -> Z.t -> int64
  val test_bit : int64 -> Z.t -> bool
end = struct

(* negative numbers have their highest bit set, 
   so they are greater than positive ones *)
let less x y =
  if Int64.compare x Int64.zero < 0 then
    Int64.compare y Int64.zero < 0 && Int64.compare x y < 0
  else Int64.compare y Int64.zero < 0 || Int64.compare x y < 0;;

let less_eq x y =
  if Int64.compare x Int64.zero < 0 then
    Int64.compare y Int64.zero < 0 && Int64.compare x y <= 0
  else Int64.compare y Int64.zero < 0 || Int64.compare x y <= 0;;

let set_bit x n b =
  let mask = Int64.shift_left Int64.one (Z.to_int n)
  in if b then Int64.logor x mask
     else Int64.logand x (Int64.lognot mask);;

let shiftl x n = Int64.shift_left x (Z.to_int n);;

let shiftr x n = Int64.shift_right_logical x (Z.to_int n);;

let shiftr_signed x n = Int64.shift_right x (Z.to_int n);;

let test_bit x n =
  Int64.compare 
    (Int64.logand x (Int64.shift_left Int64.one (Z.to_int n)))
    Int64.zero
  <> 0;;

end;; (*struct Uint64*)›
code_reserved OCaml Uint64

code_printing code_module Uint64  (Scala)
‹object Uint64 {

def less(x: Long, y: Long) : Boolean =
  if (x < 0) y < 0 && x < y
  else y < 0 || x < y

def less_eq(x: Long, y: Long) : Boolean =
  if (x < 0) y < 0 && x <= y
  else y < 0 || x <= y

def set_bit(x: Long, n: BigInt, b: Boolean) : Long =
  if (b)
    x | (1L << n.intValue)
  else
    x & (1L << n.intValue).unary_~

def shiftl(x: Long, n: BigInt) : Long = x << n.intValue

def shiftr(x: Long, n: BigInt) : Long = x >>> n.intValue

def shiftr_signed(x: Long, n: BigInt) : Long = x >> n.intValue

def test_bit(x: Long, n: BigInt) : Boolean =
  (x & (1L << n.intValue)) != 0

} /* object Uint64 */›
code_reserved Scala Uint64

text ‹
  OCaml's conversion from Big\_int to int64 demands that the value fits int a signed 64-bit integer.
  The following justifies the implementation.
›

definition Uint64_signed :: "integer  uint64" 
where "Uint64_signed i = (if i < -(0x8000000000000000)  i  0x8000000000000000 then undefined Uint64 i else Uint64 i)"

lemma Uint64_code [code]:
  "Uint64 i = 
  (let i' = i AND 0xFFFFFFFFFFFFFFFF
   in if bit i' 63 then Uint64_signed (i' - 0x10000000000000000) else Uint64_signed i')"
  including undefined_transfer integer.lifting unfolding Uint64_signed_def
  apply transfer
  apply (subst word_of_int_via_signed)
     apply (auto simp add: shiftl_eq_push_bit push_bit_of_1 mask_eq_exp_minus_1 word_of_int_via_signed cong del: if_cong)
  done

lemma Uint64_signed_code [code abstract]:
  "Rep_uint64 (Uint64_signed i) = 
  (if i < -(0x8000000000000000)  i  0x8000000000000000 then Rep_uint64 (undefined Uint64 i) else word_of_int (int_of_integer_symbolic i))"
unfolding Uint64_signed_def Uint64_def int_of_integer_symbolic_def word_of_integer_def
by(simp add: Abs_uint64_inverse)

text ‹
  Avoid @{term Abs_uint64} in generated code, use @{term Rep_uint64'} instead. 
  The symbolic implementations for code\_simp use @{term Rep_uint64}.

  The new destructor @{term Rep_uint64'} is executable.
  As the simplifier is given the [code abstract] equations literally, 
  we cannot implement @{term Rep_uint64} directly, because that makes code\_simp loop.

  If code generation raises Match, some equation probably contains @{term Rep_uint64} 
  ([code abstract] equations for @{typ uint64} may use @{term Rep_uint64} because
  these instances will be folded away.)

  To convert @{typ "64 word"} values into @{typ uint64}, use @{term "Abs_uint64'"}.
›

definition Rep_uint64' where [simp]: "Rep_uint64' = Rep_uint64"

lemma Rep_uint64'_transfer [transfer_rule]:
  "rel_fun cr_uint64 (=) (λx. x) Rep_uint64'"
unfolding Rep_uint64'_def by(rule uint64.rep_transfer)

lemma Rep_uint64'_code [code]: "Rep_uint64' x = (BITS n. bit x n)"
  by transfer (simp add: set_bits_bit_eq)

lift_definition Abs_uint64' :: "64 word  uint64" is "λx :: 64 word. x" .

lemma Abs_uint64'_code [code]:
  "Abs_uint64' x = Uint64 (integer_of_int (uint x))"
including integer.lifting by transfer simp

declare [[code drop: "term_of_class.term_of :: uint64  _"]]

lemma term_of_uint64_code [code]:
  defines "TR  typerep.Typerep" and "bit0  STR ''Numeral_Type.bit0''" 
  shows
  "term_of_class.term_of x = 
   Code_Evaluation.App (Code_Evaluation.Const (STR ''Uint64.uint64.Abs_uint64'') (TR (STR ''fun'') [TR (STR ''Word.word'') [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR (STR ''Numeral_Type.num1'') []]]]]]]], TR (STR ''Uint64.uint64'') []]))
       (term_of_class.term_of (Rep_uint64' x))"
by(simp add: term_of_anything)

code_printing
  type_constructor uint64 
  (SML) "Uint64.uint64" and
  (Haskell) "Uint64.Word64" and
  (OCaml) "int64" and
  (Scala) "Long"
| constant Uint64 
  (SML) "Uint64.fromInt" and
  (Haskell) "(Prelude.fromInteger _ :: Uint64.Word64)" and
  (Haskell_Quickcheck) "(Prelude.fromInteger (Prelude.toInteger _) :: Uint64.Word64)" and
  (Scala) "_.longValue"
| constant Uint64_signed 
  (OCaml) "Z.to'_int64"
| constant "0 :: uint64" 
  (SML) "Uint64.zero" and
  (Haskell) "(0 :: Uint64.Word64)" and
  (OCaml) "Int64.zero" and
  (Scala) "0"
| constant "1 :: uint64" 
  (SML) "Uint64.one" and
  (Haskell) "(1 :: Uint64.Word64)" and
  (OCaml) "Int64.one" and
  (Scala) "1"
| constant "plus :: uint64  _ " 
  (SML) "Uint64.plus" and
  (Haskell) infixl 6 "+" and
  (OCaml) "Int64.add" and
  (Scala) infixl 7 "+"
| constant "uminus :: uint64  _" 
  (SML) "Uint64.negate" and
  (Haskell) "negate" and
  (OCaml) "Int64.neg" and
  (Scala) "!(- _)"
| constant "minus :: uint64  _" 
  (SML) "Uint64.minus" and
  (Haskell) infixl 6 "-" and
  (OCaml) "Int64.sub" and
  (Scala) infixl 7 "-"
| constant "times :: uint64  _  _" 
  (SML) "Uint64.times" and
  (Haskell) infixl 7 "*" and
  (OCaml) "Int64.mul" and
  (Scala) infixl 8 "*"
| constant "HOL.equal :: uint64  _  bool" 
  (SML) "!((_ : Uint64.uint64) = _)" and
  (Haskell) infix 4 "==" and
  (OCaml) "(Int64.compare _ _ = 0)" and
  (Scala) infixl 5 "=="
| class_instance uint64 :: equal 
  (Haskell) -
| constant "less_eq :: uint64  _  bool" 
  (SML) "Uint64.less'_eq" and
  (Haskell) infix 4 "<=" and
  (OCaml) "Uint64.less'_eq" and
  (Scala) "Uint64.less'_eq"
| constant "less :: uint64  _  bool" 
  (SML) "Uint64.less" and
  (Haskell) infix 4 "<" and
  (OCaml) "Uint64.less" and
  (Scala) "Uint64.less"
| constant "NOT :: uint64  _" 
  (SML) "Uint64.notb" and
  (Haskell) "Data'_Bits.complement" and
  (OCaml) "Int64.lognot" and
  (Scala) "_.unary'_~"
| constant "(AND) :: uint64  _" 
  (SML) "Uint64.andb" and
  (Haskell) infixl 7 "Data_Bits..&." and
  (OCaml) "Int64.logand" and
  (Scala) infixl 3 "&"
| constant "(OR) :: uint64  _" 
  (SML) "Uint64.orb" and
  (Haskell) infixl 5 "Data_Bits..|." and
  (OCaml) "Int64.logor" and
  (Scala) infixl 1 "|"
| constant "(XOR) :: uint64  _" 
  (SML) "Uint64.xorb" and
  (Haskell) "Data'_Bits.xor" and
  (OCaml) "Int64.logxor" and
  (Scala) infixl 2 "^"

definition uint64_divmod :: "uint64  uint64  uint64 × uint64" where
  "uint64_divmod x y = 
  (if y = 0 then (undefined ((div) :: uint64  _) x (0 :: uint64), undefined ((mod) :: uint64  _) x (0 :: uint64)) 
  else (x div y, x mod y))"

definition uint64_div :: "uint64  uint64  uint64" 
where "uint64_div x y = fst (uint64_divmod x y)"

definition uint64_mod :: "uint64  uint64  uint64" 
where "uint64_mod x y = snd (uint64_divmod x y)"

lemma div_uint64_code [code]: "x div y = (if y = 0 then 0 else uint64_div x y)"
including undefined_transfer unfolding uint64_divmod_def uint64_div_def
by transfer (simp add: word_div_def)

lemma mod_uint64_code [code]: "x mod y = (if y = 0 then x else uint64_mod x y)"
including undefined_transfer unfolding uint64_mod_def uint64_divmod_def
by transfer (simp add: word_mod_def)

definition uint64_sdiv :: "uint64  uint64  uint64"
where [code del]:
  "uint64_sdiv x y =
   (if y = 0 then undefined ((div) :: uint64  _) x (0 :: uint64)
    else Abs_uint64 (Rep_uint64 x sdiv Rep_uint64 y))"

definition div0_uint64 :: "uint64  uint64"
where [code del]: "div0_uint64 x = undefined ((div) :: uint64  _) x (0 :: uint64)"
declare [[code abort: div0_uint64]]

definition mod0_uint64 :: "uint64  uint64"
where [code del]: "mod0_uint64 x = undefined ((mod) :: uint64  _) x (0 :: uint64)"
declare [[code abort: mod0_uint64]]

lemma uint64_divmod_code [code]:
  "uint64_divmod x y =
  (if 0x8000000000000000  y then if x < y then (0, x) else (1, x - y)
   else if y = 0 then (div0_uint64 x, mod0_uint64 x)
   else let q = push_bit 1 (uint64_sdiv (drop_bit 1 x) y);
            r = x - q * y
        in if r  y then (q + 1, r - y) else (q, r))"
  including undefined_transfer unfolding uint64_divmod_def uint64_sdiv_def div0_uint64_def mod0_uint64_def
  by transfer (simp add: divmod_via_sdivmod shiftr_eq_drop_bit shiftl_eq_push_bit ac_simps)

lemma uint64_sdiv_code [code abstract]:
  "Rep_uint64 (uint64_sdiv x y) =
   (if y = 0 then Rep_uint64 (undefined ((div) :: uint64  _) x (0 :: uint64))
    else Rep_uint64 x sdiv Rep_uint64 y)"
unfolding uint64_sdiv_def by(simp add: Abs_uint64_inverse)

text ‹
  Note that we only need a translation for signed division, but not for the remainder
  because @{thm uint64_divmod_code} computes both with division only.
›

code_printing
  constant uint64_div 
  (SML) "Uint64.divide" and
  (Haskell) "Prelude.div"
| constant uint64_mod 
  (SML) "Uint64.modulus" and
  (Haskell) "Prelude.mod"
| constant uint64_divmod 
  (Haskell) "divmod"
| constant uint64_sdiv 
  (OCaml) "Int64.div" and
  (Scala) "_ '/ _"

definition uint64_test_bit :: "uint64  integer  bool"
where [code del]:
  "uint64_test_bit x n =
  (if n < 0  63 < n then undefined (bit :: uint64  _) x n
   else bit x (nat_of_integer n))"

lemma bit_uint64_code [code]:
  "bit x n  n < 64  uint64_test_bit x (integer_of_nat n)"
  including undefined_transfer integer.lifting unfolding uint64_test_bit_def
  by (transfer, simp, transfer, simp)

lemma uint64_test_bit_code [code]:
  "uint64_test_bit w n =
  (if n < 0  63 < n then undefined (bit :: uint64  _) w n else bit (Rep_uint64 w) (nat_of_integer n))"
  unfolding uint64_test_bit_def by(simp add: bit_uint64.rep_eq)

code_printing constant uint64_test_bit 
  (SML) "Uint64.test'_bit" and
  (Haskell) "Data'_Bits.testBitBounded" and
  (OCaml) "Uint64.test'_bit" and
  (Scala) "Uint64.test'_bit" and
  (Eval) "(fn x => fn i => if i < 0 orelse i >= 64 then raise (Fail \"argument to uint64'_test'_bit out of bounds\") else Uint64.test'_bit x i)"

definition uint64_set_bit :: "uint64  integer  bool  uint64"
where [code del]:
  "uint64_set_bit x n b =
  (if n < 0  63 < n then undefined (set_bit :: uint64  _) x n b
   else set_bit x (nat_of_integer n) b)"

lemma set_bit_uint64_code [code]:
  "set_bit x n b = (if n < 64 then uint64_set_bit x (integer_of_nat n) b else x)"
including undefined_transfer integer.lifting unfolding uint64_set_bit_def
by(transfer)(auto cong: conj_cong simp add: not_less set_bit_beyond word_size)

lemma uint64_set_bit_code [code abstract]:
  "Rep_uint64 (uint64_set_bit w n b) = 
  (if n < 0  63 < n then Rep_uint64 (undefined (set_bit :: uint64  _) w n b)
   else set_bit (Rep_uint64 w) (nat_of_integer n) b)"
including undefined_transfer unfolding uint64_set_bit_def by transfer simp

code_printing constant uint64_set_bit 
  (SML) "Uint64.set'_bit" and
  (Haskell) "Data'_Bits.setBitBounded" and
  (OCaml) "Uint64.set'_bit" and
  (Scala) "Uint64.set'_bit" and
  (Eval) "(fn x => fn i => fn b => if i < 0 orelse i >= 64 then raise (Fail \"argument to uint64'_set'_bit out of bounds\") else Uint64.set'_bit x i b)"

lift_definition uint64_set_bits :: "(nat  bool)  uint64  nat  uint64" is set_bits_aux .

lemma uint64_set_bits_code [code]:
  "uint64_set_bits f w n =
  (if n = 0 then w 
   else let n' = n - 1 in uint64_set_bits f (push_bit 1 w OR (if f n' then 1 else 0)) n')"
  apply (transfer fixing: n)
  apply (cases n)
   apply (simp_all add: shiftl_eq_push_bit)
  done

lemma set_bits_uint64 [code]:
  "(BITS n. f n) = uint64_set_bits f 0 64"
by transfer(simp add: set_bits_conv_set_bits_aux)


lemma lsb_code [code]: fixes x :: uint64 shows "lsb x = bit x 0"
  by transfer (simp add: lsb_word_eq)


definition uint64_shiftl :: "uint64  integer  uint64"
where [code del]:
  "uint64_shiftl x n = (if n < 0  64  n then undefined (push_bit :: nat  uint64  _) x n else push_bit (nat_of_integer n) x)"

lemma shiftl_uint64_code [code]: "push_bit n x = (if n < 64 then uint64_shiftl x (integer_of_nat n) else 0)"
  including undefined_transfer integer.lifting unfolding uint64_shiftl_def
  by transfer simp

lemma uint64_shiftl_code [code abstract]:
  "Rep_uint64 (uint64_shiftl w n) =
  (if n < 0  64  n then Rep_uint64 (undefined (push_bit :: nat  uint64  _) w n) else push_bit (nat_of_integer n) (Rep_uint64 w))"
including undefined_transfer unfolding uint64_shiftl_def by transfer simp

code_printing constant uint64_shiftl 
  (SML) "Uint64.shiftl" and
  (Haskell) "Data'_Bits.shiftlBounded" and
  (OCaml) "Uint64.shiftl" and
  (Scala) "Uint64.shiftl" and
  (Eval) "(fn x => fn i => if i < 0 orelse i >= 64 then raise (Fail \"argument to uint64'_shiftl out of bounds\") else Uint64.shiftl x i)"


definition uint64_shiftr :: "uint64  integer  uint64"
where [code del]:
  "uint64_shiftr x n = (if n < 0  64  n then undefined (drop_bit :: nat  uint64  _) x n else drop_bit (nat_of_integer n) x)"

lemma shiftr_uint64_code [code]: "drop_bit n x = (if n < 64 then uint64_shiftr x (integer_of_nat n) else 0)"
  including undefined_transfer integer.lifting unfolding uint64_shiftr_def
  by transfer simp

lemma uint64_shiftr_code [code abstract]:
  "Rep_uint64 (uint64_shiftr w n) =
  (if n < 0  64  n then Rep_uint64 (undefined (drop_bit :: nat  uint64  _) w n) else drop_bit (nat_of_integer n) (Rep_uint64 w))"
  including undefined_transfer unfolding uint64_shiftr_def by transfer simp

code_printing constant uint64_shiftr 
  (SML) "Uint64.shiftr" and
  (Haskell) "Data'_Bits.shiftrBounded" and
  (OCaml) "Uint64.shiftr" and
  (Scala) "Uint64.shiftr" and
  (Eval) "(fn x => fn i => if i < 0 orelse i >= 64 then raise (Fail \"argument to uint64'_shiftr out of bounds\") else Uint64.shiftr x i)"


definition uint64_sshiftr :: "uint64  integer  uint64"
where [code del]:
  "uint64_sshiftr x n =
  (if n < 0  64  n then undefined sshiftr_uint64 x n else sshiftr_uint64 x (nat_of_integer n))"

lemma sshiftr_uint64_code [code]:
  "x >>> n = 
  (if n < 64 then uint64_sshiftr x (integer_of_nat n) else if bit x 63 then - 1 else 0)"
  including undefined_transfer integer.lifting unfolding uint64_sshiftr_def
  by transfer (simp add: not_less signed_drop_bit_beyond)

lemma uint64_sshiftr_code [code abstract]:
  "Rep_uint64 (uint64_sshiftr w n) =
  (if n < 0  64  n then Rep_uint64 (undefined sshiftr_uint64 w n) else signed_drop_bit (nat_of_integer n) (Rep_uint64 w))"
including undefined_transfer unfolding uint64_sshiftr_def by transfer simp

code_printing constant uint64_sshiftr 
  (SML) "Uint64.shiftr'_signed" and
  (Haskell) 
    "(Prelude.fromInteger (Prelude.toInteger (Data'_Bits.shiftrBounded (Prelude.fromInteger (Prelude.toInteger _) :: Uint64.Int64) _)) :: Uint64.Word64)" and
  (OCaml) "Uint64.shiftr'_signed" and
  (Scala) "Uint64.shiftr'_signed" and
  (Eval) "(fn x => fn i => if i < 0 orelse i >= 64 then raise (Fail \"argument to uint64'_shiftr'_signed out of bounds\") else Uint64.shiftr'_signed x i)"

lemma uint64_msb_test_bit: "msb x  bit (x :: uint64) 63"
  by transfer (simp add: msb_word_iff_bit)

lemma msb_uint64_code [code]: "msb x  uint64_test_bit x 63"
  by (simp add: uint64_test_bit_def uint64_msb_test_bit)

lemma uint64_of_int_code [code]: "uint64_of_int i = Uint64 (integer_of_int i)"
including integer.lifting by transfer simp

lemma int_of_uint64_code [code]:
  "int_of_uint64 x = int_of_integer (integer_of_uint64 x)"
by(simp add: integer_of_uint64_def)

lemma nat_of_uint64_code [code]:
  "nat_of_uint64 x = nat_of_integer (integer_of_uint64 x)"
unfolding integer_of_uint64_def including integer.lifting by transfer simp

definition integer_of_uint64_signed :: "uint64  integer"
where
  "integer_of_uint64_signed n = (if bit n 63 then undefined integer_of_uint64 n else integer_of_uint64 n)"

lemma integer_of_uint64_signed_code [code]:
  "integer_of_uint64_signed n =
  (if bit n 63 then undefined integer_of_uint64 n else integer_of_int (uint (Rep_uint64' n)))"
unfolding integer_of_uint64_signed_def integer_of_uint64_def
including undefined_transfer by transfer simp

lemma integer_of_uint64_code [code]:
  "integer_of_uint64 n =
  (if bit n 63 then integer_of_uint64_signed (n AND 0x7FFFFFFFFFFFFFFF) OR 0x8000000000000000 else integer_of_uint64_signed n)"
proof -
  have (0x7FFFFFFFFFFFFFFF :: uint64) = mask 63
    by (simp add: mask_eq_exp_minus_1)
  then have *: n AND 0x7FFFFFFFFFFFFFFF = take_bit 63 n
    by (simp add: take_bit_eq_mask)
  have **: (0x8000000000000000 :: int) = 2 ^ 63
    by simp
  show ?thesis
    unfolding integer_of_uint64_def integer_of_uint64_signed_def o_def *
    including undefined_transfer integer.lifting
    apply transfer
    apply (rule bit_eqI)
    apply (simp add: test_bit_eq_bit bit_or_iff bit_take_bit_iff bit_uint_iff)
    apply (simp only: bit_exp_iff bit_or_iff **)
    apply auto
    done
qed

code_printing
  constant "integer_of_uint64" 
  (SML) "Uint64.toInt" and
  (Haskell) "Prelude.toInteger"
| constant "integer_of_uint64_signed" 
  (OCaml) "Z.of'_int64" and
  (Scala) "BigInt"

section ‹Quickcheck setup›

definition uint64_of_natural :: "natural  uint64"
where "uint64_of_natural x  Uint64 (integer_of_natural x)"

instantiation uint64 :: "{random, exhaustive, full_exhaustive}" begin
definition "random_uint64  qc_random_cnv uint64_of_natural"
definition "exhaustive_uint64  qc_exhaustive_cnv uint64_of_natural"
definition "full_exhaustive_uint64  qc_full_exhaustive_cnv uint64_of_natural"
instance ..
end

instantiation uint64 :: narrowing begin

interpretation quickcheck_narrowing_samples
  "λi. let x = Uint64 i in (x, 0xFFFFFFFFFFFFFFFF - x)" "0"
  "Typerep.Typerep (STR ''Uint64.uint64'') []" .

definition "narrowing_uint64 d = qc_narrowing_drawn_from (narrowing_samples d) d"
declare [[code drop: "partial_term_of :: uint64 itself  _"]]
lemmas partial_term_of_uint64 [code] = partial_term_of_code

instance ..
end

no_notation sshiftr_uint64 (infixl ">>>" 55)

end

Theory Uint32

(*  Title:      Uint32.thy
    Author:     Andreas Lochbihler, ETH Zurich
*)

chapter ‹Unsigned words of 32 bits›

theory Uint32 imports
  Code_Target_Word_Base
begin

declare prod.Quotient[transfer_rule]

section ‹Type definition and primitive operations›

typedef uint32 = "UNIV :: 32 word set" .. 

setup_lifting type_definition_uint32

text ‹Use an abstract type for code generation to disable pattern matching on @{term Abs_uint32}.›
declare Rep_uint32_inverse[code abstype]

declare Quotient_uint32[transfer_rule]

instantiation uint32 :: comm_ring_1
begin
lift_definition zero_uint32 :: uint32 is "0 :: 32 word" .
lift_definition one_uint32 :: uint32 is "1" .
lift_definition plus_uint32 :: "uint32  uint32  uint32" is "(+) :: 32 word  _" .
lift_definition minus_uint32 :: "uint32  uint32  uint32" is "(-)" .
lift_definition uminus_uint32 :: "uint32  uint32" is uminus .
lift_definition times_uint32 :: "uint32  uint32  uint32" is "(*)" .
instance by (standard; transfer) (simp_all add: algebra_simps)
end

instantiation uint32 :: semiring_modulo
begin
lift_definition divide_uint32 :: "uint32  uint32  uint32" is "(div)" .
lift_definition modulo_uint32 :: "uint32  uint32  uint32" is "(mod)" .
instance by (standard; transfer) (fact word_mod_div_equality)
end

instantiation uint32 :: linorder begin
lift_definition less_uint32 :: "uint32  uint32  bool" is "(<)" .
lift_definition less_eq_uint32 :: "uint32  uint32  bool" is "(≤)" .
instance by (standard; transfer) (simp_all add: less_le_not_le linear)
end

lemmas [code] = less_uint32.rep_eq less_eq_uint32.rep_eq

context
  includes lifting_syntax
  notes
    transfer_rule_of_bool [transfer_rule]
    transfer_rule_numeral [transfer_rule]
begin

lemma [transfer_rule]:
  "((=) ===> cr_uint32) of_bool of_bool"
  by transfer_prover

lemma transfer_rule_numeral_uint [transfer_rule]:
  "((=) ===> cr_uint32) numeral numeral"
  by transfer_prover

lemma [transfer_rule]:
  (cr_uint32 ===> (⟷)) even ((dvd) 2 :: uint32  bool)
  by (unfold dvd_def) transfer_prover

end

instantiation uint32:: semiring_bits
begin

lift_definition bit_uint32 :: ‹uint32  nat  bool› is bit .

instance
  by (standard; transfer)
    (fact bit_iff_odd even_iff_mod_2_eq_zero odd_iff_mod_2_eq_one odd_one bits_induct
       bits_div_0 bits_div_by_1 bits_mod_div_trivial even_succ_div_2
       even_mask_div_iff exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq
       div_exp_mod_exp_eq even_mult_exp_div_exp_iff)+

end

instantiation uint32 :: semiring_bit_shifts
begin
lift_definition push_bit_uint32 :: ‹nat  uint32  uint32› is push_bit .
lift_definition drop_bit_uint32 :: ‹nat  uint32  uint32› is drop_bit .
lift_definition take_bit_uint32 :: ‹nat  uint32  uint32› is take_bit .
instance by (standard; transfer)
  (fact push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod)+
end

instantiation uint32 :: ring_bit_operations
begin
lift_definition not_uint32 :: ‹uint32  uint32› is NOT .
lift_definition and_uint32 :: ‹uint32  uint32  uint32› is (AND) .
lift_definition or_uint32 :: ‹uint32  uint32  uint32› is (OR) .
lift_definition xor_uint32 :: ‹uint32  uint32  uint32› is (XOR) .
lift_definition mask_uint32 :: ‹nat  uint32› is mask .
instance by (standard; transfer)
  (simp_all add: bit_and_iff bit_or_iff bit_xor_iff bit_not_iff minus_eq_not_minus_1 mask_eq_decr_exp)
end

lemma [code]:
  ‹take_bit n a = a AND mask n for a :: uint32
  by (fact take_bit_eq_mask)

lemma [code]:
  ‹mask (Suc n) = push_bit n (1 :: uint32) OR mask n
  ‹mask 0 = (0 :: uint32)
  by (simp_all add: mask_Suc_exp push_bit_of_1)

instance uint32 :: semiring_bit_syntax ..

context
  includes lifting_syntax
begin

lemma test_bit_uint32_transfer [transfer_rule]:
  (cr_uint32 ===> (=)) bit (!!)
  unfolding test_bit_eq_bit by transfer_prover

lemma shiftl_uint32_transfer [transfer_rule]:
  (cr_uint32 ===> (=) ===> cr_uint32) (λk n. push_bit n k) (<<)
  unfolding shiftl_eq_push_bit by transfer_prover

lemma shiftr_uint32_transfer [transfer_rule]:
  (cr_uint32 ===> (=) ===> cr_uint32) (λk n. drop_bit n k) (>>)
  unfolding shiftr_eq_drop_bit by transfer_prover

end

instantiation uint32 :: lsb
begin
lift_definition lsb_uint32 :: ‹uint32  bool› is lsb .
instance by (standard; transfer)
  (fact lsb_odd)
end

instantiation uint32 :: msb
begin
lift_definition msb_uint32 :: ‹uint32  bool› is msb .
instance ..
end

instantiation uint32 :: set_bit
begin
lift_definition set_bit_uint32 :: ‹uint32  nat  bool  uint32› is set_bit .
instance
  apply standard
  apply transfer
  apply (simp add: bit_simps)
  done
end

instantiation uint32 :: bit_comprehension begin
lift_definition set_bits_uint32 :: "(nat  bool)  uint32" is "set_bits" .
instance by (standard; transfer) (fact set_bits_bit_eq)
end

lemmas [code] = bit_uint32.rep_eq lsb_uint32.rep_eq msb_uint32.rep_eq

instantiation uint32 :: equal begin
lift_definition equal_uint32 :: "uint32  uint32  bool" is "equal_class.equal" .
instance by standard (transfer, simp add: equal_eq)
end

lemmas [code] = equal_uint32.rep_eq

instantiation uint32 :: size begin
lift_definition size_uint32 :: "uint32  nat" is "size" .
instance ..
end

lemmas [code] = size_uint32.rep_eq                                                    

lift_definition sshiftr_uint32 :: "uint32  nat  uint32" (infixl ">>>" 55) is λw n. signed_drop_bit n w .

lift_definition uint32_of_int :: "int  uint32" is "word_of_int" .

definition uint32_of_nat :: "nat  uint32"
where "uint32_of_nat = uint32_of_int  int"

lift_definition int_of_uint32 :: "uint32  int" is "uint" .
lift_definition nat_of_uint32 :: "uint32  nat" is "unat" .

definition integer_of_uint32 :: "uint32  integer"
where "integer_of_uint32 = integer_of_int o int_of_uint32"

text ‹Use pretty numerals from integer for pretty printing›

context includes integer.lifting begin

lift_definition Uint32 :: "integer  uint32" is "word_of_int" .

lemma Rep_uint32_numeral [simp]: "Rep_uint32 (numeral n) = numeral n"
by(induction n)(simp_all add: one_uint32_def Abs_uint32_inverse numeral.simps plus_uint32_def)

lemma numeral_uint32_transfer [transfer_rule]:
  "(rel_fun (=) cr_uint32) numeral numeral"
by(auto simp add: cr_uint32_def)

lemma numeral_uint32 [code_unfold]: "numeral n = Uint32 (numeral n)"
by transfer simp

lemma Rep_uint32_neg_numeral [simp]: "Rep_uint32 (- numeral n) = - numeral n"
by(simp only: uminus_uint32_def)(simp add: Abs_uint32_inverse)

lemma neg_numeral_uint32 [code_unfold]: "- numeral n = Uint32 (- numeral n)"
by transfer(simp add: cr_uint32_def)

end

lemma Abs_uint32_numeral [code_post]: "Abs_uint32 (numeral n) = numeral n"
by(induction n)(simp_all add: one_uint32_def numeral.simps plus_uint32_def Abs_uint32_inverse)

lemma Abs_uint32_0 [code_post]: "Abs_uint32 0 = 0"
by(simp add: zero_uint32_def)

lemma Abs_uint32_1 [code_post]: "Abs_uint32 1 = 1"
by(simp add: one_uint32_def)

section ‹Code setup›

code_printing code_module Uint32  (SML)
‹(* Test that words can handle numbers between 0 and 31 *)
val _ = if 5 <= Word.wordSize then () else raise (Fail ("wordSize less than 5"));

structure Uint32 : sig
  val set_bit : Word32.word -> IntInf.int -> bool -> Word32.word
  val shiftl : Word32.word -> IntInf.int -> Word32.word
  val shiftr : Word32.word -> IntInf.int -> Word32.word
  val shiftr_signed : Word32.word -> IntInf.int -> Word32.word
  val test_bit : Word32.word -> IntInf.int -> bool
end = struct

fun set_bit x n b =
  let val mask = Word32.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))
  in if b then Word32.orb (x, mask)
     else Word32.andb (x, Word32.notb mask)
  end

fun shiftl x n =
  Word32.<< (x, Word.fromLargeInt (IntInf.toLarge n))

fun shiftr x n =
  Word32.>> (x, Word.fromLargeInt (IntInf.toLarge n))

fun shiftr_signed x n =
  Word32.~>> (x, Word.fromLargeInt (IntInf.toLarge n))

fun test_bit x n =
  Word32.andb (x, Word32.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))) <> Word32.fromInt 0

end; (* struct Uint32 *)›
code_reserved SML Uint32

code_printing code_module Uint32  (Haskell)
 ‹module Uint32(Int32, Word32) where

  import Data.Int(Int32)
  import Data.Word(Word32)›
code_reserved Haskell Uint32

text ‹
  OCaml and Scala provide only signed 32bit numbers, so we use these and 
  implement sign-sensitive operations like comparisons manually.
›
code_printing code_module "Uint32"  (OCaml)
‹module Uint32 : sig
  val less : int32 -> int32 -> bool
  val less_eq : int32 -> int32 -> bool
  val set_bit : int32 -> Z.t -> bool -> int32
  val shiftl : int32 -> Z.t -> int32
  val shiftr : int32 -> Z.t -> int32
  val shiftr_signed : int32 -> Z.t -> int32
  val test_bit : int32 -> Z.t -> bool
end = struct

(* negative numbers have their highest bit set, 
   so they are greater than positive ones *)
let less x y =
  if Int32.compare x Int32.zero < 0 then
    Int32.compare y Int32.zero < 0 && Int32.compare x y < 0
  else Int32.compare y Int32.zero < 0 || Int32.compare x y < 0;;

let less_eq x y =
  if Int32.compare x Int32.zero < 0 then
    Int32.compare y Int32.zero < 0 && Int32.compare x y <= 0
  else Int32.compare y Int32.zero < 0 || Int32.compare x y <= 0;;

let set_bit x n b =
  let mask = Int32.shift_left Int32.one (Z.to_int n)
  in if b then Int32.logor x mask
     else Int32.logand x (Int32.lognot mask);;

let shiftl x n = Int32.shift_left x (Z.to_int n);;

let shiftr x n = Int32.shift_right_logical x (Z.to_int n);;

let shiftr_signed x n = Int32.shift_right x (Z.to_int n);;

let test_bit x n =
  Int32.compare 
    (Int32.logand x (Int32.shift_left Int32.one (Z.to_int n)))
    Int32.zero
  <> 0;;

end;; (*struct Uint32*)›
code_reserved OCaml Uint32

code_printing code_module Uint32  (Scala)
‹object Uint32 {

def less(x: Int, y: Int) : Boolean =
  if (x < 0) y < 0 && x < y
  else y < 0 || x < y

def less_eq(x: Int, y: Int) : Boolean =
  if (x < 0) y < 0 && x <= y
  else y < 0 || x <= y

def set_bit(x: Int, n: BigInt, b: Boolean) : Int =
  if (b)
    x | (1 << n.intValue)
  else
    x & (1 << n.intValue).unary_~

def shiftl(x: Int, n: BigInt) : Int = x << n.intValue

def shiftr(x: Int, n: BigInt) : Int = x >>> n.intValue

def shiftr_signed(x: Int, n: BigInt) : Int = x >> n.intValue

def test_bit(x: Int, n: BigInt) : Boolean =
  (x & (1 << n.intValue)) != 0

} /* object Uint32 */›
code_reserved Scala Uint32

text ‹
  OCaml's conversion from Big\_int to int32 demands that the value fits int a signed 32-bit integer.
  The following justifies the implementation.
›

definition Uint32_signed :: "integer  uint32" 
where "Uint32_signed i = (if i < -(0x80000000)  i  0x80000000 then undefined Uint32 i else Uint32 i)"

lemma Uint32_code [code]:
  "Uint32 i = 
  (let i' = i AND 0xFFFFFFFF
   in if bit i' 31 then Uint32_signed (i' - 0x100000000) else Uint32_signed i')"
  including undefined_transfer integer.lifting unfolding Uint32_signed_def
  apply transfer
  apply (subst word_of_int_via_signed)
     apply (auto simp add: shiftl_eq_push_bit push_bit_of_1 mask_eq_exp_minus_1 word_of_int_via_signed cong del: if_cong)
  done

lemma Uint32_signed_code [code abstract]:
  "Rep_uint32 (Uint32_signed i) = 
  (if i < -(0x80000000)  i  0x80000000 then Rep_uint32 (undefined Uint32 i) else word_of_int (int_of_integer_symbolic i))"
unfolding Uint32_signed_def Uint32_def int_of_integer_symbolic_def word_of_integer_def
by(simp add: Abs_uint32_inverse)

text ‹
  Avoid @{term Abs_uint32} in generated code, use @{term Rep_uint32'} instead. 
  The symbolic implementations for code\_simp use @{term Rep_uint32}.

  The new destructor @{term Rep_uint32'} is executable.
  As the simplifier is given the [code abstract] equations literally, 
  we cannot implement @{term Rep_uint32} directly, because that makes code\_simp loop.

  If code generation raises Match, some equation probably contains @{term Rep_uint32} 
  ([code abstract] equations for @{typ uint32} may use @{term Rep_uint32} because
  these instances will be folded away.)

  To convert @{typ "32 word"} values into @{typ uint32}, use @{term "Abs_uint32'"}.
›

definition Rep_uint32' where [simp]: "Rep_uint32' = Rep_uint32"

lemma Rep_uint32'_transfer [transfer_rule]:
  "rel_fun cr_uint32 (=) (λx. x) Rep_uint32'"
unfolding Rep_uint32'_def by(rule uint32.rep_transfer)

lemma Rep_uint32'_code [code]: "Rep_uint32' x = (BITS n. bit x n)"
  by transfer (simp add: set_bits_bit_eq) 

lift_definition Abs_uint32' :: "32 word  uint32" is "λx :: 32 word. x" .

lemma Abs_uint32'_code [code]:
  "Abs_uint32' x = Uint32 (integer_of_int (uint x))"
including integer.lifting by transfer simp

declare [[code drop: "term_of_class.term_of :: uint32  _"]]

lemma term_of_uint32_code [code]:
  defines "TR  typerep.Typerep" and "bit0  STR ''Numeral_Type.bit0''" 
  shows
  "term_of_class.term_of x = 
   Code_Evaluation.App (Code_Evaluation.Const (STR ''Uint32.uint32.Abs_uint32'') (TR (STR ''fun'') [TR (STR ''Word.word'') [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR (STR ''Numeral_Type.num1'') []]]]]]], TR (STR ''Uint32.uint32'') []]))
       (term_of_class.term_of (Rep_uint32' x))"
by(simp add: term_of_anything)

code_printing
  type_constructor uint32 
  (SML) "Word32.word" and
  (Haskell) "Uint32.Word32" and
  (OCaml) "int32" and
  (Scala) "Int" and
  (Eval) "Word32.word"
| constant Uint32 
  (SML) "Word32.fromLargeInt (IntInf.toLarge _)" and
  (Haskell) "(Prelude.fromInteger _ :: Uint32.Word32)" and
  (Haskell_Quickcheck) "(Prelude.fromInteger (Prelude.toInteger _) :: Uint32.Word32)" and
  (Scala) "_.intValue"
| constant Uint32_signed 
  (OCaml) "Z.to'_int32"
| constant "0 :: uint32" 
  (SML) "(Word32.fromInt 0)" and
  (Haskell) "(0 :: Uint32.Word32)" and
  (OCaml) "Int32.zero" and
  (Scala) "0"
| constant "1 :: uint32" 
  (SML) "(Word32.fromInt 1)" and
  (Haskell) "(1 :: Uint32.Word32)" and
  (OCaml) "Int32.one" and
  (Scala) "1"
| constant "plus :: uint32  _ " 
  (SML) "Word32.+ ((_), (_))" and
  (Haskell) infixl 6 "+" and
  (OCaml) "Int32.add" and
  (Scala) infixl 7 "+"
| constant "uminus :: uint32  _" 
  (SML) "Word32.~" and
  (Haskell) "negate" and
  (OCaml) "Int32.neg" and
  (Scala) "!(- _)"
| constant "minus :: uint32  _" 
  (SML) "Word32.- ((_), (_))" and
  (Haskell) infixl 6 "-" and
  (OCaml) "Int32.sub" and
  (Scala) infixl 7 "-"
| constant "times :: uint32  _  _" 
  (SML) "Word32.* ((_), (_))" and
  (Haskell) infixl 7 "*" and
  (OCaml) "Int32.mul" and
  (Scala) infixl 8 "*"
| constant "HOL.equal :: uint32  _  bool" 
  (SML) "!((_ : Word32.word) = _)" and
  (Haskell) infix 4 "==" and
  (OCaml) "(Int32.compare _ _ = 0)" and
  (Scala) infixl 5 "=="
| class_instance uint32 :: equal 
  (Haskell) -
| constant "less_eq :: uint32  _  bool" 
  (SML) "Word32.<= ((_), (_))" and
  (Haskell) infix 4 "<=" and
  (OCaml) "Uint32.less'_eq" and
  (Scala) "Uint32.less'_eq"
| constant "less :: uint32  _  bool" 
  (SML) "Word32.< ((_), (_))" and
  (Haskell) infix 4 "<" and
  (OCaml) "Uint32.less" and
  (Scala) "Uint32.less"
| constant "NOT :: uint32  _" 
  (SML) "Word32.notb" and
  (Haskell) "Data'_Bits.complement" and
  (OCaml) "Int32.lognot" and
  (Scala) "_.unary'_~"
| constant "(AND) :: uint32  _" 
  (SML) "Word32.andb ((_),/ (_))" and
  (Haskell) infixl 7 "Data_Bits..&." and
  (OCaml) "Int32.logand" and
  (Scala) infixl 3 "&"
| constant "(OR) :: uint32  _" 
  (SML) "Word32.orb ((_),/ (_))" and
  (Haskell) infixl 5 "Data_Bits..|." and
  (OCaml) "Int32.logor" and
  (Scala) infixl 1 "|"
| constant "(XOR) :: uint32  _" 
  (SML) "Word32.xorb ((_),/ (_))" and
  (Haskell) "Data'_Bits.xor" and
  (OCaml) "Int32.logxor" and
  (Scala) infixl 2 "^"

definition uint32_divmod :: "uint32  uint32  uint32 × uint32" where
  "uint32_divmod x y = 
  (if y = 0 then (undefined ((div) :: uint32  _) x (0 :: uint32), undefined ((mod) :: uint32  _) x (0 :: uint32)) 
  else (x div y, x mod y))"

definition uint32_div :: "uint32  uint32  uint32" 
where "uint32_div x y = fst (uint32_divmod x y)"

definition uint32_mod :: "uint32  uint32  uint32" 
where "uint32_mod x y = snd (uint32_divmod x y)"

lemma div_uint32_code [code]: "x div y = (if y = 0 then 0 else uint32_div x y)"
including undefined_transfer unfolding uint32_divmod_def uint32_div_def
by transfer (simp add: word_div_def)

lemma mod_uint32_code [code]: "x mod y = (if y = 0 then x else uint32_mod x y)"
including undefined_transfer unfolding uint32_mod_def uint32_divmod_def
by transfer (simp add: word_mod_def)

definition uint32_sdiv :: "uint32  uint32  uint32"
where [code del]:
  "uint32_sdiv x y =
   (if y = 0 then undefined ((div) :: uint32  _) x (0 :: uint32)
    else Abs_uint32 (Rep_uint32 x sdiv Rep_uint32 y))"

definition div0_uint32 :: "uint32  uint32"
where [code del]: "div0_uint32 x = undefined ((div) :: uint32  _) x (0 :: uint32)"
declare [[code abort: div0_uint32]]

definition mod0_uint32 :: "uint32  uint32"
where [code del]: "mod0_uint32 x = undefined ((mod) :: uint32  _) x (0 :: uint32)"
declare [[code abort: mod0_uint32]]

lemma uint32_divmod_code [code]:
  "uint32_divmod x y =
  (if 0x80000000  y then if x < y then (0, x) else (1, x - y)
   else if y = 0 then (div0_uint32 x, mod0_uint32 x)
   else let q = (uint32_sdiv (drop_bit 1 x) y) << 1;
            r = x - q * y
        in if r  y then (q + 1, r - y) else (q, r))"
  including undefined_transfer unfolding uint32_divmod_def uint32_sdiv_def div0_uint32_def mod0_uint32_def
  by transfer (simp add: divmod_via_sdivmod shiftr_eq_drop_bit shiftl_eq_push_bit ac_simps)

lemma uint32_sdiv_code [code abstract]:
  "Rep_uint32 (uint32_sdiv x y) =
   (if y = 0 then Rep_uint32 (undefined ((div) :: uint32  _) x (0 :: uint32))
    else Rep_uint32 x sdiv Rep_uint32 y)"
unfolding uint32_sdiv_def by(simp add: Abs_uint32_inverse)

text ‹
  Note that we only need a translation for signed division, but not for the remainder
  because @{thm uint32_divmod_code} computes both with division only.
›

code_printing
  constant uint32_div 
  (SML) "Word32.div ((_), (_))" and
  (Haskell) "Prelude.div"
| constant uint32_mod 
  (SML) "Word32.mod ((_), (_))" and
  (Haskell) "Prelude.mod"
| constant uint32_divmod 
  (Haskell) "divmod"
| constant uint32_sdiv 
  (OCaml) "Int32.div" and
  (Scala) "_ '/ _"

definition uint32_test_bit :: "uint32  integer  bool"
where [code del]:
  "uint32_test_bit x n =
  (if n < 0  31 < n then undefined (bit :: uint32  _) x n
   else bit x (nat_of_integer n))"

lemma test_bit_uint32_code [code]:
  "bit x n  n < 32  uint32_test_bit x (integer_of_nat n)"
  including undefined_transfer integer.lifting unfolding uint32_test_bit_def
  by (transfer, simp, transfer, simp)

lemma uint32_test_bit_code [code]:
  "uint32_test_bit w n =
  (if n < 0  31 < n then undefined (bit :: uint32  _) w n else bit (Rep_uint32 w) (nat_of_integer n))"
  unfolding uint32_test_bit_def by(simp add: bit_uint32.rep_eq)

code_printing constant uint32_test_bit 
  (SML) "Uint32.test'_bit" and
  (Haskell) "Data'_Bits.testBitBounded" and
  (OCaml) "Uint32.test'_bit" and
  (Scala) "Uint32.test'_bit" and
  (Eval) "(fn w => fn n => if n < 0 orelse 32 <= n then raise (Fail \"argument to uint32'_test'_bit out of bounds\") else Uint32.test'_bit w n)"

definition uint32_set_bit :: "uint32  integer  bool  uint32"
where [code del]:
  "uint32_set_bit x n b =
  (if n < 0  31 < n then undefined (set_bit :: uint32  _) x n b
   else set_bit x (nat_of_integer n) b)"

lemma set_bit_uint32_code [code]:
  "set_bit x n b = (if n < 32 then uint32_set_bit x (integer_of_nat n) b else x)"
including undefined_transfer integer.lifting unfolding uint32_set_bit_def
by(transfer)(auto cong: conj_cong simp add: not_less set_bit_beyond word_size)

lemma uint32_set_bit_code [code abstract]:
  "Rep_uint32 (uint32_set_bit w n b) = 
  (if n < 0  31 < n then Rep_uint32 (undefined (set_bit :: uint32  _) w n b)
   else set_bit (Rep_uint32 w) (nat_of_integer n) b)"
including undefined_transfer unfolding uint32_set_bit_def by transfer simp

code_printing constant uint32_set_bit 
  (SML) "Uint32.set'_bit" and
  (Haskell) "Data'_Bits.setBitBounded" and
  (OCaml) "Uint32.set'_bit" and
  (Scala) "Uint32.set'_bit" and
  (Eval) "(fn w => fn n => fn b => if n < 0 orelse 32 <= n then raise (Fail \"argument to uint32'_set'_bit out of bounds\") else Uint32.set'_bit x n b)"

lift_definition uint32_set_bits :: "(nat  bool)  uint32  nat  uint32" is set_bits_aux .

lemma uint32_set_bits_code [code]:
  "uint32_set_bits f w n =
  (if n = 0 then w 
   else let n' = n - 1 in uint32_set_bits f (push_bit 1 w OR (if f n' then 1 else 0)) n')"
  apply (transfer fixing: n)
  apply (cases n)
   apply (simp_all add: shiftl_eq_push_bit)
  done

lemma set_bits_uint32 [code]:
  "(BITS n. f n) = uint32_set_bits f 0 32"
by transfer(simp add: set_bits_conv_set_bits_aux)


lemma lsb_code [code]: fixes x :: uint32 shows "lsb x  bit x 0"
  by transfer (simp add: lsb_word_eq)


definition uint32_shiftl :: "uint32  integer  uint32"
where [code del]:
  "uint32_shiftl x n = (if n < 0  32  n then undefined (push_bit :: nat  uint32  _) x n else push_bit (nat_of_integer n) x)"

lemma shiftl_uint32_code [code]: "push_bit n x = (if n < 32 then uint32_shiftl x (integer_of_nat n) else 0)"
  including undefined_transfer integer.lifting unfolding uint32_shiftl_def
  by transfer simp

lemma uint32_shiftl_code [code abstract]:
  "Rep_uint32 (uint32_shiftl w n) =
  (if n < 0  32  n then Rep_uint32 (undefined (push_bit :: nat  uint32  _) w n) else push_bit (nat_of_integer n) (Rep_uint32 w))"
  including undefined_transfer unfolding uint32_shiftl_def
  by transfer (simp add: shiftl_eq_push_bit)

code_printing constant uint32_shiftl 
  (SML) "Uint32.shiftl" and
  (Haskell) "Data'_Bits.shiftlBounded" and
  (OCaml) "Uint32.shiftl" and
  (Scala) "Uint32.shiftl" and
  (Eval) "(fn x => fn i => if i < 0 orelse i >= 32 then raise Fail \"argument to uint32'_shiftl out of bounds\" else Uint32.shiftl x i)"

definition uint32_shiftr :: "uint32  integer  uint32"
where [code del]:
  "uint32_shiftr x n = (if n < 0  32  n then undefined (drop_bit :: nat  uint32  _) x n else drop_bit (nat_of_integer n) x)"

lemma shiftr_uint32_code [code]: "drop_bit n x = (if n < 32 then uint32_shiftr x (integer_of_nat n) else 0)"
  including undefined_transfer integer.lifting unfolding uint32_shiftr_def
  by transfer simp

lemma uint32_shiftr_code [code abstract]:
  "Rep_uint32 (uint32_shiftr w n) =
  (if n < 0  32  n then Rep_uint32 (undefined (drop_bit :: nat  uint32  _) w n) else drop_bit (nat_of_integer n) (Rep_uint32 w))"
  including undefined_transfer unfolding uint32_shiftr_def by transfer simp

code_printing constant uint32_shiftr 
  (SML) "Uint32.shiftr" and
  (Haskell) "Data'_Bits.shiftrBounded" and
  (OCaml) "Uint32.shiftr" and
  (Scala) "Uint32.shiftr" and
  (Eval) "(fn x => fn i => if i < 0 orelse i >= 32 then raise Fail \"argument to uint32'_shiftr out of bounds\" else Uint32.shiftr x i)"

definition uint32_sshiftr :: "uint32  integer  uint32"
where [code del]:
  "uint32_sshiftr x n =
  (if n < 0  32  n then undefined sshiftr_uint32 x n else sshiftr_uint32 x (nat_of_integer n))"

lemma sshiftr_uint32_code [code]:
  "x >>> n = 
  (if n < 32 then uint32_sshiftr x (integer_of_nat n) else if bit x 31 then - 1 else 0)"
  including undefined_transfer integer.lifting unfolding uint32_sshiftr_def
  by transfer (simp add: not_less signed_drop_bit_beyond)

lemma uint32_sshiftr_code [code abstract]:
  "Rep_uint32 (uint32_sshiftr w n) =
  (if n < 0  32  n then Rep_uint32 (undefined sshiftr_uint32 w n) else signed_drop_bit (nat_of_integer n) (Rep_uint32 w))"
including undefined_transfer unfolding uint32_sshiftr_def by transfer simp

code_printing constant uint32_sshiftr 
  (SML) "Uint32.shiftr'_signed" and
  (Haskell) 
    "(Prelude.fromInteger (Prelude.toInteger (Data'_Bits.shiftrBounded (Prelude.fromInteger (Prelude.toInteger _) :: Uint32.Int32) _)) :: Uint32.Word32)" and
  (OCaml) "Uint32.shiftr'_signed" and
  (Scala) "Uint32.shiftr'_signed" and
  (Eval) "(fn x => fn i => if i < 0 orelse i >= 32 then raise Fail \"argument to uint32'_shiftr'_signed out of bounds\" else Uint32.shiftr'_signed x i)"

lemma uint32_msb_test_bit: "msb x  bit (x :: uint32) 31"
  by transfer (simp add: msb_word_iff_bit)

lemma msb_uint32_code [code]: "msb x  uint32_test_bit x 31"
  by (simp add: uint32_test_bit_def uint32_msb_test_bit)

lemma uint32_of_int_code [code]: "uint32_of_int i = Uint32 (integer_of_int i)"
including integer.lifting by transfer simp

lemma int_of_uint32_code [code]:
  "int_of_uint32 x = int_of_integer (integer_of_uint32 x)"
by(simp add: integer_of_uint32_def)

lemma nat_of_uint32_code [code]:
  "nat_of_uint32 x = nat_of_integer (integer_of_uint32 x)"
unfolding integer_of_uint32_def including integer.lifting by transfer simp

definition integer_of_uint32_signed :: "uint32  integer"
where
  "integer_of_uint32_signed n = (if bit n 31 then undefined integer_of_uint32 n else integer_of_uint32 n)"

lemma integer_of_uint32_signed_code [code]:
  "integer_of_uint32_signed n =
  (if bit n 31 then undefined integer_of_uint32 n else integer_of_int (uint (Rep_uint32' n)))"
unfolding integer_of_uint32_signed_def integer_of_uint32_def
including undefined_transfer by transfer simp

lemma integer_of_uint32_code [code]:
  "integer_of_uint32 n =
  (if bit n 31 then integer_of_uint32_signed (n AND 0x7FFFFFFF) OR 0x80000000 else integer_of_uint32_signed n)"
proof -
  have (0x7FFFFFFF :: uint32) = mask 31
    by (simp add: mask_eq_exp_minus_1)
  then have *: n AND 0x7FFFFFFF = take_bit 31 n
    by (simp add: take_bit_eq_mask)
  have **: (0x80000000 :: int) = 2 ^ 31
    by simp
  show ?thesis
    unfolding integer_of_uint32_def integer_of_uint32_signed_def o_def *
    including undefined_transfer integer.lifting
    apply transfer
    apply (rule bit_eqI)
    apply (simp add: test_bit_eq_bit bit_or_iff bit_take_bit_iff bit_uint_iff)
    apply (simp only: bit_exp_iff bit_or_iff **)
    apply auto
    done
qed

code_printing
  constant "integer_of_uint32" 
  (SML) "IntInf.fromLarge (Word32.toLargeInt _) : IntInf.int" and
  (Haskell) "Prelude.toInteger"
| constant "integer_of_uint32_signed" 
  (OCaml) "Z.of'_int32" and
  (Scala) "BigInt"

section ‹Quickcheck setup›

definition uint32_of_natural :: "natural  uint32"
where "uint32_of_natural x  Uint32 (integer_of_natural x)"

instantiation uint32 :: "{random, exhaustive, full_exhaustive}" begin
definition "random_uint32  qc_random_cnv uint32_of_natural"
definition "exhaustive_uint32  qc_exhaustive_cnv uint32_of_natural"
definition "full_exhaustive_uint32  qc_full_exhaustive_cnv uint32_of_natural"
instance ..
end

instantiation uint32 :: narrowing begin

interpretation quickcheck_narrowing_samples
  "λi. let x = Uint32 i in (x, 0xFFFFFFFF - x)" "0"
  "Typerep.Typerep (STR ''Uint32.uint32'') []" .

definition "narrowing_uint32 d = qc_narrowing_drawn_from (narrowing_samples d) d"
declare [[code drop: "partial_term_of :: uint32 itself  _"]]
lemmas partial_term_of_uint32 [code] = partial_term_of_code

instance ..
end

no_notation sshiftr_uint32 (infixl ">>>" 55)

end

Theory Uint16

(*  Title:      Uint16.thy
    Author:     Andreas Lochbihler, ETH Zurich
*)

chapter ‹Unsigned words of 16 bits›

theory Uint16 imports
  Code_Target_Word_Base
begin

text ‹
  Restriction for ML code generation:
  This theory assumes that the ML system provides a Word16
  implementation (mlton does, but PolyML 5.5 does not).
  Therefore, the code setup lives in the target SML_word›
  rather than SML›.  This ensures that code generation still
  works as long as uint16› is not involved.
  For the target SML› itself, no special code generation 
  for this type is set up. Nevertheless, it should work by emulation via @{typ "16 word"} 
  if the theory Code_Target_Bits_Int› is imported.

  Restriction for OCaml code generation:
  OCaml does not provide an int16 type, so no special code generation 
  for this type is set up.
›

declare prod.Quotient[transfer_rule]

section ‹Type definition and primitive operations›

typedef uint16 = "UNIV :: 16 word set" ..

setup_lifting type_definition_uint16

text ‹Use an abstract type for code generation to disable pattern matching on @{term Abs_uint16}.›
declare Rep_uint16_inverse[code abstype]

declare Quotient_uint16[transfer_rule]

instantiation uint16 :: comm_ring_1
begin
lift_definition zero_uint16 :: uint16 is "0 :: 16 word" .
lift_definition one_uint16 :: uint16 is "1" .
lift_definition plus_uint16 :: "uint16  uint16  uint16" is "(+) :: 16 word  _" .
lift_definition minus_uint16 :: "uint16  uint16  uint16" is "(-)" .
lift_definition uminus_uint16 :: "uint16  uint16" is uminus .
lift_definition times_uint16 :: "uint16  uint16  uint16" is "(*)" .
instance by (standard; transfer) (simp_all add: algebra_simps)
end

instantiation uint16 :: semiring_modulo
begin
lift_definition divide_uint16 :: "uint16  uint16  uint16" is "(div)" .
lift_definition modulo_uint16 :: "uint16  uint16  uint16" is "(mod)" .
instance by (standard; transfer) (fact word_mod_div_equality)
end

instantiation uint16 :: linorder begin
lift_definition less_uint16 :: "uint16  uint16  bool" is "(<)" .
lift_definition less_eq_uint16 :: "uint16  uint16  bool" is "(≤)" .
instance by (standard; transfer) (simp_all add: less_le_not_le linear)
end

lemmas [code] = less_uint16.rep_eq less_eq_uint16.rep_eq

context
  includes lifting_syntax
  notes
    transfer_rule_of_bool [transfer_rule]
    transfer_rule_numeral [transfer_rule]
begin

lemma [transfer_rule]:
  "((=) ===> cr_uint16) of_bool of_bool"
  by transfer_prover

lemma transfer_rule_numeral_uint [transfer_rule]:
  "((=) ===> cr_uint16) numeral numeral"
  by transfer_prover

lemma [transfer_rule]:
  (cr_uint16 ===> (⟷)) even ((dvd) 2 :: uint16  bool)
  by (unfold dvd_def) transfer_prover

end

instantiation uint16 :: semiring_bits
begin

lift_definition bit_uint16 :: ‹uint16  nat  bool› is bit .

instance
  by (standard; transfer)
    (fact bit_iff_odd even_iff_mod_2_eq_zero odd_iff_mod_2_eq_one odd_one bits_induct
       bits_div_0 bits_div_by_1 bits_mod_div_trivial even_succ_div_2
       even_mask_div_iff exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq
       div_exp_mod_exp_eq even_mult_exp_div_exp_iff)+

end

instantiation uint16 :: semiring_bit_shifts
begin
lift_definition push_bit_uint16 :: ‹nat  uint16  uint16› is push_bit .
lift_definition drop_bit_uint16 :: ‹nat  uint16  uint16› is drop_bit .
lift_definition take_bit_uint16 :: ‹nat  uint16  uint16› is take_bit .
instance by (standard; transfer)
  (fact push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod)+
end

instantiation uint16 :: ring_bit_operations
begin
lift_definition not_uint16 :: ‹uint16  uint16› is NOT .
lift_definition and_uint16 :: ‹uint16  uint16  uint16› is (AND) .
lift_definition or_uint16 :: ‹uint16  uint16  uint16› is (OR) .
lift_definition xor_uint16 :: ‹uint16  uint16  uint16› is (XOR) .
lift_definition mask_uint16 :: ‹nat  uint16› is mask .
instance by (standard; transfer)
  (simp_all add: bit_and_iff bit_or_iff bit_xor_iff bit_not_iff minus_eq_not_minus_1 mask_eq_decr_exp)
end

lemma [code]:
  ‹take_bit n a = a AND mask n for a :: uint16
  by (fact take_bit_eq_mask)

lemma [code]:
  ‹mask (Suc n) = push_bit n (1 :: uint16) OR mask n
  ‹mask 0 = (0 :: uint16)
  by (simp_all add: mask_Suc_exp push_bit_of_1)

instance uint16 :: semiring_bit_syntax ..

context
  includes lifting_syntax
begin

lemma test_bit_uint16_transfer [transfer_rule]:
  (cr_uint16 ===> (=)) bit (!!)
  unfolding test_bit_eq_bit by transfer_prover

lemma shiftl_uint16_transfer [transfer_rule]:
  (cr_uint16 ===> (=) ===> cr_uint16) (λk n. push_bit n k) (<<)
  unfolding shiftl_eq_push_bit by transfer_prover

lemma shiftr_uint16_transfer [transfer_rule]:
  (cr_uint16 ===> (=) ===> cr_uint16) (λk n. drop_bit n k) (>>)
  unfolding shiftr_eq_drop_bit by transfer_prover

end

instantiation uint16 :: lsb
begin
lift_definition lsb_uint16 :: ‹uint16  bool› is lsb .
instance by (standard; transfer)
  (fact lsb_odd)
end

instantiation uint16 :: msb
begin
lift_definition msb_uint16 :: ‹uint16  bool› is msb .
instance ..
end

instantiation uint16 :: set_bit
begin
lift_definition set_bit_uint16 :: ‹uint16  nat  bool  uint16› is set_bit .
instance
  apply standard
  apply transfer
  apply (simp add: bit_simps)
  done
end

instantiation uint16 :: bit_comprehension begin
lift_definition set_bits_uint16 :: "(nat  bool)  uint16" is "set_bits" .
instance by (standard; transfer) (fact set_bits_bit_eq)
end

lemmas [code] = bit_uint16.rep_eq lsb_uint16.rep_eq msb_uint16.rep_eq

instantiation uint16 :: equal begin
lift_definition equal_uint16 :: "uint16  uint16  bool" is "equal_class.equal" .
instance by standard (transfer, simp add: equal_eq)
end

lemmas [code] = equal_uint16.rep_eq

instantiation uint16 :: size begin
lift_definition size_uint16 :: "uint16  nat" is "size" .
instance ..
end

lemmas [code] = size_uint16.rep_eq

lift_definition sshiftr_uint16 :: "uint16  nat  uint16" (infixl ">>>" 55) is λw n. signed_drop_bit n w .

lift_definition uint16_of_int :: "int  uint16" is "word_of_int" .

definition uint16_of_nat :: "nat  uint16"
where "uint16_of_nat = uint16_of_int  int"

lift_definition int_of_uint16 :: "uint16  int" is "uint" .
lift_definition nat_of_uint16 :: "uint16  nat" is "unat" .

definition integer_of_uint16 :: "uint16  integer"
where "integer_of_uint16 = integer_of_int o int_of_uint16"

text ‹Use pretty numerals from integer for pretty printing›

context includes integer.lifting begin

lift_definition Uint16 :: "integer  uint16" is "word_of_int" .

lemma Rep_uint16_numeral [simp]: "Rep_uint16 (numeral n) = numeral n"
by(induction n)(simp_all add: one_uint16_def Abs_uint16_inverse numeral.simps plus_uint16_def)

lemma Rep_uint16_neg_numeral [simp]: "Rep_uint16 (- numeral n) = - numeral n"
by(simp only: uminus_uint16_def)(simp add: Abs_uint16_inverse)

lemma numeral_uint16_transfer [transfer_rule]:
  "(rel_fun (=) cr_uint16) numeral numeral"
by(auto simp add: cr_uint16_def)

lemma numeral_uint16 [code_unfold]: "numeral n = Uint16 (numeral n)"
by transfer simp

lemma neg_numeral_uint16 [code_unfold]: "- numeral n = Uint16 (- numeral n)"
by transfer(simp add: cr_uint16_def)

end

lemma Abs_uint16_numeral [code_post]: "Abs_uint16 (numeral n) = numeral n"
by(induction n)(simp_all add: one_uint16_def numeral.simps plus_uint16_def Abs_uint16_inverse)

lemma Abs_uint16_0 [code_post]: "Abs_uint16 0 = 0"
by(simp add: zero_uint16_def)

lemma Abs_uint16_1 [code_post]: "Abs_uint16 1 = 1"
by(simp add: one_uint16_def)

section ‹Code setup›

code_printing code_module Uint16  (SML_word)
‹(* Test that words can handle numbers between 0 and 15 *)
val _ = if 4 <= Word.wordSize then () else raise (Fail ("wordSize less than 4"));

structure Uint16 : sig
  val set_bit : Word16.word -> IntInf.int -> bool -> Word16.word
  val shiftl : Word16.word -> IntInf.int -> Word16.word
  val shiftr : Word16.word -> IntInf.int -> Word16.word
  val shiftr_signed : Word16.word -> IntInf.int -> Word16.word
  val test_bit : Word16.word -> IntInf.int -> bool
end = struct

fun set_bit x n b =
  let val mask = Word16.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))
  in if b then Word16.orb (x, mask)
     else Word16.andb (x, Word16.notb mask)
  end

fun shiftl x n =
  Word16.<< (x, Word.fromLargeInt (IntInf.toLarge n))

fun shiftr x n =
  Word16.>> (x, Word.fromLargeInt (IntInf.toLarge n))

fun shiftr_signed x n =
  Word16.~>> (x, Word.fromLargeInt (IntInf.toLarge n))

fun test_bit x n =
  Word16.andb (x, Word16.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))) <> Word16.fromInt 0

end; (* struct Uint16 *)›
code_reserved SML_word Uint16

code_printing code_module Uint16  (Haskell)
 ‹module Uint16(Int16, Word16) where

  import Data.Int(Int16)
  import Data.Word(Word16)›
code_reserved Haskell Uint16

text ‹Scala provides unsigned 16-bit numbers as Char.›

code_printing code_module Uint16  (Scala)
‹object Uint16 {

def set_bit(x: scala.Char, n: BigInt, b: Boolean) : scala.Char =
  if (b)
    (x | (1.toChar << n.intValue)).toChar
  else
    (x & (1.toChar << n.intValue).unary_~).toChar

def shiftl(x: scala.Char, n: BigInt) : scala.Char = (x << n.intValue).toChar

def shiftr(x: scala.Char, n: BigInt) : scala.Char = (x >>> n.intValue).toChar

def shiftr_signed(x: scala.Char, n: BigInt) : scala.Char = (x.toShort >> n.intValue).toChar

def test_bit(x: scala.Char, n: BigInt) : Boolean = (x & (1.toChar << n.intValue)) != 0

} /* object Uint16 */›
code_reserved Scala Uint16

text ‹
  Avoid @{term Abs_uint16} in generated code, use @{term Rep_uint16'} instead. 
  The symbolic implementations for code\_simp use @{term Rep_uint16}.

  The new destructor @{term Rep_uint16'} is executable.
  As the simplifier is given the [code abstract] equations literally, 
  we cannot implement @{term Rep_uint16} directly, because that makes code\_simp loop.

  If code generation raises Match, some equation probably contains @{term Rep_uint16} 
  ([code abstract] equations for @{typ uint16} may use @{term Rep_uint16} because
  these instances will be folded away.)

  To convert @{typ "16 word"} values into @{typ uint16}, use @{term "Abs_uint16'"}.
›

definition Rep_uint16' where [simp]: "Rep_uint16' = Rep_uint16"

lemma Rep_uint16'_transfer [transfer_rule]:
  "rel_fun cr_uint16 (=) (λx. x) Rep_uint16'"
unfolding Rep_uint16'_def by(rule uint16.rep_transfer)

lemma Rep_uint16'_code [code]: "Rep_uint16' x = (BITS n. bit x n)"
  by transfer (simp add: set_bits_bit_eq)

lift_definition Abs_uint16' :: "16 word  uint16" is "λx :: 16 word. x" .

lemma Abs_uint16'_code [code]:
  "Abs_uint16' x = Uint16 (integer_of_int (uint x))"
including integer.lifting by transfer simp

declare [[code drop: "term_of_class.term_of :: uint16  _"]]

lemma term_of_uint16_code [code]:
  defines "TR  typerep.Typerep" and "bit0  STR ''Numeral_Type.bit0''" shows
  "term_of_class.term_of x = 
   Code_Evaluation.App (Code_Evaluation.Const (STR ''Uint16.uint16.Abs_uint16'') (TR (STR ''fun'') [TR (STR ''Word.word'') [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR (STR ''Numeral_Type.num1'') []]]]]], TR (STR ''Uint16.uint16'') []]))
       (term_of_class.term_of (Rep_uint16' x))"
by(simp add: term_of_anything)

lemma Uin16_code [code abstract]: "Rep_uint16 (Uint16 i) = word_of_int (int_of_integer_symbolic i)"
unfolding Uint16_def int_of_integer_symbolic_def by(simp add: Abs_uint16_inverse)

code_printing
  type_constructor uint16 
  (SML_word) "Word16.word" and
  (Haskell) "Uint16.Word16" and
  (Scala) "scala.Char"
| constant Uint16 
  (SML_word) "Word16.fromLargeInt (IntInf.toLarge _)" and
  (Haskell) "(Prelude.fromInteger _ :: Uint16.Word16)" and
  (Haskell_Quickcheck) "(Prelude.fromInteger (Prelude.toInteger _) :: Uint16.Word16)" and
  (Scala) "_.charValue"
| constant "0 :: uint16" 
  (SML_word) "(Word16.fromInt 0)" and
  (Haskell) "(0 :: Uint16.Word16)" and
  (Scala) "0"
| constant "1 :: uint16" 
  (SML_word) "(Word16.fromInt 1)" and
  (Haskell) "(1 :: Uint16.Word16)" and
  (Scala) "1"
| constant "plus :: uint16  _  _" 
  (SML_word) "Word16.+ ((_), (_))" and
  (Haskell) infixl 6 "+" and
  (Scala) "(_ +/ _).toChar"
| constant "uminus :: uint16  _" 
  (SML_word) "Word16.~" and
  (Haskell) "negate" and
  (Scala) "(- _).toChar"
| constant "minus :: uint16  _" 
  (SML_word) "Word16.- ((_), (_))" and
  (Haskell) infixl 6 "-" and
  (Scala) "(_ -/ _).toChar"
| constant "times :: uint16  _  _" 
  (SML_word) "Word16.* ((_), (_))" and
  (Haskell) infixl 7 "*" and
  (Scala) "(_ */ _).toChar"
| constant "HOL.equal :: uint16  _  bool" 
  (SML_word) "!((_ : Word16.word) = _)" and
  (Haskell) infix 4 "==" and
  (Scala) infixl 5 "=="
| class_instance uint16 :: equal  (Haskell) -
| constant "less_eq :: uint16  _  bool" 
  (SML_word) "Word16.<= ((_), (_))" and
  (Haskell) infix 4 "<=" and
  (Scala) infixl 4 "<="
| constant "less :: uint16  _  bool" 
  (SML_word) "Word16.< ((_), (_))" and
  (Haskell) infix 4 "<" and
  (Scala) infixl 4 "<"
| constant "NOT :: uint16  _" 
  (SML_word) "Word16.notb" and
  (Haskell) "Data'_Bits.complement" and
  (Scala) "_.unary'_~.toChar"
| constant "(AND) :: uint16  _" 
  (SML_word) "Word16.andb ((_),/ (_))" and
  (Haskell) infixl 7 "Data_Bits..&." and
  (Scala) "(_ & _).toChar"
| constant "(OR) :: uint16  _" 
  (SML_word) "Word16.orb ((_),/ (_))" and
  (Haskell) infixl 5 "Data_Bits..|." and
  (Scala) "(_ | _).toChar"
| constant "(XOR) :: uint16  _" 
  (SML_word) "Word16.xorb ((_),/ (_))" and
  (Haskell) "Data'_Bits.xor" and
  (Scala) "(_ ^ _).toChar"

definition uint16_div :: "uint16  uint16  uint16" 
where "uint16_div x y = (if y = 0 then undefined ((div) :: uint16  _) x (0 :: uint16) else x div y)"

definition uint16_mod :: "uint16  uint16  uint16" 
where "uint16_mod x y = (if y = 0 then undefined ((mod) :: uint16  _) x (0 :: uint16) else x mod y)"

context includes undefined_transfer begin

lemma div_uint16_code [code]: "x div y = (if y = 0 then 0 else uint16_div x y)"
unfolding uint16_div_def by transfer (simp add: word_div_def)

lemma mod_uint16_code [code]: "x mod y = (if y = 0 then x else uint16_mod x y)"
unfolding uint16_mod_def by transfer (simp add: word_mod_def)

lemma uint16_div_code [code abstract]:
  "Rep_uint16 (uint16_div x y) =
  (if y = 0 then Rep_uint16 (undefined ((div) :: uint16  _) x (0 :: uint16)) else Rep_uint16 x div Rep_uint16 y)"
unfolding uint16_div_def by transfer simp

lemma uint16_mod_code [code abstract]:
  "Rep_uint16 (uint16_mod x y) =
  (if y = 0 then Rep_uint16 (undefined ((mod) :: uint16  _) x (0 :: uint16)) else Rep_uint16 x mod Rep_uint16 y)"
unfolding uint16_mod_def by transfer simp

end

code_printing constant uint16_div 
  (SML_word) "Word16.div ((_), (_))" and
  (Haskell) "Prelude.div" and
  (Scala) "(_ '/ _).toChar"
| constant uint16_mod 
  (SML_word) "Word16.mod ((_), (_))" and
  (Haskell) "Prelude.mod" and
  (Scala) "(_ % _).toChar"

definition uint16_test_bit :: "uint16  integer  bool"
where [code del]:
  "uint16_test_bit x n =
  (if n < 0  15 < n then undefined (bit :: uint16  _) x n
   else bit x (nat_of_integer n))"

lemma test_bit_uint16_code [code]:
  "bit x n  n < 16  uint16_test_bit x (integer_of_nat n)"
  including undefined_transfer integer.lifting unfolding uint16_test_bit_def
  by (transfer, simp, transfer, simp)

lemma uint16_test_bit_code [code]:
  "uint16_test_bit w n =
  (if n < 0  15 < n then undefined (bit :: uint16  _) w n else bit (Rep_uint16 w) (nat_of_integer n))"
  unfolding uint16_test_bit_def by (simp add: bit_uint16.rep_eq)

code_printing constant uint16_test_bit 
  (SML_word) "Uint16.test'_bit" and
  (Haskell) "Data'_Bits.testBitBounded" and
  (Scala) "Uint16.test'_bit"

definition uint16_set_bit :: "uint16  integer  bool  uint16"
where [code del]:
  "uint16_set_bit x n b =
  (if n < 0  15 < n then undefined (set_bit :: uint16  _) x n b
   else set_bit x (nat_of_integer n) b)"

lemma set_bit_uint16_code [code]:
  "set_bit x n b = (if n < 16 then uint16_set_bit x (integer_of_nat n) b else x)"
including undefined_transfer integer.lifting unfolding uint16_set_bit_def
by(transfer)(auto cong: conj_cong simp add: not_less set_bit_beyond word_size)

lemma uint16_set_bit_code [code abstract]:
  "Rep_uint16 (uint16_set_bit w n b) = 
  (if n < 0  15 < n then Rep_uint16 (undefined (set_bit :: uint16  _) w n b)
   else set_bit (Rep_uint16 w) (nat_of_integer n) b)"
including undefined_transfer unfolding uint16_set_bit_def by transfer simp

code_printing constant uint16_set_bit 
  (SML_word) "Uint16.set'_bit" and
  (Haskell) "Data'_Bits.setBitBounded" and
  (Scala) "Uint16.set'_bit"

lift_definition uint16_set_bits :: "(nat  bool)  uint16  nat  uint16" is set_bits_aux .

lemma uint16_set_bits_code [code]:
  "uint16_set_bits f w n =
  (if n = 0 then w 
   else let n' = n - 1 in uint16_set_bits f ((push_bit 1 w) OR (if f n' then 1 else 0)) n')"
  apply (transfer fixing: n)
  apply (cases n)
   apply (simp_all add: shiftl_eq_push_bit)
  done

lemma set_bits_uint16 [code]:
  "(BITS n. f n) = uint16_set_bits f 0 16"
by transfer(simp add: set_bits_conv_set_bits_aux)


lemma lsb_code [code]: fixes x :: uint16 shows "lsb x  bit x 0"
  by transfer (simp add: lsb_odd)

definition uint16_shiftl :: "uint16  integer  uint16"
where [code del]:
  "uint16_shiftl x n = (if n < 0  16  n then undefined (push_bit :: nat  uint16  _) x n else push_bit (nat_of_integer n) x)"

lemma shiftl_uint16_code [code]: "push_bit n x = (if n < 16 then uint16_shiftl x (integer_of_nat n) else 0)"
  including undefined_transfer integer.lifting unfolding uint16_shiftl_def
  by transfer simp

lemma uint16_shiftl_code [code abstract]:
  "Rep_uint16 (uint16_shiftl w n) =
  (if n < 0  16  n then Rep_uint16 (undefined (push_bit :: nat  uint16  _) w n)
   else push_bit (nat_of_integer n) (Rep_uint16 w))"
  including undefined_transfer unfolding uint16_shiftl_def
  by transfer simp

code_printing constant uint16_shiftl 
  (SML_word) "Uint16.shiftl" and
  (Haskell) "Data'_Bits.shiftlBounded" and
  (Scala) "Uint16.shiftl"

definition uint16_shiftr :: "uint16  integer  uint16"
where [code del]:
  "uint16_shiftr x n = (if n < 0  16  n then undefined (drop_bit :: nat  uint16  _) x n else drop_bit (nat_of_integer n) x)"

lemma shiftr_uint16_code [code]: "drop_bit n x = (if n < 16 then uint16_shiftr x (integer_of_nat n) else 0)"
  including undefined_transfer integer.lifting unfolding uint16_shiftr_def
  by transfer simp

lemma uint16_shiftr_code [code abstract]:
  "Rep_uint16 (uint16_shiftr w n) =
  (if n < 0  16  n then Rep_uint16 (undefined (drop_bit :: nat  uint16  _) w n)
   else drop_bit (nat_of_integer n) (Rep_uint16 w))"
including undefined_transfer unfolding uint16_shiftr_def by transfer simp

code_printing constant uint16_shiftr 
  (SML_word) "Uint16.shiftr" and
  (Haskell) "Data'_Bits.shiftrBounded" and
  (Scala) "Uint16.shiftr"

definition uint16_sshiftr :: "uint16  integer  uint16"
where [code del]:
  "uint16_sshiftr x n =
  (if n < 0  16  n then undefined sshiftr_uint16 x n else sshiftr_uint16 x (nat_of_integer n))"

lemma sshiftr_uint16_code [code]:
  "x >>> n = 
  (if n < 16 then uint16_sshiftr x (integer_of_nat n) else if bit x 15 then -1 else 0)"
including undefined_transfer integer.lifting unfolding uint16_sshiftr_def
by transfer (simp add: not_less signed_drop_bit_beyond word_size)

lemma uint16_sshiftr_code [code abstract]:
  "Rep_uint16 (uint16_sshiftr w n) =
  (if n < 0  16  n then Rep_uint16 (undefined sshiftr_uint16 w n)
   else signed_drop_bit (nat_of_integer n) (Rep_uint16 w))"
including undefined_transfer unfolding uint16_sshiftr_def by transfer simp

code_printing constant uint16_sshiftr 
  (SML_word) "Uint16.shiftr'_signed" and
  (Haskell) 
    "(Prelude.fromInteger (Prelude.toInteger (Data'_Bits.shiftrBounded (Prelude.fromInteger (Prelude.toInteger _) :: Uint16.Int16) _)) :: Uint16.Word16)" and
  (Scala) "Uint16.shiftr'_signed"

lemma uint16_msb_test_bit: "msb x  bit (x :: uint16) 15"
  by transfer (simp add: msb_word_iff_bit)

lemma msb_uint16_code [code]: "msb x  uint16_test_bit x 15"
  by (simp add: uint16_test_bit_def uint16_msb_test_bit)

lemma uint16_of_int_code [code]: "uint16_of_int i = Uint16 (integer_of_int i)"
including integer.lifting by transfer simp

lemma int_of_uint16_code [code]:
  "int_of_uint16 x = int_of_integer (integer_of_uint16 x)"
by(simp add: integer_of_uint16_def)

lemma nat_of_uint16_code [code]:
  "nat_of_uint16 x = nat_of_integer (integer_of_uint16 x)"
unfolding integer_of_uint16_def including integer.lifting by transfer simp

lemma integer_of_uint16_code [code]:
  "integer_of_uint16 n = integer_of_int (uint (Rep_uint16' n))"
unfolding integer_of_uint16_def by transfer auto

code_printing
  constant "integer_of_uint16" 
  (SML_word) "Word16.toInt _ : IntInf.int" and
  (Haskell) "Prelude.toInteger" and
  (Scala) "BigInt"

section ‹Quickcheck setup›

definition uint16_of_natural :: "natural  uint16"
where "uint16_of_natural x  Uint16 (integer_of_natural x)"

instantiation uint16 :: "{random, exhaustive, full_exhaustive}" begin
definition "random_uint16  qc_random_cnv uint16_of_natural"
definition "exhaustive_uint16  qc_exhaustive_cnv uint16_of_natural"
definition "full_exhaustive_uint16  qc_full_exhaustive_cnv uint16_of_natural"
instance ..
end

instantiation uint16 :: narrowing begin

interpretation quickcheck_narrowing_samples
  "λi. let x = Uint16 i in (x, 0xFFFF - x)" "0"
  "Typerep.Typerep (STR ''Uint16.uint16'') []" .

definition "narrowing_uint16 d = qc_narrowing_drawn_from (narrowing_samples d) d"
declare [[code drop: "partial_term_of :: uint16 itself  _"]]
lemmas partial_term_of_uint16 [code] = partial_term_of_code

instance ..
end

no_notation sshiftr_uint16 (infixl ">>>" 55)

end

Theory Uint8

(*  Title:      Uint8.thy
    Author:     Andreas Lochbihler, ETH Zurich
*)

chapter ‹Unsigned words of 8 bits›

theory Uint8 imports
  Code_Target_Word_Base
begin

text ‹
  Restriction for OCaml code generation:
  OCaml does not provide an int8 type, so no special code generation 
  for this type is set up. If the theory Code_Target_Bits_Int›
  is imported, the type uint8› is emulated via @{typ "8 word"}.
›

declare prod.Quotient[transfer_rule]

section ‹Type definition and primitive operations›

typedef uint8 = "UNIV :: 8 word set" ..

setup_lifting type_definition_uint8

text ‹Use an abstract type for code generation to disable pattern matching on @{term Abs_uint8}.›
declare Rep_uint8_inverse[code abstype]

declare Quotient_uint8[transfer_rule]

instantiation uint8 :: comm_ring_1
begin
lift_definition zero_uint8 :: uint8 is "0 :: 8 word" .
lift_definition one_uint8 :: uint8 is "1" .
lift_definition plus_uint8 :: "uint8  uint8  uint8" is "(+) :: 8 word  _" .
lift_definition minus_uint8 :: "uint8  uint8  uint8" is "(-)" .
lift_definition uminus_uint8 :: "uint8  uint8" is uminus .
lift_definition times_uint8 :: "uint8  uint8  uint8" is "(*)" .
instance by (standard; transfer) (simp_all add: algebra_simps)
end

instantiation uint8 :: semiring_modulo
begin
lift_definition divide_uint8 :: "uint8  uint8  uint8" is "(div)" .
lift_definition modulo_uint8 :: "uint8  uint8  uint8" is "(mod)" .
instance by (standard; transfer) (fact word_mod_div_equality)
end

instantiation uint8 :: linorder begin
lift_definition less_uint8 :: "uint8  uint8  bool" is "(<)" .
lift_definition less_eq_uint8 :: "uint8  uint8  bool" is "(≤)" .
instance by (standard; transfer) (simp_all add: less_le_not_le linear)
end

lemmas [code] = less_uint8.rep_eq less_eq_uint8.rep_eq

context
  includes lifting_syntax
  notes
    transfer_rule_of_bool [transfer_rule]
    transfer_rule_numeral [transfer_rule]
begin

lemma [transfer_rule]:
  "((=) ===> cr_uint8) of_bool of_bool"
  by transfer_prover

lemma transfer_rule_numeral_uint [transfer_rule]:
  "((=) ===> cr_uint8) numeral numeral"
  by transfer_prover

lemma [transfer_rule]:
  (cr_uint8 ===> (⟷)) even ((dvd) 2 :: uint8  bool)
  by (unfold dvd_def) transfer_prover

end

instantiation uint8 :: semiring_bits
begin

lift_definition bit_uint8 :: ‹uint8  nat  bool› is bit .

instance
  by (standard; transfer)
    (fact bit_iff_odd even_iff_mod_2_eq_zero odd_iff_mod_2_eq_one odd_one bits_induct
       bits_div_0 bits_div_by_1 bits_mod_div_trivial even_succ_div_2
       even_mask_div_iff exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq
       div_exp_mod_exp_eq even_mult_exp_div_exp_iff)+

end

instantiation uint8 :: semiring_bit_shifts
begin
lift_definition push_bit_uint8 :: ‹nat  uint8  uint8› is push_bit .
lift_definition drop_bit_uint8 :: ‹nat  uint8  uint8› is drop_bit .
lift_definition take_bit_uint8 :: ‹nat  uint8  uint8› is take_bit .
instance by (standard; transfer)
  (fact push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod)+
end

instantiation uint8 :: ring_bit_operations
begin
lift_definition not_uint8 :: ‹uint8  uint8› is NOT .
lift_definition and_uint8 :: ‹uint8  uint8  uint8› is (AND) .
lift_definition or_uint8 :: ‹uint8  uint8  uint8› is (OR) .
lift_definition xor_uint8 :: ‹uint8  uint8  uint8› is (XOR) .
lift_definition mask_uint8 :: ‹nat  uint8› is mask .
instance by (standard; transfer)
  (simp_all add: bit_and_iff bit_or_iff bit_xor_iff bit_not_iff minus_eq_not_minus_1 mask_eq_decr_exp)
end

lemma [code]:
  ‹take_bit n a = a AND mask n for a :: uint8
  by (fact take_bit_eq_mask)

lemma [code]:
  ‹mask (Suc n) = push_bit n (1 :: uint8) OR mask n
  ‹mask 0 = (0 :: uint8)
  by (simp_all add: mask_Suc_exp push_bit_of_1)

instance uint8 :: semiring_bit_syntax ..

context
  includes lifting_syntax
begin

lemma test_bit_uint8_transfer [transfer_rule]:
  (cr_uint8 ===> (=)) bit (!!)
  unfolding test_bit_eq_bit by transfer_prover

lemma shiftl_uint8_transfer [transfer_rule]:
  (cr_uint8 ===> (=) ===> cr_uint8) (λk n. push_bit n k) (<<)
  unfolding shiftl_eq_push_bit by transfer_prover

lemma shiftr_uint8_transfer [transfer_rule]:
  (cr_uint8 ===> (=) ===> cr_uint8) (λk n. drop_bit n k) (>>)
  unfolding shiftr_eq_drop_bit by transfer_prover

end

instantiation uint8 :: lsb
begin
lift_definition lsb_uint8 :: ‹uint8  bool› is lsb .
instance by (standard; transfer)
  (fact lsb_odd)
end

instantiation uint8 :: msb
begin
lift_definition msb_uint8 :: ‹uint8  bool› is msb .
instance ..
end

instantiation uint8 :: set_bit
begin
lift_definition set_bit_uint8 :: ‹uint8  nat  bool  uint8› is set_bit .
instance
  apply standard
  apply transfer
  apply (simp add: bit_simps)
  done
end

instantiation uint8 :: bit_comprehension begin
lift_definition set_bits_uint8 :: "(nat  bool)  uint8" is "set_bits" .
instance by (standard; transfer) (fact set_bits_bit_eq)
end

lemmas [code] = bit_uint8.rep_eq lsb_uint8.rep_eq msb_uint8.rep_eq

instantiation uint8 :: equal begin
lift_definition equal_uint8 :: "uint8  uint8  bool" is "equal_class.equal" .
instance by standard (transfer, simp add: equal_eq)
end

lemmas [code] = equal_uint8.rep_eq

instantiation uint8 :: size begin
lift_definition size_uint8 :: "uint8  nat" is "size" .
instance ..
end

lemmas [code] = size_uint8.rep_eq

lift_definition sshiftr_uint8 :: "uint8  nat  uint8" (infixl ">>>" 55) is λw n. signed_drop_bit n w .

lift_definition uint8_of_int :: "int  uint8" is "word_of_int" .

definition uint8_of_nat :: "nat  uint8"
where "uint8_of_nat = uint8_of_int  int"

lift_definition int_of_uint8 :: "uint8  int" is "uint" .
lift_definition nat_of_uint8 :: "uint8  nat" is "unat" .

definition integer_of_uint8 :: "uint8  integer"
where "integer_of_uint8 = integer_of_int o int_of_uint8"

text ‹Use pretty numerals from integer for pretty printing›

context includes integer.lifting begin

lift_definition Uint8 :: "integer  uint8" is "word_of_int" .

lemma Rep_uint8_numeral [simp]: "Rep_uint8 (numeral n) = numeral n"
by(induction n)(simp_all add: one_uint8_def Abs_uint8_inverse numeral.simps plus_uint8_def)

lemma numeral_uint8_transfer [transfer_rule]:
  "(rel_fun (=) cr_uint8) numeral numeral"
by(auto simp add: cr_uint8_def)

lemma numeral_uint8 [code_unfold]: "numeral n = Uint8 (numeral n)"
by transfer simp

lemma Rep_uint8_neg_numeral [simp]: "Rep_uint8 (- numeral n) = - numeral n"
by(simp only: uminus_uint8_def)(simp add: Abs_uint8_inverse)

lemma neg_numeral_uint8 [code_unfold]: "- numeral n = Uint8 (- numeral n)"
by transfer(simp add: cr_uint8_def)

end

lemma Abs_uint8_numeral [code_post]: "Abs_uint8 (numeral n) = numeral n"
by(induction n)(simp_all add: one_uint8_def numeral.simps plus_uint8_def Abs_uint8_inverse)

lemma Abs_uint8_0 [code_post]: "Abs_uint8 0 = 0"
by(simp add: zero_uint8_def)

lemma Abs_uint8_1 [code_post]: "Abs_uint8 1 = 1"
by(simp add: one_uint8_def)

section ‹Code setup›

code_printing code_module Uint8  (SML)
‹(* Test that words can handle numbers between 0 and 3 *)
val _ = if 3 <= Word.wordSize then () else raise (Fail ("wordSize less than 3"));

structure Uint8 : sig
  val set_bit : Word8.word -> IntInf.int -> bool -> Word8.word
  val shiftl : Word8.word -> IntInf.int -> Word8.word
  val shiftr : Word8.word -> IntInf.int -> Word8.word
  val shiftr_signed : Word8.word -> IntInf.int -> Word8.word
  val test_bit : Word8.word -> IntInf.int -> bool
end = struct

fun set_bit x n b =
  let val mask = Word8.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))
  in if b then Word8.orb (x, mask)
     else Word8.andb (x, Word8.notb mask)
  end

fun shiftl x n =
  Word8.<< (x, Word.fromLargeInt (IntInf.toLarge n))

fun shiftr x n =
  Word8.>> (x, Word.fromLargeInt (IntInf.toLarge n))

fun shiftr_signed x n =
  Word8.~>> (x, Word.fromLargeInt (IntInf.toLarge n))

fun test_bit x n =
  Word8.andb (x, Word8.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))) <> Word8.fromInt 0

end; (* struct Uint8 *)›
code_reserved SML Uint8

code_printing code_module Uint8  (Haskell)
 ‹module Uint8(Int8, Word8) where

  import Data.Int(Int8)
  import Data.Word(Word8)›
code_reserved Haskell Uint8

text ‹
  Scala provides only signed 8bit numbers, so we use these and 
  implement sign-sensitive operations like comparisons manually.
›

code_printing code_module Uint8  (Scala)
‹object Uint8 {

def less(x: Byte, y: Byte) : Boolean =
  if (x < 0) y < 0 && x < y
  else y < 0 || x < y

def less_eq(x: Byte, y: Byte) : Boolean =
  if (x < 0) y < 0 && x <= y
  else y < 0 || x <= y

def set_bit(x: Byte, n: BigInt, b: Boolean) : Byte =
  if (b)
    (x | (1 << n.intValue)).toByte
  else
    (x & (1 << n.intValue).unary_~).toByte

def shiftl(x: Byte, n: BigInt) : Byte = (x << n.intValue).toByte

def shiftr(x: Byte, n: BigInt) : Byte = ((x & 255) >>> n.intValue).toByte

def shiftr_signed(x: Byte, n: BigInt) : Byte = (x >> n.intValue).toByte

def test_bit(x: Byte, n: BigInt) : Boolean =
  (x & (1 << n.intValue)) != 0

} /* object Uint8 */›
code_reserved Scala Uint8

text ‹
  Avoid @{term Abs_uint8} in generated code, use @{term Rep_uint8'} instead. 
  The symbolic implementations for code\_simp use @{term Rep_uint8}.

  The new destructor @{term Rep_uint8'} is executable.
  As the simplifier is given the [code abstract] equations literally, 
  we cannot implement @{term Rep_uint8} directly, because that makes code\_simp loop.

  If code generation raises Match, some equation probably contains @{term Rep_uint8} 
  ([code abstract] equations for @{typ uint8} may use @{term Rep_uint8} because
  these instances will be folded away.)

  To convert @{typ "8 word"} values into @{typ uint8}, use @{term "Abs_uint8'"}.
›

definition Rep_uint8' where [simp]: "Rep_uint8' = Rep_uint8"

lemma Rep_uint8'_transfer [transfer_rule]:
  "rel_fun cr_uint8 (=) (λx. x) Rep_uint8'"
unfolding Rep_uint8'_def by(rule uint8.rep_transfer)

lemma Rep_uint8'_code [code]: "Rep_uint8' x = (BITS n. bit x n)"
  by transfer (simp add: set_bits_bit_eq)

lift_definition Abs_uint8' :: "8 word  uint8" is "λx :: 8 word. x" .

lemma Abs_uint8'_code [code]: "Abs_uint8' x = Uint8 (integer_of_int (uint x))"
including integer.lifting by transfer simp

declare [[code drop: "term_of_class.term_of :: uint8  _"]]

lemma term_of_uint8_code [code]:
  defines "TR  typerep.Typerep" and "bit0  STR ''Numeral_Type.bit0''" shows
  "term_of_class.term_of x = 
   Code_Evaluation.App (Code_Evaluation.Const (STR ''Uint8.uint8.Abs_uint8'') (TR (STR ''fun'') [TR (STR ''Word.word'') [TR bit0 [TR bit0 [TR bit0 [TR (STR ''Numeral_Type.num1'') []]]]], TR (STR ''Uint8.uint8'') []]))
       (term_of_class.term_of (Rep_uint8' x))"
by(simp add: term_of_anything)

lemma Uin8_code [code abstract]: "Rep_uint8 (Uint8 i) = word_of_int (int_of_integer_symbolic i)"
unfolding Uint8_def int_of_integer_symbolic_def by(simp add: Abs_uint8_inverse)

code_printing type_constructor uint8 
  (SML) "Word8.word" and
  (Haskell) "Uint8.Word8" and
  (Scala) "Byte"
| constant Uint8  
  (SML) "Word8.fromLargeInt (IntInf.toLarge _)" and
  (Haskell) "(Prelude.fromInteger _ :: Uint8.Word8)" and
  (Haskell_Quickcheck) "(Prelude.fromInteger (Prelude.toInteger _) :: Uint8.Word8)" and
  (Scala) "_.byteValue"
| constant "0 :: uint8" 
  (SML) "(Word8.fromInt 0)" and
  (Haskell) "(0 :: Uint8.Word8)" and
  (Scala) "0.toByte"
| constant "1 :: uint8" 
  (SML) "(Word8.fromInt 1)" and
  (Haskell) "(1 :: Uint8.Word8)" and
  (Scala) "1.toByte"
| constant "plus :: uint8  _  _" 
  (SML) "Word8.+ ((_), (_))" and
  (Haskell) infixl 6 "+" and
  (Scala) "(_ +/ _).toByte"
| constant "uminus :: uint8  _" 
  (SML) "Word8.~" and
  (Haskell) "negate" and
  (Scala) "(- _).toByte"
| constant "minus :: uint8  _" 
  (SML) "Word8.- ((_), (_))" and
  (Haskell) infixl 6 "-" and
  (Scala) "(_ -/ _).toByte"
| constant "times :: uint8  _  _" 
  (SML) "Word8.* ((_), (_))" and
  (Haskell) infixl 7 "*" and
  (Scala) "(_ */ _).toByte"
| constant "HOL.equal :: uint8  _  bool" 
  (SML) "!((_ : Word8.word) = _)" and
  (Haskell) infix 4 "==" and
  (Scala) infixl 5 "=="
| class_instance uint8 :: equal  (Haskell) -
| constant "less_eq :: uint8  _  bool" 
  (SML) "Word8.<= ((_), (_))" and
  (Haskell) infix 4 "<=" and
  (Scala) "Uint8.less'_eq"
| constant "less :: uint8  _  bool" 
  (SML) "Word8.< ((_), (_))" and
  (Haskell) infix 4 "<" and
  (Scala) "Uint8.less"
| constant "NOT :: uint8  _" 
  (SML) "Word8.notb" and
  (Haskell) "Data'_Bits.complement" and
  (Scala) "_.unary'_~.toByte"
| constant "(AND) :: uint8  _" 
  (SML) "Word8.andb ((_),/ (_))" and
  (Haskell) infixl 7 "Data_Bits..&." and
  (Scala) "(_ & _).toByte"
| constant "(OR) :: uint8  _" 
  (SML) "Word8.orb ((_),/ (_))" and
  (Haskell) infixl 5 "Data_Bits..|." and
  (Scala) "(_ | _).toByte"
| constant "(XOR) :: uint8  _" 
  (SML) "Word8.xorb ((_),/ (_))" and
  (Haskell) "Data'_Bits.xor" and
  (Scala) "(_ ^ _).toByte"

definition uint8_divmod :: "uint8  uint8  uint8 × uint8" where
  "uint8_divmod x y = 
  (if y = 0 then (undefined ((div) :: uint8  _) x (0 :: uint8), undefined ((mod) :: uint8  _) x (0 :: uint8)) 
  else (x div y, x mod y))"

definition uint8_div :: "uint8  uint8  uint8" 
where "uint8_div x y = fst (uint8_divmod x y)"

definition uint8_mod :: "uint8  uint8  uint8" 
where "uint8_mod x y = snd (uint8_divmod x y)"

lemma div_uint8_code [code]: "x div y = (if y = 0 then 0 else uint8_div x y)"
including undefined_transfer unfolding uint8_divmod_def uint8_div_def
by transfer (simp add: word_div_def)

lemma mod_uint8_code [code]: "x mod y = (if y = 0 then x else uint8_mod x y)"
including undefined_transfer unfolding uint8_mod_def uint8_divmod_def
by transfer (simp add: word_mod_def)

definition uint8_sdiv :: "uint8  uint8  uint8"
where
  "uint8_sdiv x y =
   (if y = 0 then undefined ((div) :: uint8  _) x (0 :: uint8)
    else Abs_uint8 (Rep_uint8 x sdiv Rep_uint8 y))"

definition div0_uint8 :: "uint8  uint8"
where [code del]: "div0_uint8 x = undefined ((div) :: uint8  _) x (0 :: uint8)"
declare [[code abort: div0_uint8]]

definition mod0_uint8 :: "uint8  uint8"
where [code del]: "mod0_uint8 x = undefined ((mod) :: uint8  _) x (0 :: uint8)"
declare [[code abort: mod0_uint8]]

lemma uint8_divmod_code [code]:
  "uint8_divmod x y =
  (if 0x80  y then if x < y then (0, x) else (1, x - y)
   else if y = 0 then (div0_uint8 x, mod0_uint8 x)
   else let q = (uint8_sdiv (x >> 1) y) << 1;
            r = x - q * y
        in if r  y then (q + 1, r - y) else (q, r))"
including undefined_transfer unfolding uint8_divmod_def uint8_sdiv_def div0_uint8_def mod0_uint8_def
  apply transfer
  apply (simp add: divmod_via_sdivmod)
  apply (simp add: shiftl_eq_push_bit shiftr_eq_drop_bit)
  done

lemma uint8_sdiv_code [code abstract]:
  "Rep_uint8 (uint8_sdiv x y) =
   (if y = 0 then Rep_uint8 (undefined ((div) :: uint8  _) x (0 :: uint8))
    else Rep_uint8 x sdiv Rep_uint8 y)"
unfolding uint8_sdiv_def by(simp add: Abs_uint8_inverse)

text ‹
  Note that we only need a translation for signed division, but not for the remainder
  because @{thm uint8_divmod_code} computes both with division only.
›

code_printing
  constant uint8_div 
  (SML) "Word8.div ((_), (_))" and
  (Haskell) "Prelude.div"
| constant uint8_mod 
  (SML) "Word8.mod ((_), (_))" and
  (Haskell) "Prelude.mod"
| constant uint8_divmod 
  (Haskell) "divmod"
| constant uint8_sdiv 
  (Scala) "(_ '/ _).toByte"

definition uint8_test_bit :: "uint8  integer  bool"
where [code del]:
  "uint8_test_bit x n =
  (if n < 0  7 < n then undefined (test_bit :: uint8  _) x n
   else x !! (nat_of_integer n))"

lemma bit_uint8_code [code]:
  "bit x n  n < 8  uint8_test_bit x (integer_of_nat n)"
  including undefined_transfer integer.lifting unfolding uint8_test_bit_def
  by (transfer, simp, transfer, simp)

lemma uint8_test_bit_code [code]:
  "uint8_test_bit w n =
  (if n < 0  7 < n then undefined (test_bit :: uint8  _) w n else Rep_uint8 w !! nat_of_integer n)"
  unfolding uint8_test_bit_def
  by (simp add: bit_uint8.rep_eq test_bit_eq_bit)

code_printing constant uint8_test_bit 
  (SML) "Uint8.test'_bit" and
  (Haskell) "Data'_Bits.testBitBounded" and
  (Scala) "Uint8.test'_bit" and
  (Eval) "(fn x => fn i => if i < 0 orelse i >= 8 then raise (Fail \"argument to uint8'_test'_bit out of bounds\") else Uint8.test'_bit x i)"


definition uint8_set_bit :: "uint8  integer  bool  uint8"
where [code del]:
  "uint8_set_bit x n b =
  (if n < 0  7 < n then undefined (set_bit :: uint8  _) x n b
   else set_bit x (nat_of_integer n) b)"

lemma set_bit_uint8_code [code]:
  "set_bit x n b = (if n < 8 then uint8_set_bit x (integer_of_nat n) b else x)"
including undefined_transfer integer.lifting unfolding uint8_set_bit_def
by(transfer)(auto cong: conj_cong simp add: not_less set_bit_beyond word_size)

lemma uint8_set_bit_code [code abstract]:
  "Rep_uint8 (uint8_set_bit w n b) = 
  (if n < 0  7 < n then Rep_uint8 (undefined (set_bit :: uint8  _) w n b)
   else set_bit (Rep_uint8 w) (nat_of_integer n) b)"
including undefined_transfer unfolding uint8_set_bit_def by transfer simp

code_printing constant uint8_set_bit 
  (SML) "Uint8.set'_bit" and
  (Haskell) "Data'_Bits.setBitBounded" and
  (Scala) "Uint8.set'_bit" and
  (Eval) "(fn x => fn i => fn b => if i < 0 orelse i >= 8 then raise (Fail \"argument to uint8'_set'_bit out of bounds\") else Uint8.set'_bit x i b)"


lift_definition uint8_set_bits :: "(nat  bool)  uint8  nat  uint8" is set_bits_aux .

lemma uint8_set_bits_code [code]:
  "uint8_set_bits f w n =
  (if n = 0 then w 
   else let n' = n - 1 in uint8_set_bits f (push_bit 1 w OR (if f n' then 1 else 0)) n')"
  apply (transfer fixing: n)
  apply (cases n)
   apply (simp_all add: shiftl_eq_push_bit)
  done

lemma set_bits_uint8 [code]:
  "(BITS n. f n) = uint8_set_bits f 0 8"
by transfer(simp add: set_bits_conv_set_bits_aux)


lemma lsb_code [code]: fixes x :: uint8 shows "lsb x = x !! 0"
  by transfer (simp add: lsb_odd)


definition uint8_shiftl :: "uint8  integer  uint8"
where [code del]:
  "uint8_shiftl x n = (if n < 0  8  n then undefined (push_bit :: nat  uint8  _) x n else push_bit (nat_of_integer n) x)"

lemma shiftl_uint8_code [code]:
  "push_bit n x = (if n < 8 then uint8_shiftl x (integer_of_nat n) else 0)"
  including undefined_transfer integer.lifting unfolding uint8_shiftl_def
  by transfer simp

lemma uint8_shiftl_code [code abstract]:
  "Rep_uint8 (uint8_shiftl w n) =
  (if n < 0  8  n then Rep_uint8 (undefined (push_bit :: nat  uint8  _) w n)
   else push_bit (nat_of_integer n) (Rep_uint8 w))"
  including undefined_transfer unfolding uint8_shiftl_def
  by transfer simp

code_printing constant uint8_shiftl 
  (SML) "Uint8.shiftl" and
  (Haskell) "Data'_Bits.shiftlBounded" and
  (Scala) "Uint8.shiftl" and
  (Eval) "(fn x => fn i => if i < 0 orelse i >= 8 then raise (Fail \"argument to uint8'_shiftl out of bounds\") else Uint8.shiftl x i)"

definition uint8_shiftr :: "uint8  integer  uint8"
where [code del]:
  "uint8_shiftr x n = (if n < 0  8  n then undefined (shiftr :: uint8  _) x n else x >> (nat_of_integer n))"

lemma shiftr_uint8_code [code]:
  "drop_bit n x = (if n < 8 then uint8_shiftr x (integer_of_nat n) else 0)"
  including undefined_transfer integer.lifting unfolding uint8_shiftr_def
  by transfer simp

lemma uint8_shiftr_code [code abstract]:
  "Rep_uint8 (uint8_shiftr w n) =
  (if n < 0  8  n then Rep_uint8 (undefined (shiftr :: uint8  _) w n) 
   else drop_bit (nat_of_integer n) (Rep_uint8 w))"
including undefined_transfer unfolding uint8_shiftr_def by transfer simp

code_printing constant uint8_shiftr 
  (SML) "Uint8.shiftr" and
  (Haskell) "Data'_Bits.shiftrBounded" and
  (Scala) "Uint8.shiftr" and
  (Eval) "(fn x => fn i => if i < 0 orelse i >= 8 then raise (Fail \"argument to uint8'_shiftr out of bounds\") else Uint8.shiftr x i)"

definition uint8_sshiftr :: "uint8  integer  uint8"
where [code del]:
  "uint8_sshiftr x n =
  (if n < 0  8  n then undefined sshiftr_uint8 x n else sshiftr_uint8 x (nat_of_integer n))"

lemma sshiftr_uint8_code [code]:
  "x >>> n = 
  (if n < 8 then uint8_sshiftr x (integer_of_nat n) else if x !! 7 then -1 else 0)"
  including undefined_transfer integer.lifting unfolding uint8_sshiftr_def
  by transfer (simp add: not_less signed_drop_bit_beyond word_size)

lemma uint8_sshiftr_code [code abstract]:
  "Rep_uint8 (uint8_sshiftr w n) =
  (if n < 0  8  n then Rep_uint8 (undefined sshiftr_uint8 w n)
   else signed_drop_bit (nat_of_integer n) (Rep_uint8 w))"
  including undefined_transfer unfolding uint8_sshiftr_def
  by transfer simp

code_printing constant uint8_sshiftr 
  (SML) "Uint8.shiftr'_signed" and
  (Haskell) 
    "(Prelude.fromInteger (Prelude.toInteger (Data'_Bits.shiftrBounded (Prelude.fromInteger (Prelude.toInteger _) :: Uint8.Int8) _)) :: Uint8.Word8)" and
  (Scala) "Uint8.shiftr'_signed" and
  (Eval) "(fn x => fn i => if i < 0 orelse i >= 8 then raise (Fail \"argument to uint8'_sshiftr out of bounds\") else Uint8.shiftr'_signed x i)"

lemma uint8_msb_test_bit: "msb x  (x :: uint8) !! 7"
  by transfer (simp add: msb_word_iff_bit)

lemma msb_uint16_code [code]: "msb x  uint8_test_bit x 7"
  by (simp add: uint8_test_bit_def uint8_msb_test_bit)

lemma uint8_of_int_code [code]: "uint8_of_int i = Uint8 (integer_of_int i)"
including integer.lifting by transfer simp

lemma int_of_uint8_code [code]:
  "int_of_uint8 x = int_of_integer (integer_of_uint8 x)"
by(simp add: integer_of_uint8_def)

lemma nat_of_uint8_code [code]:
  "nat_of_uint8 x = nat_of_integer (integer_of_uint8 x)"
unfolding integer_of_uint8_def including integer.lifting by transfer simp

definition integer_of_uint8_signed :: "uint8  integer"
where
  "integer_of_uint8_signed n = (if n !! 7 then undefined integer_of_uint8 n else integer_of_uint8 n)"

lemma integer_of_uint8_signed_code [code]:
  "integer_of_uint8_signed n =
  (if bit n 7 then undefined integer_of_uint8 n else integer_of_int (uint (Rep_uint8' n)))"
unfolding integer_of_uint8_signed_def integer_of_uint8_def
including undefined_transfer by transfer simp

lemma integer_of_uint8_code [code]:
  "integer_of_uint8 n =
  (if bit n 7 then integer_of_uint8_signed (n AND 0x7F) OR 0x80 else integer_of_uint8_signed n)"
proof -
  have (0x7F :: uint8) = mask 7
    by (simp add: mask_eq_exp_minus_1)
  then have *: n AND 0x7F = take_bit 7 n
    by (simp only: take_bit_eq_mask)
  have **: (0x80 :: int) = 2 ^ 7
    by simp
  show ?thesis
  unfolding integer_of_uint8_def integer_of_uint8_signed_def o_def *
  including undefined_transfer integer.lifting
  apply transfer
  apply (auto simp add: bit_take_bit_iff uint_take_bit_eq)
  apply (rule bit_eqI)
  apply (simp add: bit_uint_iff bit_or_iff bit_take_bit_iff)
  apply (simp only: ** bit_exp_iff)
  apply auto
  done
qed

code_printing
  constant "integer_of_uint8" 
  (SML) "IntInf.fromLarge (Word8.toLargeInt _)" and
  (Haskell) "Prelude.toInteger"
| constant "integer_of_uint8_signed" 
  (Scala) "BigInt"

section ‹Quickcheck setup›

definition uint8_of_natural :: "natural  uint8"
where "uint8_of_natural x  Uint8 (integer_of_natural x)"

instantiation uint8 :: "{random, exhaustive, full_exhaustive}" begin
definition "random_uint8  qc_random_cnv uint8_of_natural"
definition "exhaustive_uint8  qc_exhaustive_cnv uint8_of_natural"
definition "full_exhaustive_uint8  qc_full_exhaustive_cnv uint8_of_natural"
instance ..
end

instantiation uint8 :: narrowing begin

interpretation quickcheck_narrowing_samples
  "λi. let x = Uint8 i in (x, 0xFF - x)" "0"
  "Typerep.Typerep (STR ''Uint8.uint8'') []" .

definition "narrowing_uint8 d = qc_narrowing_drawn_from (narrowing_samples d) d"
declare [[code drop: "partial_term_of :: uint8 itself  _"]]
lemmas partial_term_of_uint8 [code] = partial_term_of_code

instance ..
end

no_notation sshiftr_uint8 (infixl ">>>" 55)

end

Theory Uint

(*  Title:      Uint.thy
    Author:     Peter Lammich, TU Munich
    Author:     Andreas Lochbihler, ETH Zurich
*)

chapter ‹Unsigned words of default size›

theory Uint imports
  Code_Target_Word_Base
begin

text ‹
  This theory provides access to words in the target languages of the code generator
  whose bit width is the default of the target language. To that end, the type uint›
  models words of width dflt_size›, but dflt_size› is known only to be positive.

  Usage restrictions:
  Default-size words (type uint›) cannot be used for evaluation, because 
  the results depend on the particular choice of word size in the target language
  and implementation. Symbolic evaluation has not yet been set up for uint›.
›

text ‹The default size type›
typedecl dflt_size

instantiation dflt_size :: typerep begin
definition "typerep_class.typerep   λ_ :: dflt_size itself. Typerep.Typerep (STR ''Uint.dflt_size'') []"
instance ..
end

consts dflt_size_aux :: "nat"
specification (dflt_size_aux) dflt_size_aux_g0: "dflt_size_aux > 0"
  by auto
hide_fact dflt_size_aux_def

instantiation dflt_size :: len begin
definition "len_of_dflt_size (_ :: dflt_size itself)  dflt_size_aux"
instance by(intro_classes)(simp add: len_of_dflt_size_def dflt_size_aux_g0)
end

abbreviation "dflt_size  len_of (TYPE (dflt_size))"

context includes integer.lifting begin
lift_definition dflt_size_integer :: integer is "int dflt_size" .
declare dflt_size_integer_def[code del]
  ― ‹The code generator will substitute a machine-dependent value for this constant›

lemma dflt_size_by_int[code]: "dflt_size = nat_of_integer dflt_size_integer"
by transfer simp

lemma dflt_size[simp]: 
  "dflt_size > 0"
  "dflt_size  Suc 0"
  "¬ dflt_size < Suc 0"
  using len_gt_0[where 'a=dflt_size]
  by (simp_all del: len_gt_0)
end

declare prod.Quotient[transfer_rule]

section ‹Type definition and primitive operations›

typedef uint = "UNIV :: dflt_size word set" .. 

setup_lifting type_definition_uint

text ‹Use an abstract type for code generation to disable pattern matching on @{term Abs_uint}.›
declare Rep_uint_inverse[code abstype]

declare Quotient_uint[transfer_rule]

instantiation uint :: comm_ring_1
begin
lift_definition zero_uint :: uint is "0 :: dflt_size word" .
lift_definition one_uint :: uint is "1" .
lift_definition plus_uint :: "uint  uint  uint" is "(+) :: dflt_size word  _" .
lift_definition minus_uint :: "uint  uint  uint" is "(-)" .
lift_definition uminus_uint :: "uint  uint" is uminus .
lift_definition times_uint :: "uint  uint  uint" is "(*)" .
instance by (standard; transfer) (simp_all add: algebra_simps)
end

instantiation uint :: semiring_modulo
begin
lift_definition divide_uint :: "uint  uint  uint" is "(div)" .
lift_definition modulo_uint :: "uint  uint  uint" is "(mod)" .
instance by (standard; transfer) (fact word_mod_div_equality)
end

instantiation uint :: linorder begin
lift_definition less_uint :: "uint  uint  bool" is "(<)" .
lift_definition less_eq_uint :: "uint  uint  bool" is "(≤)" .
instance by (standard; transfer) (simp_all add: less_le_not_le linear)
end

lemmas [code] = less_uint.rep_eq less_eq_uint.rep_eq

context
  includes lifting_syntax
  notes
    transfer_rule_of_bool [transfer_rule]
    transfer_rule_numeral [transfer_rule]
begin

lemma [transfer_rule]:
  "((=) ===> cr_uint) of_bool of_bool"
  by transfer_prover

lemma transfer_rule_numeral_uint [transfer_rule]:
  "((=) ===> cr_uint) numeral numeral"
  by transfer_prover

lemma [transfer_rule]:
  (cr_uint ===> (⟷)) even ((dvd) 2 :: uint  bool)
  by (unfold dvd_def) transfer_prover

end

instantiation uint :: semiring_bits
begin

lift_definition bit_uint :: ‹uint  nat  bool› is bit .

instance
  by (standard; transfer)
    (fact bit_iff_odd even_iff_mod_2_eq_zero odd_iff_mod_2_eq_one odd_one bits_induct
       bits_div_0 bits_div_by_1 bits_mod_div_trivial even_succ_div_2
       even_mask_div_iff exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq
       div_exp_mod_exp_eq even_mult_exp_div_exp_iff)+

end

instantiation uint :: semiring_bit_shifts
begin
lift_definition push_bit_uint :: ‹nat  uint  uint› is push_bit .
lift_definition drop_bit_uint :: ‹nat  uint  uint› is drop_bit .
lift_definition take_bit_uint :: ‹nat  uint  uint› is take_bit .
instance by (standard; transfer)
  (fact push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod)+
end

instantiation uint :: ring_bit_operations
begin
lift_definition not_uint :: ‹uint  uint› is NOT .
lift_definition and_uint :: ‹uint  uint  uint› is (AND) .
lift_definition or_uint :: ‹uint  uint  uint› is (OR) .
lift_definition xor_uint :: ‹uint  uint  uint› is (XOR) .
lift_definition mask_uint :: ‹nat  uint› is mask .
instance by (standard; transfer)
  (simp_all add: bit_and_iff bit_or_iff bit_xor_iff bit_not_iff minus_eq_not_minus_1 mask_eq_decr_exp)
end

lemma [code]:
  ‹take_bit n a = a AND mask n for a :: uint
  by (fact take_bit_eq_mask)

lemma [code]:
  ‹mask (Suc n) = push_bit n (1 :: uint) OR mask n
  ‹mask 0 = (0 :: uint)
  by (simp_all add: mask_Suc_exp push_bit_of_1)

instance uint :: semiring_bit_syntax ..

context
  includes lifting_syntax
begin

lemma test_bit_uint_transfer [transfer_rule]:
  (cr_uint ===> (=)) bit (!!)
  unfolding test_bit_eq_bit by transfer_prover

lemma shiftl_uint_transfer [transfer_rule]:
  (cr_uint ===> (=) ===> cr_uint) (λk n. push_bit n k) (<<)
  unfolding shiftl_eq_push_bit by transfer_prover

lemma shiftr_uint_transfer [transfer_rule]:
  (cr_uint ===> (=) ===> cr_uint) (λk n. drop_bit n k) (>>)
  unfolding shiftr_eq_drop_bit by transfer_prover

end

instantiation uint :: lsb
begin
lift_definition lsb_uint :: ‹uint  bool› is lsb .
instance by (standard; transfer)
  (fact lsb_odd)
end

instantiation uint :: msb
begin
lift_definition msb_uint :: ‹uint  bool› is msb .
instance ..
end

instantiation uint :: set_bit
begin
lift_definition set_bit_uint :: ‹uint  nat  bool  uint› is set_bit .
instance
  apply standard
  apply transfer
  apply (simp add: bit_simps)
  done
end

instantiation uint :: bit_comprehension begin
lift_definition set_bits_uint :: "(nat  bool)  uint" is "set_bits" .
instance by (standard; transfer) (fact set_bits_bit_eq)
end

lemmas [code] = bit_uint.rep_eq lsb_uint.rep_eq msb_uint.rep_eq

instantiation uint :: equal begin
lift_definition equal_uint :: "uint  uint  bool" is "equal_class.equal" .
instance by standard (transfer, simp add: equal_eq)
end

lemmas [code] = equal_uint.rep_eq

instantiation uint :: size begin
lift_definition size_uint :: "uint  nat" is "size" .
instance ..
end

lemmas [code] = size_uint.rep_eq

lift_definition sshiftr_uint :: "uint  nat  uint" (infixl ">>>" 55) is λw n. signed_drop_bit n w .

lift_definition uint_of_int :: "int  uint" is "word_of_int" .

text ‹Use pretty numerals from integer for pretty printing›

context includes integer.lifting begin

lift_definition Uint :: "integer  uint" is "word_of_int" .

lemma Rep_uint_numeral [simp]: "Rep_uint (numeral n) = numeral n"
by(induction n)(simp_all add: one_uint_def Abs_uint_inverse numeral.simps plus_uint_def)

lemma numeral_uint_transfer [transfer_rule]:
  "(rel_fun (=) cr_uint) numeral numeral"
by(auto simp add: cr_uint_def)

lemma numeral_uint [code_unfold]: "numeral n = Uint (numeral n)"
by transfer simp

lemma Rep_uint_neg_numeral [simp]: "Rep_uint (- numeral n) = - numeral n"
by(simp only: uminus_uint_def)(simp add: Abs_uint_inverse)

lemma neg_numeral_uint [code_unfold]: "- numeral n = Uint (- numeral n)"
by transfer(simp add: cr_uint_def)

end

lemma Abs_uint_numeral [code_post]: "Abs_uint (numeral n) = numeral n"
by(induction n)(simp_all add: one_uint_def numeral.simps plus_uint_def Abs_uint_inverse)

lemma Abs_uint_0 [code_post]: "Abs_uint 0 = 0"
by(simp add: zero_uint_def)

lemma Abs_uint_1 [code_post]: "Abs_uint 1 = 1"
by(simp add: one_uint_def)

section ‹Code setup›

code_printing code_module Uint  (SML)
‹
structure Uint : sig
  val set_bit : Word.word -> IntInf.int -> bool -> Word.word
  val shiftl : Word.word -> IntInf.int -> Word.word
  val shiftr : Word.word -> IntInf.int -> Word.word
  val shiftr_signed : Word.word -> IntInf.int -> Word.word
  val test_bit : Word.word -> IntInf.int -> bool
end = struct

fun set_bit x n b =
  let val mask = Word.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))
  in if b then Word.orb (x, mask)
     else Word.andb (x, Word.notb mask)
  end

fun shiftl x n =
  Word.<< (x, Word.fromLargeInt (IntInf.toLarge n))

fun shiftr x n =
  Word.>> (x, Word.fromLargeInt (IntInf.toLarge n))

fun shiftr_signed x n =
  Word.~>> (x, Word.fromLargeInt (IntInf.toLarge n))

fun test_bit x n =
  Word.andb (x, Word.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))) <> Word.fromInt 0

end; (* struct Uint *)›
code_reserved SML Uint

code_printing code_module Uint  (Haskell)
 ‹module Uint(Int, Word, dflt_size) where

  import qualified Prelude
  import Data.Int(Int)
  import Data.Word(Word)
  import qualified Data.Bits

  dflt_size :: Prelude.Integer
  dflt_size = Prelude.toInteger (bitSize_aux (0::Word)) where
    bitSize_aux :: (Data.Bits.Bits a, Prelude.Bounded a) => a -> Int
    bitSize_aux = Data.Bits.bitSize›
  and (Haskell_Quickcheck)
 ‹module Uint(Int, Word, dflt_size) where

  import qualified Prelude
  import Data.Int(Int)
  import Data.Word(Word)
  import qualified Data.Bits

  dflt_size :: Prelude.Int
  dflt_size = bitSize_aux (0::Word) where
    bitSize_aux :: (Data.Bits.Bits a, Prelude.Bounded a) => a -> Int
    bitSize_aux = Data.Bits.bitSize
›
code_reserved Haskell Uint dflt_size

text ‹
  OCaml and Scala provide only signed bit numbers, so we use these and 
  implement sign-sensitive operations like comparisons manually.
›

code_printing code_module "Uint"  (OCaml)
‹module Uint : sig
  type t = int
  val dflt_size : Z.t
  val less : t -> t -> bool
  val less_eq : t -> t -> bool
  val set_bit : t -> Z.t -> bool -> t
  val shiftl : t -> Z.t -> t
  val shiftr : t -> Z.t -> t
  val shiftr_signed : t -> Z.t -> t
  val test_bit : t -> Z.t -> bool
  val int_mask : int
  val int32_mask : int32
  val int64_mask : int64
end = struct

type t = int

let dflt_size = Z.of_int Sys.int_size;;

(* negative numbers have their highest bit set, 
   so they are greater than positive ones *)
let less x y =
  if x<0 then
    y<0 && x<y
  else y < 0 || x < y;;

let less_eq x y =
  if x < 0 then
    y < 0 &&  x <= y
  else y < 0 || x <= y;;

let set_bit x n b =
  let mask = 1 lsl (Z.to_int n)
  in if b then x lor mask
     else x land (lnot mask);;

let shiftl x n = x lsl (Z.to_int n);;

let shiftr x n = x lsr (Z.to_int n);;

let shiftr_signed x n = x asr (Z.to_int n);;

let test_bit x n = x land (1 lsl (Z.to_int n)) <> 0;;

let int_mask =
  if Sys.int_size < 32 then lnot 0 else 0xFFFFFFFF;;

let int32_mask = 
  if Sys.int_size < 32 then Int32.pred (Int32.shift_left Int32.one Sys.int_size)
  else Int32.of_string "0xFFFFFFFF";;

let int64_mask = 
  if Sys.int_size < 64 then Int64.pred (Int64.shift_left Int64.one Sys.int_size)
  else Int64.of_string "0xFFFFFFFFFFFFFFFF";;

end;; (*struct Uint*)›
code_reserved OCaml Uint

code_printing code_module Uint  (Scala)
‹object Uint {
def dflt_size : BigInt = BigInt(32)

def less(x: Int, y: Int) : Boolean =
  if (x < 0) y < 0 && x < y
  else y < 0 || x < y

def less_eq(x: Int, y: Int) : Boolean =
  if (x < 0) y < 0 && x <= y
  else y < 0 || x <= y

def set_bit(x: Int, n: BigInt, b: Boolean) : Int =
  if (b)
    x | (1 << n.intValue)
  else
    x & (1 << n.intValue).unary_~

def shiftl(x: Int, n: BigInt) : Int = x << n.intValue

def shiftr(x: Int, n: BigInt) : Int = x >>> n.intValue

def shiftr_signed(x: Int, n: BigInt) : Int = x >> n.intValue

def test_bit(x: Int, n: BigInt) : Boolean =
  (x & (1 << n.intValue)) != 0

} /* object Uint */›
code_reserved Scala Uint


text ‹
  OCaml's conversion from Big\_int to int demands that the value fits into a signed integer.
  The following justifies the implementation.
›

context includes integer.lifting begin
definition wivs_mask :: int where "wivs_mask = 2^ dflt_size - 1"
lift_definition wivs_mask_integer :: integer is wivs_mask .
lemma [code]: "wivs_mask_integer = 2 ^ dflt_size - 1"
  by transfer (simp add: wivs_mask_def)

definition wivs_shift :: int where "wivs_shift = 2 ^ dflt_size"
lift_definition wivs_shift_integer :: integer is wivs_shift .
lemma [code]: "wivs_shift_integer = 2 ^ dflt_size"
  by transfer (simp add: wivs_shift_def)

definition wivs_index :: nat where "wivs_index == dflt_size - 1"
lift_definition wivs_index_integer :: integer is "int wivs_index".
lemma wivs_index_integer_code[code]: "wivs_index_integer = dflt_size_integer - 1"
  by transfer (simp add: wivs_index_def of_nat_diff)

definition wivs_overflow :: int where "wivs_overflow == 2^ (dflt_size - 1)"
lift_definition wivs_overflow_integer :: integer is wivs_overflow .
lemma [code]: "wivs_overflow_integer = 2 ^ (dflt_size - 1)"
  by transfer (simp add: wivs_overflow_def)

definition wivs_least :: int where "wivs_least == - wivs_overflow"
lift_definition wivs_least_integer :: integer is wivs_least .
lemma [code]: "wivs_least_integer = - (2 ^ (dflt_size - 1))"
  by transfer (simp add: wivs_overflow_def wivs_least_def)

definition Uint_signed :: "integer  uint" where
  "Uint_signed i = (if i < wivs_least_integer  wivs_overflow_integer  i then undefined Uint i else Uint i)"

lemma Uint_code [code]:
  "Uint i = 
  (let i' = i AND wivs_mask_integer in 
   if bit i' wivs_index then Uint_signed (i' - wivs_shift_integer) else Uint_signed i')"
  including undefined_transfer 
  unfolding Uint_signed_def
  apply transfer
  apply (subst word_of_int_via_signed)
       apply (auto simp add: shiftl_eq_push_bit push_bit_of_1 mask_eq_exp_minus_1 word_of_int_via_signed
         wivs_mask_def wivs_index_def wivs_overflow_def wivs_least_def wivs_shift_def)
  done

lemma Uint_signed_code [code abstract]:
  "Rep_uint (Uint_signed i) = 
  (if i < wivs_least_integer  i  wivs_overflow_integer then Rep_uint (undefined Uint i) else word_of_int (int_of_integer_symbolic i))"
  unfolding Uint_signed_def Uint_def int_of_integer_symbolic_def word_of_integer_def
  by(simp add: Abs_uint_inverse)
end

text ‹
  Avoid @{term Abs_uint} in generated code, use @{term Rep_uint'} instead. 
  The symbolic implementations for code\_simp use @{term Rep_uint}.

  The new destructor @{term Rep_uint'} is executable.
  As the simplifier is given the [code abstract] equations literally, 
  we cannot implement @{term Rep_uint} directly, because that makes code\_simp loop.

  If code generation raises Match, some equation probably contains @{term Rep_uint} 
  ([code abstract] equations for @{typ uint} may use @{term Rep_uint} because
  these instances will be folded away.)
›

definition Rep_uint' where [simp]: "Rep_uint' = Rep_uint"

lemma Rep_uint'_code [code]: "Rep_uint' x = (BITS n. bit x n)"
  unfolding Rep_uint'_def by transfer (simp add: set_bits_bit_eq)

lift_definition Abs_uint' :: "dflt_size word  uint" is "λx :: dflt_size word. x" .

lemma Abs_uint'_code [code]:
  "Abs_uint' x = Uint (integer_of_int (uint x))"
including integer.lifting by transfer simp

declare [[code drop: "term_of_class.term_of :: uint  _"]]

lemma term_of_uint_code [code]:
  defines "TR  typerep.Typerep" and "bit0  STR ''Numeral_Type.bit0''" 
  shows
  "term_of_class.term_of x = 
   Code_Evaluation.App (Code_Evaluation.Const (STR ''Uint.uint.Abs_uint'') (TR (STR ''fun'') [TR (STR ''Word.word'')  [TR (STR ''Uint.dflt_size'') []], TR (STR ''Uint.uint'') []]))
       (term_of_class.term_of (Rep_uint' x))"
  by(simp add: term_of_anything)

text ‹Important:
  We must prevent the reflection oracle (eval-tac) to 
  use our machine-dependent type.
›

code_printing
  type_constructor uint 
  (SML) "Word.word" and
  (Haskell) "Uint.Word" and
  (OCaml) "Uint.t" and
  (Scala) "Int" and
  (Eval) "*** \"Error: Machine dependent type\" ***" and
  (Quickcheck) "Word.word" 
| constant dflt_size_integer 
  (SML) "(IntInf.fromLarge (Int.toLarge Word.wordSize))" and
  (Eval) "(raise (Fail \"Machine dependent code\"))" and
  (Quickcheck) "Word.wordSize" and
  (Haskell) "Uint.dflt'_size" and
  (OCaml) "Uint.dflt'_size" and
  (Scala) "Uint.dflt'_size"
| constant Uint 
  (SML) "Word.fromLargeInt (IntInf.toLarge _)" and
  (Eval) "(raise (Fail \"Machine dependent code\"))" and
  (Quickcheck) "Word.fromInt" and
  (Haskell) "(Prelude.fromInteger _ :: Uint.Word)" and
  (Haskell_Quickcheck) "(Prelude.fromInteger (Prelude.toInteger _) :: Uint.Word)" and
  (Scala) "_.intValue"
| constant Uint_signed 
  (OCaml) "Z.to'_int"
| constant "0 :: uint" 
  (SML) "(Word.fromInt 0)" and
  (Eval) "(raise (Fail \"Machine dependent code\"))" and
  (Quickcheck) "(Word.fromInt 0)" and
  (Haskell) "(0 :: Uint.Word)" and
  (OCaml) "0" and
  (Scala) "0"
| constant "1 :: uint" 
  (SML) "(Word.fromInt 1)" and
  (Eval) "(raise (Fail \"Machine dependent code\"))" and
  (Quickcheck) "(Word.fromInt 1)" and
  (Haskell) "(1 :: Uint.Word)" and
  (OCaml) "1" and
  (Scala) "1"
| constant "plus :: uint  _ " 
  (SML) "Word.+ ((_), (_))" and
  (Eval) "(raise (Fail \"Machine dependent code\"))" and
  (Quickcheck) "Word.+ ((_), (_))" and
  (Haskell) infixl 6 "+" and
  (OCaml) "Pervasives.(+)" and
  (Scala) infixl 7 "+"
| constant "uminus :: uint  _" 
  (SML) "Word.~" and
  (Eval) "(raise (Fail \"Machine dependent code\"))" and
  (Quickcheck) "Word.~" and
  (Haskell) "negate" and
  (OCaml) "Pervasives.(~-)" and
  (Scala) "!(- _)"
| constant "minus :: uint  _" 
  (SML) "Word.- ((_), (_))" and
  (Eval) "(raise (Fail \"Machine dependent code\"))" and
  (Quickcheck) "Word.- ((_), (_))" and
  (Haskell) infixl 6 "-" and
  (OCaml) "Pervasives.(-)" and
  (Scala) infixl 7 "-"
| constant "times :: uint  _  _" 
  (SML) "Word.* ((_), (_))" and
  (Eval) "(raise (Fail \"Machine dependent code\"))" and
  (Quickcheck) "Word.* ((_), (_))" and
  (Haskell) infixl 7 "*" and
  (OCaml) "Pervasives.( * )" and
  (Scala) infixl 8 "*"
| constant "HOL.equal :: uint  _  bool" 
  (SML) "!((_ : Word.word) = _)" and
  (Eval) "(raise (Fail \"Machine dependent code\"))" and
  (Quickcheck) "!((_ : Word.word) = _)" and
  (Haskell) infix 4 "==" and
  (OCaml) "(Pervasives.(=):Uint.t -> Uint.t -> bool)" and
  (Scala) infixl 5 "=="
| class_instance uint :: equal 
  (Haskell) -
| constant "less_eq :: uint  _  bool" 
  (SML) "Word.<= ((_), (_))" and
  (Eval) "(raise (Fail \"Machine dependent code\"))" and
  (Quickcheck) "Word.<= ((_), (_))" and
  (Haskell) infix 4 "<=" and
  (OCaml) "Uint.less'_eq" and
  (Scala) "Uint.less'_eq"
| constant "less :: uint  _  bool" 
  (SML) "Word.< ((_), (_))" and
  (Eval) "(raise (Fail \"Machine dependent code\"))" and
  (Quickcheck) "Word.< ((_), (_))" and
  (Haskell) infix 4 "<" and
  (OCaml) "Uint.less" and
  (Scala) "Uint.less"
| constant "NOT :: uint  _" 
  (SML) "Word.notb" and
  (Eval) "(raise (Fail \"Machine dependent code\"))" and
  (Quickcheck) "Word.notb" and
  (Haskell) "Data'_Bits.complement" and
  (OCaml) "Pervasives.lnot" and
  (Scala) "_.unary'_~"
| constant "(AND) :: uint  _" 
  (SML) "Word.andb ((_),/ (_))" and
  (Eval) "(raise (Fail \"Machine dependent code\"))" and
  (Quickcheck) "Word.andb ((_),/ (_))" and
  (Haskell) infixl 7 "Data_Bits..&." and
  (OCaml) "Pervasives.(land)" and
  (Scala) infixl 3 "&"
| constant "(OR) :: uint  _" 
  (SML) "Word.orb ((_),/ (_))" and
  (Eval) "(raise (Fail \"Machine dependent code\"))" and
  (Quickcheck) "Word.orb ((_),/ (_))" and
  (Haskell) infixl 5 "Data_Bits..|." and
  (OCaml) "Pervasives.(lor)" and
  (Scala) infixl 1 "|"
| constant "(XOR) :: uint  _" 
  (SML) "Word.xorb ((_),/ (_))" and
  (Eval) "(raise (Fail \"Machine dependent code\"))" and
  (Quickcheck) "Word.xorb ((_),/ (_))" and
  (Haskell) "Data'_Bits.xor" and
  (OCaml) "Pervasives.(lxor)" and
  (Scala) infixl 2 "^"

definition uint_divmod :: "uint  uint  uint × uint" where
  "uint_divmod x y = 
  (if y = 0 then (undefined ((div) :: uint  _) x (0 :: uint), undefined ((mod) :: uint  _) x (0 :: uint)) 
  else (x div y, x mod y))"

definition uint_div :: "uint  uint  uint" 
where "uint_div x y = fst (uint_divmod x y)"

definition uint_mod :: "uint  uint  uint" 
where "uint_mod x y = snd (uint_divmod x y)"

lemma div_uint_code [code]: "x div y = (if y = 0 then 0 else uint_div x y)"
including undefined_transfer unfolding uint_divmod_def uint_div_def
by transfer(simp add: word_div_def)

lemma mod_uint_code [code]: "x mod y = (if y = 0 then x else uint_mod x y)"
including undefined_transfer unfolding uint_mod_def uint_divmod_def
by transfer(simp add: word_mod_def)

definition uint_sdiv :: "uint  uint  uint"
where [code del]:
  "uint_sdiv x y =
   (if y = 0 then undefined ((div) :: uint  _) x (0 :: uint)
    else Abs_uint (Rep_uint x sdiv Rep_uint y))"

definition div0_uint :: "uint  uint"
where [code del]: "div0_uint x = undefined ((div) :: uint  _) x (0 :: uint)"
declare [[code abort: div0_uint]]

definition mod0_uint :: "uint  uint"
where [code del]: "mod0_uint x = undefined ((mod) :: uint  _) x (0 :: uint)"
declare [[code abort: mod0_uint]]

definition wivs_overflow_uint :: uint 
  where "wivs_overflow_uint  push_bit (dflt_size - 1) 1"

lemma uint_divmod_code [code]:
  "uint_divmod x y =
  (if wivs_overflow_uint  y then if x < y then (0, x) else (1, x - y)
   else if y = 0 then (div0_uint x, mod0_uint x)
   else let q = push_bit 1 (uint_sdiv (drop_bit 1 x) y);
            r = x - q * y
        in if r  y then (q + 1, r - y) else (q, r))"
proof (cases y = 0)
  case True
  moreover have x  0
    by transfer simp
  moreover have ‹wivs_overflow_uint > 0
    apply (simp add: wivs_overflow_uint_def push_bit_of_1)
    apply transfer
    apply transfer
    apply simp
    done
  ultimately show ?thesis
    by (auto simp add: uint_divmod_def div0_uint_def mod0_uint_def not_less)
next
  case False
  then show ?thesis
    including undefined_transfer 
    unfolding uint_divmod_def uint_sdiv_def div0_uint_def mod0_uint_def
      wivs_overflow_uint_def
    apply transfer
    apply (simp add: divmod_via_sdivmod push_bit_of_1 shiftl_eq_push_bit shiftr_eq_drop_bit)
    done
qed

lemma uint_sdiv_code [code abstract]:
  "Rep_uint (uint_sdiv x y) =
   (if y = 0 then Rep_uint (undefined ((div) :: uint  _) x (0 :: uint))
    else Rep_uint x sdiv Rep_uint y)"
unfolding uint_sdiv_def by(simp add: Abs_uint_inverse)

text ‹
  Note that we only need a translation for signed division, but not for the remainder
  because @{thm uint_divmod_code} computes both with division only.
›

code_printing
  constant uint_div 
  (SML) "Word.div ((_), (_))" and
  (Eval) "(raise (Fail \"Machine dependent code\"))" and
  (Quickcheck) "Word.div ((_), (_))" and
  (Haskell) "Prelude.div"
| constant uint_mod 
  (SML) "Word.mod ((_), (_))" and
  (Eval) "(raise (Fail \"Machine dependent code\"))" and
  (Quickcheck) "Word.mod ((_), (_))" and
  (Haskell) "Prelude.mod"
| constant uint_divmod 
  (Haskell) "divmod"
| constant uint_sdiv 
  (OCaml) "Pervasives.('/)" and
  (Scala) "_ '/ _"

definition uint_test_bit :: "uint  integer  bool"
where [code del]:
  "uint_test_bit x n =
  (if n < 0  dflt_size_integer  n then undefined (bit :: uint  _) x n
   else bit x (nat_of_integer n))"

lemma test_bit_uint_code [code]:
  "bit x n  n < dflt_size  uint_test_bit x (integer_of_nat n)"
  including undefined_transfer integer.lifting unfolding uint_test_bit_def
  by (transfer, simp, transfer, simp)

lemma uint_test_bit_code [code]:
  "uint_test_bit w n =
  (if n < 0  dflt_size_integer  n then undefined (bit :: uint  _) w n else bit (Rep_uint w) (nat_of_integer n))"
  unfolding uint_test_bit_def by(simp add: bit_uint.rep_eq)

code_printing constant uint_test_bit 
  (SML) "Uint.test'_bit" and
  (Eval) "(raise (Fail \"Machine dependent code\"))" and
  (Quickcheck) "Uint.test'_bit" and
  (Haskell) "Data'_Bits.testBitBounded" and
  (OCaml) "Uint.test'_bit" and
  (Scala) "Uint.test'_bit"

definition uint_set_bit :: "uint  integer  bool  uint"
where [code del]:
  "uint_set_bit x n b =
  (if n < 0  dflt_size_integer  n then undefined (set_bit :: uint  _) x n b
   else set_bit x (nat_of_integer n) b)"

lemma set_bit_uint_code [code]:
  "set_bit x n b = (if n < dflt_size then uint_set_bit x (integer_of_nat n) b else x)"
  including undefined_transfer integer.lifting unfolding uint_set_bit_def
  by (transfer) (auto cong: conj_cong simp add: not_less set_bit_beyond word_size)

lemma uint_set_bit_code [code abstract]:
  "Rep_uint (uint_set_bit w n b) = 
  (if n < 0  dflt_size_integer  n then Rep_uint (undefined (set_bit :: uint  _) w n b)
   else set_bit (Rep_uint w) (nat_of_integer n) b)"
including undefined_transfer integer.lifting unfolding uint_set_bit_def by transfer simp

code_printing constant uint_set_bit 
  (SML) "Uint.set'_bit" and
  (Eval) "(raise (Fail \"Machine dependent code\"))" and
  (Quickcheck) "Uint.set'_bit" and
  (Haskell) "Data'_Bits.setBitBounded" and
  (OCaml) "Uint.set'_bit" and
  (Scala) "Uint.set'_bit"

lift_definition uint_set_bits :: "(nat  bool)  uint  nat  uint" is set_bits_aux .

lemma uint_set_bits_code [code]:
  "uint_set_bits f w n =
  (if n = 0 then w 
   else let n' = n - 1 in uint_set_bits f (push_bit 1 w OR (if f n' then 1 else 0)) n')"
  apply (transfer fixing: n)
  apply (cases n)
   apply (simp_all add: shiftl_eq_push_bit)
  done

lemma set_bits_uint [code]:
  "(BITS n. f n) = uint_set_bits f 0 dflt_size"
  by transfer (simp add: set_bits_conv_set_bits_aux)

lemma lsb_code [code]: fixes x :: uint shows "lsb x = bit x 0"
  by transfer (simp add: lsb_word_eq)

definition uint_shiftl :: "uint  integer  uint"
where [code del]:
  "uint_shiftl x n = (if n < 0  dflt_size_integer  n then undefined (push_bit :: nat  uint  _) x n else push_bit (nat_of_integer n) x)"

lemma shiftl_uint_code [code]: "push_bit n x = (if n < dflt_size then uint_shiftl x (integer_of_nat n) else 0)"
  including undefined_transfer integer.lifting unfolding uint_shiftl_def
  by (transfer fixing: n) simp

lemma uint_shiftl_code [code abstract]:
  "Rep_uint (uint_shiftl w n) =
  (if n < 0  dflt_size_integer  n then Rep_uint (undefined (push_bit :: nat  uint  _) w n) else push_bit (nat_of_integer n) (Rep_uint w))"
  including undefined_transfer integer.lifting unfolding uint_shiftl_def by transfer simp

code_printing constant uint_shiftl 
  (SML) "Uint.shiftl" and
  (Eval) "(raise (Fail \"Machine dependent code\"))" and
  (Quickcheck) "Uint.shiftl" and
  (Haskell) "Data'_Bits.shiftlBounded" and
  (OCaml) "Uint.shiftl" and
  (Scala) "Uint.shiftl"

definition uint_shiftr :: "uint  integer  uint"
where [code del]:
  "uint_shiftr x n = (if n < 0  dflt_size_integer  n then undefined (drop_bit :: nat  uint  _) x n else drop_bit (nat_of_integer n) x)"

lemma shiftr_uint_code [code]: "drop_bit n x = (if n < dflt_size then uint_shiftr x (integer_of_nat n) else 0)"
  including undefined_transfer integer.lifting unfolding uint_shiftr_def
  by (transfer fixing: n) simp
  
lemma uint_shiftr_code [code abstract]:
  "Rep_uint (uint_shiftr w n) =
  (if n < 0  dflt_size_integer  n then Rep_uint (undefined (drop_bit :: nat  uint  _) w n) else drop_bit (nat_of_integer n) (Rep_uint w))"
including undefined_transfer unfolding uint_shiftr_def by transfer simp

code_printing constant uint_shiftr 
  (SML) "Uint.shiftr" and
  (Eval) "(raise (Fail \"Machine dependent code\"))" and
  (Quickcheck) "Uint.shiftr" and
  (Haskell) "Data'_Bits.shiftrBounded" and
  (OCaml) "Uint.shiftr" and
  (Scala) "Uint.shiftr"

definition uint_sshiftr :: "uint  integer  uint"
where [code del]:
  "uint_sshiftr x n =
  (if n < 0  dflt_size_integer  n then undefined sshiftr_uint x n else sshiftr_uint x (nat_of_integer n))"

lemma sshiftr_uint_code [code]:
  "x >>> n = 
  (if n < dflt_size then uint_sshiftr x (integer_of_nat n) else 
    if bit x wivs_index then -1 else 0)"
including undefined_transfer integer.lifting unfolding uint_sshiftr_def
by transfer(simp add: not_less signed_drop_bit_beyond word_size wivs_index_def)

lemma uint_sshiftr_code [code abstract]:
  "Rep_uint (uint_sshiftr w n) =
  (if n < 0  dflt_size_integer  n then Rep_uint (undefined sshiftr_uint w n) else signed_drop_bit (nat_of_integer n) (Rep_uint w))"
including undefined_transfer unfolding uint_sshiftr_def by transfer simp

code_printing constant uint_sshiftr 
  (SML) "Uint.shiftr'_signed" and
  (Eval) "(raise (Fail \"Machine dependent code\"))" and
  (Quickcheck) "Uint.shiftr'_signed" and
  (Haskell) 
    "(Prelude.fromInteger (Prelude.toInteger (Data'_Bits.shiftrBounded (Prelude.fromInteger (Prelude.toInteger _) :: Uint.Int) _)) :: Uint.Word)" and
  (OCaml) "Uint.shiftr'_signed" and
  (Scala) "Uint.shiftr'_signed"

lemma uint_msb_test_bit: "msb x  bit (x :: uint) wivs_index"
  by transfer (simp add: msb_word_iff_bit wivs_index_def)

lemma msb_uint_code [code]: "msb x  uint_test_bit x wivs_index_integer"
  apply(simp add: uint_test_bit_def uint_msb_test_bit 
  wivs_index_integer_code dflt_size_integer_def wivs_index_def)
  by (metis (full_types) One_nat_def dflt_size(2) less_iff_diff_less_0 
    nat_of_integer_of_nat of_nat_1 of_nat_diff of_nat_less_0_iff wivs_index_def)

lemma uint_of_int_code [code]: "uint_of_int i = (BITS n. bit i n)"
  by transfer (simp add: word_of_int_conv_set_bits)


section ‹Quickcheck setup›

definition uint_of_natural :: "natural  uint"
where "uint_of_natural x  Uint (integer_of_natural x)"

instantiation uint :: "{random, exhaustive, full_exhaustive}" begin
definition "random_uint  qc_random_cnv uint_of_natural"
definition "exhaustive_uint  qc_exhaustive_cnv uint_of_natural"
definition "full_exhaustive_uint  qc_full_exhaustive_cnv uint_of_natural"
instance ..
end

instantiation uint :: narrowing begin

interpretation quickcheck_narrowing_samples
  "λi. (Uint i, Uint (- i))" "0"
  "Typerep.Typerep (STR ''Uint.uint'') []" .

definition "narrowing_uint d = qc_narrowing_drawn_from (narrowing_samples d) d"
declare [[code drop: "partial_term_of :: uint itself  _"]]
lemmas partial_term_of_uint [code] = partial_term_of_code

instance ..
end

no_notation sshiftr_uint (infixl ">>>" 55)

end

Theory Native_Cast

(*  Title:      Native_Cast.thy
    Author:     Andreas Lochbihler, ETH Zurich
*)

chapter ‹Conversions between unsigned words and between char›

theory Native_Cast
  imports
  Uint8
  Uint16
  Uint32
  Uint64
begin

text ‹Auxiliary stuff›

lemma integer_of_char_char_of_integer [simp]:
  "integer_of_char (char_of_integer x) = x mod 256"
  by (simp add: integer_of_char_def char_of_integer_def)

lemma char_of_integer_integer_of_char [simp]:
  "char_of_integer (integer_of_char x) = x"
  by (simp add: integer_of_char_def char_of_integer_def)

lemma int_lt_numeral [simp]: "int x < numeral n  x < numeral n"
by (metis nat_numeral zless_nat_eq_int_zless)

lemma int_of_integer_ge_0: "0  int_of_integer x  0  x"
including integer.lifting by transfer simp

lemma integer_of_char_ge_0 [simp]: "0  integer_of_char x"
  including integer.lifting unfolding integer_of_char_def
  by transfer (simp add: of_char_def)


section ‹Conversion between native words›

lift_definition uint8_of_uint16 :: "uint16  uint8" is ucast .
lift_definition uint8_of_uint32 :: "uint32  uint8" is ucast .
lift_definition uint8_of_uint64 :: "uint64  uint8" is ucast .

lift_definition uint16_of_uint8 :: "uint8  uint16" is ucast .
lift_definition uint16_of_uint32 :: "uint32  uint16" is ucast .
lift_definition uint16_of_uint64 :: "uint64  uint16" is ucast .

lift_definition uint32_of_uint8 :: "uint8  uint32" is ucast .
lift_definition uint32_of_uint16 :: "uint16  uint32" is ucast .
lift_definition uint32_of_uint64 :: "uint64  uint32" is ucast .

lift_definition uint64_of_uint8 :: "uint8  uint64" is ucast .
lift_definition uint64_of_uint16 :: "uint16  uint64" is ucast .
lift_definition uint64_of_uint32 :: "uint32  uint64" is ucast .

context
begin

qualified definition mask :: integer
  where mask = (0xFFFFFFFF :: integer)

end

code_printing
  constant uint8_of_uint16 
  (SML_word) "Word8.fromLarge (Word16.toLarge _)" and
  (Haskell) "(Prelude.fromIntegral _ :: Uint8.Word8)" and
  (Scala) "_.toByte"
| constant uint8_of_uint32 
  (SML) "Word8.fromLarge (Word32.toLarge _)" and
  (Haskell) "(Prelude.fromIntegral _ :: Uint8.Word8)" and
  (Scala) "_.toByte"
| constant uint8_of_uint64 
  (SML) "Word8.fromLarge (Uint64.toLarge _)" and
  (Haskell) "(Prelude.fromIntegral _ :: Uint8.Word8)" and
  (Scala) "_.toByte"
| constant uint16_of_uint8 
  (SML_word) "Word16.fromLarge (Word8.toLarge _)" and
  (Haskell) "(Prelude.fromIntegral _ :: Uint16.Word16)" and
  (Scala) "((_).toInt & 0xFF).toChar"
| constant uint16_of_uint32 
  (SML_word) "Word16.fromLarge (Word32.toLarge _)" and
  (Haskell) "(Prelude.fromIntegral _ :: Uint16.Word16)" and
  (Scala) "_.toChar"
| constant uint16_of_uint64 
  (SML_word) "Word16.fromLarge (Uint64.toLarge _)" and
  (Haskell) "(Prelude.fromIntegral _ :: Uint16.Word16)" and
  (Scala) "_.toChar"
| constant uint32_of_uint8 
  (SML) "Word32.fromLarge (Word8.toLarge _)" and
  (Haskell) "(Prelude.fromIntegral _ :: Uint32.Word32)" and
  (Scala) "((_).toInt & 0xFF)"
| constant uint32_of_uint16 
  (SML_word) "Word32.fromLarge (Word16.toLarge _)" and
  (Haskell) "(Prelude.fromIntegral _ :: Uint32.Word32)" and
  (Scala) "(_).toInt"
| constant uint32_of_uint64 
  (SML_word) "Word32.fromLarge (Uint64.toLarge _)" and
  (Haskell) "(Prelude.fromIntegral _ :: Uint32.Word32)" and
  (Scala) "(_).toInt" and
  (OCaml) "Int64.to'_int32"
| constant uint64_of_uint8 
  (SML_word) "Word64.fromLarge (Word8.toLarge _)" and
  (Haskell) "(Prelude.fromIntegral _ :: Uint64.Word64)" and
  (Scala) "((_).toLong & 0xFF)"
| constant uint64_of_uint16 
  (SML_word) "Word64.fromLarge (Word16.toLarge _)" and
  (Haskell) "(Prelude.fromIntegral _ :: Uint64.Word64)" and
  (Scala) "_.toLong"
| constant uint64_of_uint32 
  (SML_word) "Word64.fromLarge (Word32.toLarge _)" and
  (Haskell) "(Prelude.fromIntegral _ :: Uint64.Word64)" and
  (Scala) "((_).toLong & 0xFFFFFFFFL)" and
  (OCaml) "Int64.logand (Int64.of'_int32 _) (Int64.of'_string \"4294967295\")"

text ‹
  Use @{const Abs_uint8'} etc. instead of @{const Rep_uint8} in code equations
  for conversion functions to avoid exceptions during code generation when the
  target language provides only some of the uint types.
›

lemma uint8_of_uint16_code [code]:
  "uint8_of_uint16 x = Abs_uint8' (ucast (Rep_uint16' x))"
by transfer simp

lemma uint8_of_uint32_code [code]:
  "uint8_of_uint32 x = Abs_uint8' (ucast (Rep_uint32' x))"
by transfer simp

lemma uint8_of_uint64_code [code]:
  "uint8_of_uint64 x = Abs_uint8' (ucast (Rep_uint64' x))"
by transfer simp

lemma uint16_of_uint8_code [code]:
  "uint16_of_uint8 x = Abs_uint16' (ucast (Rep_uint8' x))"
by transfer simp

lemma uint16_of_uint32_code [code]:
  "uint16_of_uint32 x = Abs_uint16' (ucast (Rep_uint32' x))"
by transfer simp

lemma uint16_of_uint64_code [code]:
  "uint16_of_uint64 x = Abs_uint16' (ucast (Rep_uint64' x))"
by transfer simp

lemma uint32_of_uint8_code [code]:
  "uint32_of_uint8 x = Abs_uint32' (ucast (Rep_uint8' x))"
by transfer simp

lemma uint32_of_uint16_code [code]:
  "uint32_of_uint16 x = Abs_uint32' (ucast (Rep_uint16' x))"
by transfer simp

lemma uint32_of_uint64_code [code]:
  "uint32_of_uint64 x = Abs_uint32' (ucast (Rep_uint64' x))"
by transfer simp

lemma uint64_of_uint8_code [code]:
  "uint64_of_uint8 x = Abs_uint64' (ucast (Rep_uint8' x))"
by transfer simp

lemma uint64_of_uint16_code [code]:
  "uint64_of_uint16 x = Abs_uint64' (ucast (Rep_uint16' x))"
by transfer simp

lemma uint64_of_uint32_code [code]:
  "uint64_of_uint32 x = Abs_uint64' (ucast (Rep_uint32' x))"
by transfer simp

end

Theory Native_Cast_Uint

(*  Title:      Native_Cast_Uint.thy
    Author:     Andreas Lochbihler, Digital Asset
*)

theory Native_Cast_Uint imports
  Native_Cast
  Uint
begin

lift_definition uint_of_uint8 :: "uint8  uint" is ucast .
lift_definition uint_of_uint16 :: "uint16  uint" is ucast .
lift_definition uint_of_uint32 :: "uint32  uint" is ucast .
lift_definition uint_of_uint64 :: "uint64  uint" is ucast .

lift_definition uint8_of_uint :: "uint  uint8" is ucast .
lift_definition uint16_of_uint :: "uint  uint16" is ucast .
lift_definition uint32_of_uint :: "uint  uint32" is ucast .
lift_definition uint64_of_uint :: "uint  uint64" is ucast .

code_printing
  constant uint_of_uint8 
  (SML) "Word.fromLarge (Word8.toLarge _)" and
  (Haskell) "(Prelude.fromIntegral _ :: Uint.Word)" and
  (Scala) "((_).toInt & 0xFF)"
| constant uint_of_uint16 
  (SML_word) "Word.fromLarge (Word16.toLarge _)" and
  (Haskell) "(Prelude.fromIntegral _ :: Uint.Word)" and
  (Scala) "(_).toInt"
| constant