Structure wordsSyntax
signature wordsSyntax =
sig
include Abbrev
type num = Arbnum.num
val mk_word_type : hol_type -> hol_type
val dest_word_type : hol_type -> hol_type
val is_word_type : hol_type -> bool
val dim_of : term -> hol_type
val size_of : term -> num
val mk_int_word_type : int -> hol_type
val mk_word : num * num -> term
val mk_wordi : num * int -> term
val mk_wordii : int * int -> term
val dest_mod_word_literal : term -> Arbnum.num * Arbnum.num
val dest_word_literal : term -> Arbnum.num
val is_word_literal : term -> bool
val uint_of_word : term -> int
val add_with_carry_tm : term
val bit_count_tm : term
val bit_count_upto_tm : term
val bit_field_insert_tm : term
val bit_set_tm : term
val concat_word_list_tm : term
val dimindex_tm : term
val dimword_tm : term
val fcp_index_tm : term
val int_max_tm : term
val int_min_tm : term
val l2w_tm : term
val n2w_tm : term
val nzcv_tm : term
val reduce_and_tm : term
val reduce_nand_tm : term
val reduce_nor_tm : term
val reduce_or_tm : term
val reduce_xnor_tm : term
val reduce_xor_tm : term
val s2w_tm : term
val saturate_add_tm : term
val saturate_mul_tm : term
val saturate_n2w_tm : term
val saturate_sub_tm : term
val saturate_w2w_tm : term
val sw2sw_tm : term
val uint_max_tm : term
val w2l_tm : term
val w2n_tm : term
val w2s_tm : term
val w2w_tm : term
val word_1comp_tm : term
val word_2comp_tm : term
val word_H_tm : term
val word_L2_tm : term
val word_L_tm : term
val word_T_tm : term
val word_abs_tm : term
val word_add_tm : term
val word_and_tm : term
val word_asr_bv_tm : term
val word_asr_tm : term
val word_bit_tm : term
val word_bits_tm : term
val word_compare_tm : term
val word_concat_tm : term
val word_div_tm : term
val word_extract_tm : term
val word_from_bin_list_tm : term
val word_from_bin_string_tm : term
val word_from_dec_list_tm : term
val word_from_dec_string_tm : term
val word_from_hex_list_tm : term
val word_from_hex_string_tm : term
val word_from_oct_list_tm : term
val word_from_oct_string_tm : term
val word_ge_tm : term
val word_gt_tm : term
val word_hi_tm : term
val word_hs_tm : term
val word_join_tm : term
val word_le_tm : term
val word_len_tm : term
val word_lo_tm : term
val word_log2_tm : term
val word_ls_tm : term
val word_lsb_tm : term
val word_lsl_bv_tm : term
val word_lsl_tm : term
val word_lsr_bv_tm : term
val word_lsr_tm : term
val word_lt_tm : term
val word_max_tm : term
val word_min_tm : term
val word_mod_tm : term
val word_modify_tm : term
val word_msb_tm : term
val word_mul_tm : term
val word_nand_tm : term
val word_nor_tm : term
val word_or_tm : term
val word_quot_tm : term
val word_reduce_tm : term
val word_rem_tm : term
val word_replicate_tm : term
val word_reverse_tm : term
val word_rol_bv_tm : term
val word_rol_tm : term
val word_ror_bv_tm : term
val word_ror_tm : term
val word_rrx_tm : term
val word_sign_extend_tm : term
val word_slice_tm : term
val word_smax_tm : term
val word_smin_tm : term
val word_sub_tm : term
val word_to_bin_list_tm : term
val word_to_bin_string_tm : term
val word_to_dec_list_tm : term
val word_to_dec_string_tm : term
val word_to_hex_list_tm : term
val word_to_hex_string_tm : term
val word_to_oct_list_tm : term
val word_to_oct_string_tm : term
val word_xnor_tm : term
val word_xor_tm : term
val dest_add_with_carry : term -> term * term * term
val dest_bit_count : term -> term
val dest_bit_count_upto : term -> term * term
val dest_bit_field_insert : term -> term * term * term * term
val dest_bit_set : term -> term * term
val dest_concat_word_list : term -> term * hol_type
val dest_dimindex : term -> hol_type
val dest_dimword : term -> hol_type
val dest_index : term -> term * term
val dest_int_max : term -> hol_type
val dest_int_min : term -> hol_type
val dest_l2w : term -> term * term * hol_type
val dest_n2w : term -> term * hol_type
val dest_nzcv : term -> term * term
val dest_reduce_and : term -> term
val dest_reduce_nand : term -> term
val dest_reduce_nor : term -> term
val dest_reduce_or : term -> term
val dest_reduce_xnor : term -> term
val dest_reduce_xor : term -> term
val dest_s2w : term -> term * term * term * hol_type
val dest_saturate_add : term -> term * term
val dest_saturate_mul : term -> term * term
val dest_saturate_n2w : term -> term * hol_type
val dest_saturate_sub : term -> term * term
val dest_saturate_w2w : term -> term * hol_type
val dest_sw2sw : term -> term * hol_type
val dest_uint_max : term -> hol_type
val dest_w2l : term -> term * term
val dest_w2n : term -> term
val dest_w2s : term -> term * term * term
val dest_w2w : term -> term * hol_type
val dest_word_1comp : term -> term
val dest_word_2comp : term -> term
val dest_word_H : term -> hol_type
val dest_word_L : term -> hol_type
val dest_word_L2 : term -> hol_type
val dest_word_T : term -> hol_type
val dest_word_abs : term -> term
val dest_word_add : term -> term * term
val dest_word_and : term -> term * term
val dest_word_asr : term -> term * term
val dest_word_asr_bv : term -> term * term
val dest_word_bit : term -> term * term
val dest_word_bits : term -> term * term * term
val dest_word_compare : term -> term * term
val dest_word_concat : term -> term * term
val dest_word_div : term -> term * term
val dest_word_extract : term -> term * term * term * hol_type
val dest_word_from_bin_list : term -> term * hol_type
val dest_word_from_bin_string : term -> term * hol_type
val dest_word_from_dec_list : term -> term * hol_type
val dest_word_from_dec_string : term -> term * hol_type
val dest_word_from_hex_list : term -> term * hol_type
val dest_word_from_hex_string : term -> term * hol_type
val dest_word_from_oct_list : term -> term * hol_type
val dest_word_from_oct_string : term -> term * hol_type
val dest_word_ge : term -> term * term
val dest_word_gt : term -> term * term
val dest_word_hi : term -> term * term
val dest_word_hs : term -> term * term
val dest_word_join : term -> term * term
val dest_word_le : term -> term * term
val dest_word_len : term -> term
val dest_word_lo : term -> term * term
val dest_word_log2 : term -> term
val dest_word_ls : term -> term * term
val dest_word_lsb : term -> term
val dest_word_lsl : term -> term * term
val dest_word_lsl_bv : term -> term * term
val dest_word_lsr : term -> term * term
val dest_word_lsr_bv : term -> term * term
val dest_word_lt : term -> term * term
val dest_word_max : term -> term * term
val dest_word_min : term -> term * term
val dest_word_mod : term -> term * term
val dest_word_modify : term -> term * term
val dest_word_msb : term -> term
val dest_word_mul : term -> term * term
val dest_word_nand : term -> term * term
val dest_word_nor : term -> term * term
val dest_word_or : term -> term * term
val dest_word_quot : term -> term * term
val dest_word_reduce : term -> term * term
val dest_word_rem : term -> term * term
val dest_word_replicate : term -> term * term
val dest_word_reverse : term -> term
val dest_word_rol : term -> term * term
val dest_word_rol_bv : term -> term * term
val dest_word_ror : term -> term * term
val dest_word_ror_bv : term -> term * term
val dest_word_rrx : term -> term * term
val dest_word_sign_extend : term -> term * term
val dest_word_slice : term -> term * term * term
val dest_word_smax : term -> term * term
val dest_word_smin : term -> term * term
val dest_word_sub : term -> term * term
val dest_word_to_bin_list : term -> term
val dest_word_to_bin_string : term -> term
val dest_word_to_dec_list : term -> term
val dest_word_to_dec_string : term -> term
val dest_word_to_hex_list : term -> term
val dest_word_to_hex_string : term -> term
val dest_word_to_oct_list : term -> term
val dest_word_to_oct_string : term -> term
val dest_word_xnor : term -> term * term
val dest_word_xor : term -> term * term
val is_add_with_carry : term -> bool
val is_bit_count : term -> bool
val is_bit_count_upto : term -> bool
val is_bit_field_insert : term -> bool
val is_bit_set : term -> bool
val is_concat_word_list : term -> bool
val is_dimindex : term -> bool
val is_dimword : term -> bool
val is_index : term -> bool
val is_int_max : term -> bool
val is_int_min : term -> bool
val is_l2w : term -> bool
val is_n2w : term -> bool
val is_nzcv : term -> bool
val is_reduce_and : term -> bool
val is_reduce_nand : term -> bool
val is_reduce_nor : term -> bool
val is_reduce_or : term -> bool
val is_reduce_xnor : term -> bool
val is_reduce_xor : term -> bool
val is_s2w : term -> bool
val is_saturate_add : term -> bool
val is_saturate_mul : term -> bool
val is_saturate_n2w : term -> bool
val is_saturate_sub : term -> bool
val is_saturate_w2w : term -> bool
val is_sw2sw : term -> bool
val is_uint_max : term -> bool
val is_w2l : term -> bool
val is_w2n : term -> bool
val is_w2s : term -> bool
val is_w2w : term -> bool
val is_word_1comp : term -> bool
val is_word_2comp : term -> bool
val is_word_H : term -> bool
val is_word_L : term -> bool
val is_word_L2 : term -> bool
val is_word_T : term -> bool
val is_word_abs : term -> bool
val is_word_add : term -> bool
val is_word_and : term -> bool
val is_word_asr : term -> bool
val is_word_asr_bv : term -> bool
val is_word_bit : term -> bool
val is_word_bits : term -> bool
val is_word_compare : term -> bool
val is_word_concat : term -> bool
val is_word_div : term -> bool
val is_word_extract : term -> bool
val is_word_from_bin_list : term -> bool
val is_word_from_bin_string : term -> bool
val is_word_from_dec_list : term -> bool
val is_word_from_dec_string : term -> bool
val is_word_from_hex_list : term -> bool
val is_word_from_hex_string : term -> bool
val is_word_from_oct_list : term -> bool
val is_word_from_oct_string : term -> bool
val is_word_ge : term -> bool
val is_word_gt : term -> bool
val is_word_hi : term -> bool
val is_word_hs : term -> bool
val is_word_join : term -> bool
val is_word_le : term -> bool
val is_word_len : term -> bool
val is_word_lo : term -> bool
val is_word_log2 : term -> bool
val is_word_ls : term -> bool
val is_word_lsb : term -> bool
val is_word_lsl : term -> bool
val is_word_lsl_bv : term -> bool
val is_word_lsr : term -> bool
val is_word_lsr_bv : term -> bool
val is_word_lt : term -> bool
val is_word_max : term -> bool
val is_word_min : term -> bool
val is_word_mod : term -> bool
val is_word_modify : term -> bool
val is_word_msb : term -> bool
val is_word_mul : term -> bool
val is_word_nand : term -> bool
val is_word_nor : term -> bool
val is_word_or : term -> bool
val is_word_quot : term -> bool
val is_word_reduce : term -> bool
val is_word_rem : term -> bool
val is_word_replicate : term -> bool
val is_word_reverse : term -> bool
val is_word_rol : term -> bool
val is_word_rol_bv : term -> bool
val is_word_ror : term -> bool
val is_word_ror_bv : term -> bool
val is_word_rrx : term -> bool
val is_word_sign_extend : term -> bool
val is_word_slice : term -> bool
val is_word_smax : term -> bool
val is_word_smin : term -> bool
val is_word_sub : term -> bool
val is_word_to_bin_list : term -> bool
val is_word_to_bin_string : term -> bool
val is_word_to_dec_list : term -> bool
val is_word_to_dec_string : term -> bool
val is_word_to_hex_list : term -> bool
val is_word_to_hex_string : term -> bool
val is_word_to_oct_list : term -> bool
val is_word_to_oct_string : term -> bool
val is_word_xnor : term -> bool
val is_word_xor : term -> bool
val mk_add_with_carry : term * term * term -> term
val mk_bit_count_upto : term * term -> term
val mk_bit_count : term -> term
val mk_bit_field_insert : term * term * term * term -> term
val mk_bit_set : term * term -> term
val mk_concat_word_list : term * hol_type -> term
val mk_dimindex : hol_type -> term
val mk_dimword : hol_type -> term
val mk_index : term * term -> term
val mk_int_max : hol_type -> term
val mk_int_min : hol_type -> term
val mk_l2w : term * term * hol_type -> term
val mk_n2w : term * hol_type -> term
val mk_nzcv : term * term -> term
val mk_reduce_and : term -> term
val mk_reduce_nand : term -> term
val mk_reduce_nor : term -> term
val mk_reduce_or : term -> term
val mk_reduce_xnor : term -> term
val mk_reduce_xor : term -> term
val mk_s2w : term * term * term * hol_type -> term
val mk_saturate_add : term * term -> term
val mk_saturate_mul : term * term -> term
val mk_saturate_n2w : term * hol_type -> term
val mk_saturate_sub : term * term -> term
val mk_saturate_w2w : term * hol_type -> term
val mk_sw2sw : term * hol_type -> term
val mk_uint_max : hol_type -> term
val mk_w2l : term * term -> term
val mk_w2n : term -> term
val mk_w2s : term * term * term -> term
val mk_w2w : term * hol_type -> term
val mk_word_1comp : term -> term
val mk_word_2comp : term -> term
val mk_word_H : hol_type -> term
val mk_word_L : hol_type -> term
val mk_word_L2 : hol_type -> term
val mk_word_T : hol_type -> term
val mk_word_abs : term -> term
val mk_word_add : term * term -> term
val mk_word_and : term * term -> term
val mk_word_asr : term * term -> term
val mk_word_asr_bv : term * term -> term
val mk_word_bit : term * term -> term
val mk_word_bits : term * term * term -> term
val mk_word_compare : term * term -> term
val mk_word_concat : term * term -> term
val mk_word_div : term * term -> term
val mk_word_extract : term * term * term * hol_type -> term
val mk_word_from_bin_list : term * hol_type -> term
val mk_word_from_bin_string : term * hol_type -> term
val mk_word_from_dec_list : term * hol_type -> term
val mk_word_from_dec_string : term * hol_type -> term
val mk_word_from_hex_list : term * hol_type -> term
val mk_word_from_hex_string : term * hol_type -> term
val mk_word_from_oct_list : term * hol_type -> term
val mk_word_from_oct_string : term * hol_type -> term
val mk_word_ge : term * term -> term
val mk_word_gt : term * term -> term
val mk_word_hi : term * term -> term
val mk_word_hs : term * term -> term
val mk_word_join : term * term -> term
val mk_word_le : term * term -> term
val mk_word_len : term -> term
val mk_word_lo : term * term -> term
val mk_word_log2 : term -> term
val mk_word_ls : term * term -> term
val mk_word_lsb : term -> term
val mk_word_lsl : term * term -> term
val mk_word_lsl_bv : term * term -> term
val mk_word_lsr : term * term -> term
val mk_word_lsr_bv : term * term -> term
val mk_word_lt : term * term -> term
val mk_word_max : term * term -> term
val mk_word_min : term * term -> term
val mk_word_mod : term * term -> term
val mk_word_modify : term * term -> term
val mk_word_msb : term -> term
val mk_word_mul : term * term -> term
val mk_word_nand : term * term -> term
val mk_word_nor : term * term -> term
val mk_word_or : term * term -> term
val mk_word_quot : term * term -> term
val mk_word_reduce : term * term -> term
val mk_word_rem : term * term -> term
val mk_word_replicate : term * term -> term
val mk_word_replicate_ty : term * term * hol_type -> term
val mk_word_reverse : term -> term
val mk_word_rol : term * term -> term
val mk_word_rol_bv : term * term -> term
val mk_word_ror : term * term -> term
val mk_word_ror_bv : term * term -> term
val mk_word_rrx : term * term -> term
val mk_word_sign_extend : term * term -> term
val mk_word_slice : term * term * term -> term
val mk_word_smax : term * term -> term
val mk_word_smin : term * term -> term
val mk_word_sub : term * term -> term
val mk_word_to_bin_list : term -> term
val mk_word_to_bin_string : term -> term
val mk_word_to_dec_list : term -> term
val mk_word_to_dec_string : term -> term
val mk_word_to_hex_list : term -> term
val mk_word_to_hex_string : term -> term
val mk_word_to_oct_list : term -> term
val mk_word_to_oct_string : term -> term
val mk_word_xnor : term * term -> term
val mk_word_xor : term * term -> term
end
HOL 4, Kananaskis-13