1signature polytypicLib = 2sig 3 include Abbrev 4 5(* The types required *) 6type ('a,'b) dict = ('a,'b) Binarymap.dict 7type proof = proofManagerLib.proof; 8 9(* The types defined *) 10 type translation_scheme = 11 {target : hol_type, induction : thm, recursion : thm, 12 left : term, right : term, predicate : term, 13 bottom : term, bottom_thm : thm}; 14 type function = 15 {const : term, definition : thm, 16 induction : (thm * (term * (term * hol_type)) list) option} 17 datatype exception_level = Standard | Fatal | Debug; 18 19(* The exception constructor *) 20 val polyExn : exception_level * string list * string -> exn 21 22 val cstores : (string, hol_type list ref) dict ref; 23 24(* Exception handling functions *) 25 val exn_to_string : exn -> string 26 val Raise : exn -> 'a 27 val isFatal : exn -> bool 28 val wrapException : string -> exn -> 'a 29 val wrapExceptionHOL : string -> exn -> 'a 30 val mkStandardExn : string -> string -> exn 31 val mkFatalExn : string -> string -> exn 32 val mkDebugExn : string -> string -> exn 33 val tryfind_e : exn -> ('a -> 'b) -> 'a list -> 'b 34 val first_e : exn -> ('a -> bool) -> 'a list -> 'a 35 val can : ('a -> 'b) -> 'a -> bool 36 val total : ('a -> 'b) -> 'a -> 'b option 37 val repeat : ('a -> 'a) -> 'a -> 'a 38 val debug : bool ref 39 val assert : string -> (string * ('a -> bool)) list -> 'a -> 'a 40 val guarenteed : ('a -> 'b) -> 'a -> 'b 41 42(* Tracing functions *) 43 val type_trace : int -> string -> unit 44 val xlist_to_string : ('a -> string) -> 'a list -> string 45 val xpair_to_string : ('a -> string) -> ('b -> string) -> 'a * 'b -> string 46 47(* Input testing *) 48 val both : bool * bool -> bool 49 val is_conjunction_of : (term -> bool) -> term -> bool 50 val is_disjunction_of : (term -> bool) -> term -> bool 51 val is_implication_of : (term -> bool) -> (term -> bool) -> term -> bool 52 val is_anything : term -> bool 53 val is_source_function : term -> bool 54 val is_target_function : term -> bool 55 val is_expanded_function : term -> bool 56 val is_single_constructor : translation_scheme -> term -> bool 57 val is_double_term_target : translation_scheme -> term list -> term -> term -> bool 58 val is_double_term_source : term list -> term -> term -> bool 59 60(* List manipulation tools *) 61 val pick_e : exn -> ('a -> 'b) -> 'a list -> 'b * 'a list 62 val bucket_alist : (''a * 'b) list -> (''a * 'b list) list 63 val mappartition : ('a -> 'b) -> 'a list -> 'b list * 'a list 64 val reachable_graph : (''a -> ''a list) -> ''a -> (''a * ''a) list 65 val TC : (''a * ''a) list -> (''a * ''a) list 66 val RTC : (''a * ''a) list -> (''a * ''a) list 67 68(* Term manipulation tools *) 69 val list_mk_cond : (term * term) list -> term -> term 70 val imk_comb : (term * term) -> term 71 val rimk_comb : (term * term) -> term 72 val list_imk_comb : (term * term list) -> term 73 val full_beta_conv : term -> term 74 val full_beta : term -> term 75 76(* Theorem manipulation tools *) 77 val UNDISCH_ONLY : thm -> thm 78 val UNDISCH_ALL_ONLY : thm -> thm 79 val CONJUNCTS_HYP : term -> thm -> thm 80 val CONV_HYP : (term -> thm) -> thm -> thm 81 val CHOOSE_L : term list * thm -> thm -> thm 82 val GEN_THM : term list -> thm -> thm 83 val PROVE_HYP_CHECK : thm -> thm -> thm 84 val ADDR_AND_CONV : term -> term -> thm 85 val ADDL_AND_CONV : term -> term -> thm 86 val MATCH_CONV : thm -> term -> thm 87 val ORDER_FORALL_CONV : term list -> term -> thm 88 val ORDER_EXISTS_CONV : term list -> term -> thm 89 val FUN_EQ_CONV : term -> thm 90 val UNFUN_EQ_CONV : term -> thm 91 val UNBETA_LIST_CONV : term list -> term -> thm 92 val NTH_CONJ_CONV : int -> (term -> thm) -> term -> thm 93 val PUSH_COND_CONV : term -> thm 94 val CASE_SPLIT_CONV : term -> thm 95 val MK_CONJ : thm -> thm -> thm 96 val LIST_MK_CONJ : thm list -> thm 97 val TC_THMS : thm list -> thm list 98 val prove_rec_fn_exists : thm -> term -> thm 99 val UNDISCH_EQ : thm -> thm 100 val UNDISCH_ALL_EQ : thm -> thm 101 val UNDISCH_CONJ : thm -> thm 102 val DISCH_LIST_CONJ : term list -> thm -> thm 103 val DISCH_ALL_CONJ : thm -> thm 104 val MATCH_CONC : thm -> term -> thm 105 106(* Type manipulation tools *) 107 val constructors_of : hol_type -> term list 108 val base26 : int -> char list 109 val base_type : hol_type -> hol_type 110 val cannon_type : hol_type -> hol_type 111 val sub_types : hol_type -> hol_type list 112 val uncurried_subtypes : hol_type -> hol_type list 113 val split_nested_recursive_set : hol_type -> (hol_type * (hol_type list * hol_type list)) list 114 val zip_on_types : ('a -> hol_type) -> ('b -> hol_type) -> 'a list -> 'b list -> ('a * 'b) list 115 val get_type_string : hol_type -> string 116 val SAFE_INST_TYPE : {redex : hol_type, residue : hol_type} list -> thm -> thm 117 val safe_inst : {redex : hol_type, residue : hol_type} list -> term -> term 118 val safe_type_subst : {redex : hol_type, residue : hol_type} list -> hol_type -> hol_type 119 val delete_matching_types : hol_type list -> hol_type -> hol_type 120 val all_types : hol_type -> hol_type list 121 val relevant_types : hol_type -> hol_type list 122 123(* Function splitting *) 124 val RFUN_CONV : thm list -> term -> thm 125 val SPLIT_HFUN_CONV : thm -> term list -> term -> thm list * term list * thm 126 val SPLIT_PAIR_CONV : (term list -> term -> term -> bool) -> term list -> thm -> term -> thm list * term list * thm 127 val SPLIT_FUNCTION_CONV : (term list -> term -> term -> bool) * thm -> thm list -> term -> thm 128 129(* Split function definition *) 130 val build_call_graph : term * term -> term list -> (int * (int list * int list)) list 131 val create_mutual_theorem : (int * (int list * int list)) list -> thm -> thm 132 val instantiate_mutual_theorem : thm -> term list -> thm 133 val create_ind_theorem : (int * (int list * int list)) list -> translation_scheme -> thm 134 val prove_recind_thms_mutual : translation_scheme -> term -> thm * thm 135 val LEQ_REWRITES : term -> term -> thm list -> thm 136 val prove_induction_recursion_thms : translation_scheme -> term -> thm * (term * term) list * thm 137 138(* The function and theorem database *) 139 val get_translation_scheme : hol_type -> translation_scheme 140 val exists_translation_precise : hol_type -> hol_type -> bool 141 val exists_translation : hol_type -> hol_type -> bool 142 val add_translation : hol_type -> hol_type -> unit 143 val add_translation_precise : hol_type -> hol_type -> unit 144 val get_translation_precise : hol_type -> hol_type -> (string,function) dict ref 145 val get_translation : hol_type -> hol_type -> (string,function) dict ref 146 val get_theorems_precise : hol_type -> hol_type -> (string, thm) dict ref 147 val get_theorems : hol_type -> hol_type -> (string, thm) dict ref 148 val get_translation_types : hol_type -> hol_type list 149 val add_translation_scheme : hol_type -> thm -> thm -> unit 150 val clearCoding : unit -> unit 151 val clearSource : unit -> unit 152 val most_precise_type : (hol_type -> bool) -> hol_type -> hol_type 153 154(* Function retrieval *) 155 val exists_coding_function_precise : hol_type -> hol_type -> string -> bool 156 val exists_coding_function : hol_type -> hol_type -> string -> bool 157 val get_coding_function_precise : hol_type -> hol_type -> string -> function 158 val get_coding_function : hol_type -> hol_type -> string -> function 159 val get_coding_function_def : hol_type -> hol_type -> string -> thm 160 val get_coding_function_const : hol_type -> hol_type -> string -> term 161 val get_coding_function_induction : hol_type -> hol_type -> string -> thm * (term * (term * hol_type)) list 162 val get_coding_function_precise_def : hol_type -> hol_type -> string -> thm 163 val get_coding_function_precise_const : hol_type -> hol_type -> string -> term 164 val get_coding_function_precise_induction : hol_type -> hol_type -> string -> thm * (term * (term * hol_type)) list 165 val add_coding_function_precise : hol_type -> hol_type -> string -> function -> unit 166 val add_coding_function : hol_type -> hol_type -> string -> function -> unit 167 val exists_source_function_precise : hol_type -> string -> bool 168 val exists_source_function : hol_type -> string -> bool 169 val get_source_function_precise : hol_type -> string -> function 170 val get_source_function : hol_type -> string -> function 171 val get_source_function_def : hol_type -> string -> thm 172 val get_source_function_const : hol_type -> string -> term 173 val get_source_function_induction : hol_type -> string -> thm * (term * (term * hol_type)) list 174 val get_source_function_precise_def : hol_type -> string -> thm 175 val get_source_function_precise_const : hol_type -> string -> term 176 val get_source_function_precise_induction : hol_type -> string -> thm * (term * (term * hol_type)) list 177 val add_source_function_precise : hol_type -> string -> function -> unit 178 val add_source_function : hol_type -> string -> function -> unit 179 180(* Theorem retrieval *) 181 val exists_coding_theorem_precise : hol_type -> hol_type -> string -> bool 182 val exists_coding_theorem : hol_type -> hol_type -> string -> bool 183 val add_coding_theorem_precise : hol_type -> hol_type -> string -> thm -> unit 184 val add_coding_theorem : hol_type -> hol_type -> string -> thm -> unit 185 val get_coding_theorem_precise : hol_type -> hol_type -> string -> thm 186 val get_coding_theorem : hol_type -> hol_type -> string -> thm 187 val exists_source_theorem_precise : hol_type -> string -> bool 188 val exists_source_theorem : hol_type -> string -> bool 189 val get_source_theorem_precise : hol_type -> string -> thm 190 val get_source_theorem : hol_type -> string -> thm 191 val add_source_theorem_precise : hol_type -> string -> thm -> unit 192 val add_source_theorem : hol_type -> string -> thm -> unit 193 val remove_source_theorem_precise : hol_type -> string -> unit 194 val remove_coding_theorem_precise : hol_type -> hol_type -> string -> unit 195 196(* Function creation tools *) 197 val inst_function_def : (hol_type -> thm) -> (hol_type -> term) -> hol_type -> thm 198 val expanded_function_def : (term -> thm) -> (term -> thm) -> (hol_type -> thm) -> hol_type -> term list -> thm 199 val mk_split_source_function : (hol_type -> term) -> (hol_type -> thm) -> (hol_type -> term) -> (term -> thm) -> (term -> thm) -> hol_type -> thm * thm 200 val mk_split_target_function : (hol_type -> term) -> (hol_type -> thm) -> (hol_type -> term) -> (term -> thm) -> (term -> thm) -> 201 translation_scheme -> hol_type -> (thm * (term * term) list * thm) * thm 202 203(* Removal of function splits *) 204 val MATCH_IND_TERM : term -> thm -> thm 205 val strengthen_proof_term : thm list -> term -> thm 206 val prove_split_term : (term * (term * hol_type)) list -> thm -> thm -> thm * term -> term -> thm 207 val prove_all_split_terms : (hol_type -> thm * (term * (term * hol_type)) list) * (hol_type -> thm) * (term -> thm) * (term -> thm) * thm * term -> 208 (term * hol_type) list -> thm -> thm list * thm 209 val remove_hyp_terms : thm -> thm list -> thm list * thm -> thm 210 val match_mapping : thm -> (term * term) list -> (hol_type -> term) -> thm -> hol_type -> (term * (term * hol_type)) list 211 val unsplit_function : (hol_type -> thm * (term * (term * hol_type)) list) -> (hol_type -> thm) -> (hol_type -> term) -> 212 (term -> thm) -> (term -> thm) -> thm * term -> hol_type -> thm * thm -> thm 213 214(* Full function creation *) 215 val mk_source_functions : string -> (hol_type -> term) -> (hol_type -> term) -> (term -> thm) -> (term -> thm) -> hol_type -> unit 216 val mk_coding_functions : string -> (hol_type -> term) -> (hol_type -> term) -> (term -> thm) -> (term -> thm) -> hol_type -> hol_type -> unit 217 val mk_target_functions : string -> (hol_type -> term) -> (hol_type -> term) -> (term -> thm) -> (term -> thm) -> hol_type -> hol_type -> unit 218 219(* Automatic generation of functions *) 220 val add_coding_function_generator : hol_type -> string -> (hol_type -> bool) -> (hol_type -> function) -> unit 221 val add_source_function_generator : string -> (hol_type -> bool) -> (hol_type -> function) -> unit 222 val generate_coding_function : hol_type -> string -> hol_type -> unit 223 val generate_source_function : string -> hol_type -> unit 224 val add_compound_coding_function_generator : string -> (hol_type -> term) -> (hol_type -> term) -> (term -> thm) -> (term -> thm) -> hol_type -> unit 225 val add_compound_target_function_generator : string -> (hol_type -> term) -> (hol_type -> term) -> (term -> thm) -> (term -> thm) -> hol_type -> unit 226 val add_compound_source_function_generator : string -> (hol_type -> term) -> (hol_type -> term) -> (term -> thm) -> (term -> thm) -> unit 227 228(* Automatic generation of theorems *) 229 val generate_coding_theorem : hol_type -> string -> hol_type -> thm 230 val generate_source_theorem : string -> hol_type -> thm 231 val set_coding_theorem_conclusion : hol_type -> string -> (hol_type -> term) -> unit 232 val set_source_theorem_conclusion : string -> (hol_type -> term) -> unit 233 val get_coding_theorem_conclusion : hol_type -> string -> (hol_type -> term) 234 val get_source_theorem_conclusion : string -> (hol_type -> term) 235 val exists_coding_theorem_conclusion : hol_type -> string -> bool 236 val exists_source_theorem_conclusion : string -> bool 237 val make_predicate_map : thm -> (term * term list) list 238 val inductive_coding_goal : string -> (hol_type -> term) -> hol_type -> hol_type -> (term -> thm) -> proof 239 val inductive_source_goal : string -> (hol_type -> term) -> hol_type -> (term -> thm) -> proof 240 val add_inductive_coding_theorem_generator : string -> string -> hol_type -> (term -> thm) -> (hol_type -> tactic) -> unit 241 val add_inductive_source_theorem_generator : string -> string -> (term -> thm) -> (hol_type -> tactic) -> unit 242 val add_tactic_coding_theorem_generator : string -> (hol_type -> bool) -> (hol_type -> tactic) -> hol_type -> unit 243 val add_tactic_source_theorem_generator : string -> (hol_type -> bool) -> (hol_type -> tactic) -> unit 244 val add_rule_coding_theorem_generator : string -> (hol_type -> bool) -> (hol_type -> thm) -> hol_type -> unit 245 val add_rule_source_theorem_generator : string -> (hol_type -> bool) -> (hol_type -> thm) -> unit 246 247end 248