Structure bitSyntax

signature bitSyntax =
sig

  include Abbrev

  val bit_modify_tm  : term
  val bit_reverse_tm : term
  val bit_tm         : term
  val bits_tm        : term
  val bitv_tm        : term
  val bitwise_tm     : term
  val div_2exp_tm    : term
  val divmod_2exp_tm : term
  val log2_tm        : term
  val mod_2exp_eq_tm : term
  val mod_2exp_tm    : term
  val mod_2exp_max_tm: term
  val sbit_tm        : term
  val sign_extend_tm : term
  val slice_tm       : term
  val times_2exp_tm  : term

  val mk_bit         : term * term -> term
  val mk_bit_modify  : term * term * term -> term
  val mk_bit_reverse : term * term -> term
  val mk_bits        : term * term * term -> term
  val mk_bitv        : term * term -> term
  val mk_bitwise     : term * term * term * term -> term
  val mk_div_2exp    : term * term -> term
  val mk_divmod_2exp : term * term -> term
  val mk_log2        : term -> term
  val mk_mod_2exp    : term * term -> term
  val mk_mod_2exp_eq : term * term * term -> term
  val mk_mod_2exp_max: term * term -> term
  val mk_sbit        : term * term -> term
  val mk_sign_extend : term * term * term -> term
  val mk_slice       : term * term * term -> term
  val mk_times_2exp  : term * term -> term

  val dest_bit         : term -> term * term
  val dest_bit_modify  : term -> term * term * term
  val dest_bit_reverse : term -> term * term
  val dest_bits        : term -> term * term * term
  val dest_bitv        : term -> term * term
  val dest_bitwise     : term -> term * term * term * term
  val dest_div_2exp    : term -> term * term
  val dest_divmod_2exp : term -> term * term
  val dest_log2        : term -> term
  val dest_mod_2exp    : term -> term * term
  val dest_mod_2exp_eq : term -> term * term * term
  val dest_mod_2exp_max: term -> term * term
  val dest_sbit        : term -> term * term
  val dest_sign_extend : term -> term * term * term
  val dest_slice       : term -> term * term * term
  val dest_times_2exp  : term -> term * term

  val is_bit         : term -> bool
  val is_bit_modify  : term -> bool
  val is_bit_reverse : term -> bool
  val is_bits        : term -> bool
  val is_bitv        : term -> bool
  val is_bitwise     : term -> bool
  val is_div_2exp    : term -> bool
  val is_divmod_2exp : term -> bool
  val is_log2        : term -> bool
  val is_mod_2exp    : term -> bool
  val is_mod_2exp_eq : term -> bool
  val is_mod_2exp_max: term -> bool
  val is_sbit        : term -> bool
  val is_sign_extend : term -> bool
  val is_slice       : term -> bool
  val is_times_2exp  : term -> bool

end

HOL 4, Kananaskis-13