Theory Code_Bit

theory Code_Bit
imports  "$ISABELLE_HOME/src/HOL/Library/Bit"
begin

text{*Implementation for the field of integer numbers module 2.
Experimentally we have checked that this implementation is faster than 
using booleans or implementing the operations by tables.*}

code_datatype "0::bit" "(1::bit)"

code_type bit
  (SML "IntInf.int")
code_const "0::bit"
  (SML "0")
code_const "1::bit"
  (SML "1")

code_const "op + :: bit => bit => bit"
  (SML "IntInf.rem ((IntInf.+ ((_), (_))), 2)")
code_const "op * :: bit => bit => bit"
  (SML "IntInf.* ((_), (_))")
code_const "op / :: bit => bit => bit"
  (SML "IntInf.* ((_), (_))")
end