1signature encodeLib = 2sig 3 include Abbrev 4 5 val construct_bottom_value : 6 (hol_type -> bool) -> term -> hol_type -> term 7 val set_bottom_value : hol_type -> term -> unit 8 val target_bottom_value : hol_type -> term -> hol_type -> term 9 val get_encode_type : hol_type -> hol_type -> hol_type 10 val get_decode_type : hol_type -> hol_type -> hol_type 11 val get_detect_type : hol_type -> hol_type -> hol_type 12 val get_map_type : hol_type -> hol_type 13 val get_all_type : hol_type -> hol_type 14 val get_fix_type : hol_type -> hol_type -> hol_type 15 val mk_encode_var : hol_type -> hol_type -> term 16 val mk_decode_var : hol_type -> hol_type -> term 17 val mk_detect_var : hol_type -> hol_type -> term 18 val mk_map_var : hol_type -> term 19 val mk_all_var : hol_type -> term 20 val mk_fix_var : hol_type -> hol_type -> term 21 val get_encode_const : hol_type -> hol_type -> term 22 val get_decode_const : hol_type -> hol_type -> term 23 val get_map_const : hol_type -> term 24 val get_all_const : hol_type -> term 25 val get_fix_const : hol_type -> hol_type -> term 26 val get_detect_const : hol_type -> hol_type -> term 27 val get_all_function : hol_type -> term 28 val get_decode_function : hol_type -> hol_type -> term 29 val get_map_function : hol_type -> term 30 val get_fix_function : hol_type -> hol_type -> term 31 val get_detect_function : hol_type -> hol_type -> term 32 val get_encode_function : hol_type -> hol_type -> term 33 val mk_detect_term : hol_type -> hol_type -> term 34 val mk_decode_term : hol_type -> hol_type -> term 35 val mk_fix_term : hol_type -> hol_type -> term 36 val mk_encode_term : hol_type -> hol_type -> term 37 val mk_map_term : hol_type -> term 38 val mk_all_term : hol_type -> term 39 val ENCODE_CONV : thm -> term -> thm 40 val DETECT_CONV : hol_type -> term -> thm 41 val DECODE_CONV : hol_type -> term -> thm 42 val FIX_CONV : hol_type -> term -> thm 43 val mk_encodes : hol_type -> hol_type -> unit 44 val CONSOLIDATE_CONV : (term -> term) -> term -> thm 45 val mk_decodes : hol_type -> hol_type -> unit 46 val mk_detects : hol_type -> hol_type -> unit 47 val mk_maps : hol_type -> unit 48 val mk_alls : hol_type -> unit 49 val mk_fixs : hol_type -> hol_type -> unit 50 val type_vars_avoiding_itself : term -> hol_type -> hol_type list 51 val check_function : (hol_type -> term) -> hol_type -> term 52 val get_sub_types : hol_type -> hol_type -> hol_type list 53 val wrap_full : string -> hol_type -> exn -> 'a 54 55 val mk_encode_decode_map_conc : hol_type -> hol_type -> term 56 val mk_encode_map_encode_conc : hol_type -> hol_type -> term 57 val mk_map_compose_conc : hol_type -> term 58 val mk_decode_encode_fix_conc : hol_type -> hol_type -> term 59 val mk_encode_detect_all_conc : hol_type -> hol_type -> term 60 val mk_map_id_conc : hol_type -> term 61 val mk_all_id_conc : hol_type -> term 62 val mk_fix_id_conc : hol_type -> hol_type -> term 63 val mk_general_detect_conc : hol_type -> hol_type -> term 64 val mk_encode_decode_conc : hol_type -> hol_type -> term 65 val mk_encode_detect_conc : hol_type -> hol_type -> term 66 val mk_decode_encode_conc : hol_type -> hol_type -> term 67 val FULL_ENCODE_DECODE_MAP_THM : hol_type -> hol_type -> thm 68 val FULL_ENCODE_DETECT_ALL_THM : hol_type -> hol_type -> thm 69 val FULL_ENCODE_MAP_ENCODE_THM : hol_type -> hol_type -> thm 70 val FULL_DECODE_ENCODE_FIX_THM : hol_type -> hol_type -> thm 71 val FULL_MAP_COMPOSE_THM : hol_type -> thm 72 val FULL_MAP_ID_THM : hol_type -> thm 73 val FULL_ALL_ID_THM : hol_type -> thm 74 val FULL_FIX_ID_THM : hol_type -> hol_type -> thm 75 val FULL_ENCODE_DECODE_THM : hol_type -> hol_type -> thm 76 val FULL_ENCODE_DETECT_THM : hol_type -> hol_type -> thm 77 val FULL_DECODE_ENCODE_THM : hol_type -> hol_type -> thm 78 val ENCODER_CONV : term -> thm 79 val APP_MAP_CONV : term -> thm 80 val APP_ALL_CONV : term -> thm 81 val DECODE_PAIR_CONV : term -> thm 82 val DETECT_PAIR_CONV : hol_type -> term -> thm 83 val encode_decode_map_tactic : hol_type -> hol_type -> term list * term -> 84 (term list * term) list * (thm list -> thm) 85 val encode_map_encode_tactic : hol_type -> hol_type -> term list * term -> 86 (term list * term) list * (thm list -> thm) 87 val map_compose_tactic : hol_type -> term list * term -> (term list * term) list * (thm list -> thm) 88 val encode_detect_all_tactic : hol_type -> hol_type -> term list * term -> 89 (term list * term) list * (thm list -> thm) 90 val LET_RAND_CONV : term -> term -> thm 91 val decode_encode_fix_tactic : hol_type -> 'a -> term list * term -> 92 (term list * term) list * (thm list -> thm) 93 val fix_id_tactic : hol_type -> hol_type -> term list * term -> 94 (term list * term) list * (thm list -> thm) 95 val general_detect_tactic : hol_type -> hol_type -> term list * term -> 96 (term list * term) list * (thm list -> thm) 97 val detect_dead_rule : hol_type -> hol_type -> thm 98 val all_id_tactic : 'a -> term list * term -> (term list * term) list * (thm list -> thm) 99 val map_id_tactic : 'a -> term list * term -> (term list * term) list * (thm list -> thm) 100 val initialise_source_function_generators : unit -> unit 101 val initialise_coding_function_generators : hol_type -> unit 102 val initialise_coding_theorem_generators : hol_type -> unit 103 104 val mk_destructors : hol_type -> hol_type -> (thm list * thm list) 105 106 val encode_type : hol_type -> hol_type -> unit 107 val gen_encode_function : hol_type -> hol_type -> term 108 val gen_decode_function : hol_type -> hol_type -> term 109 val gen_detect_function : hol_type -> hol_type -> term 110 111 val MK_FST : thm -> thm 112 val MK_SND : thm -> thm 113 114 val CONSOLIDATE_CONV_data : (((term -> term) * term) option) ref 115 116 val predicate_equivalence : hol_type -> hol_type -> thm 117end