1signature quantHeuristicsLibSimple = 2sig 3 include Abbrev 4 5 (************************************) 6 (* Main functionality *) 7 (************************************) 8 9 (* SIMPLE_QUANT_INSTANTIATE_CONV implements functionality for 10 finding GAP guesses fast. Moreover, the found instantiations may 11 not contain free variables. As such, the functionality is similar 12 to Unwind. It allows more syntax than Unwind and can be 13 extended. It is much faster than the general quantifier 14 instantiations heuristics, but also far less powerful. *) 15 16 val SIMPLE_QUANT_INSTANTIATE_CONV : conv 17 val SIMPLE_QUANT_INST_ss : simpLib.ssfrag 18 val SIMPLE_QUANT_INSTANTIATE_TAC : tactic 19 20 val SIMPLE_EXISTS_INSTANTIATE_CONV : conv 21 val SIMPLE_FORALL_INSTANTIATE_CONV : conv 22 val SIMPLE_UEXISTS_INSTANTIATE_CONV : conv 23 val SIMPLE_SOME_INSTANTIATE_CONV : conv 24 val SIMPLE_SELECT_INSTANTIATE_CONV : conv 25 26 27 28 (************************************) 29 (* Extensions *) 30 (************************************) 31 32 (* A simple_guess_seaech_fun is a function that searches a guess. Given a 33 34 - avoid : a set of variables to avoid in the instantiation 35 - ty : search a guess for either universal or existential quantification 36 - v : variable to search an instance for 37 - tm : a term to search an instantiation in 38 39 it (if it succeeds) results in a theorem of the form 40 41 |- SIMPLE_GUESS_EXISTS v i tm 42 43 or 44 45 |- SIMPLE_GUESS_FORALL v i tm 46 47 depending on the value of ty. Moreover i does not contain any variable from avoid. 48 49 Having an additional callback argument to search guesses for subterms is also useful. 50 combine_sgsfwcs then allows combining a list of such search functions with callback 51 into a single search function. 52 *) 53 54 datatype simple_guess_type = sgty_exists | sgty_forall 55 type simple_guess_search_fun = term HOLset.set -> simple_guess_type -> term -> term -> thm 56 type simple_guess_search_fun_with_callback = simple_guess_search_fun -> simple_guess_search_fun 57 58 val combine_sgsfwcs : simple_guess_search_fun_with_callback list -> simple_guess_search_fun 59 60 (* search functions for common operations *) 61 val sgsfwc_eq : simple_guess_search_fun_with_callback (* v = _ / _ = v *) 62 val sgsfwc_eq_var : simple_guess_search_fun_with_callback (* v *) 63 val sgsfwc_neg : simple_guess_search_fun_with_callback (* ~ _ *) 64 val sgsfwc_and : simple_guess_search_fun_with_callback (* _ /\ _ *) 65 val sgsfwc_or : simple_guess_search_fun_with_callback (* _ \/ _ *) 66 val sgsfwc_imp : simple_guess_search_fun_with_callback (* _ ==> _ *) 67 val sgsfwc_forall : simple_guess_search_fun_with_callback (* !z. _ *) 68 val sgsfwc_exists : simple_guess_search_fun_with_callback (* ?z. _ *) 69 70 (* to find guesses for equations, a function can also be applied to 71 both sides of the equation first. For example, to find guesses 72 for "x" in "(x, y) = f z" it might be useful to apply "FST" to 73 both sides. This is done by "sgsfwc_eq_fun". It gets a list of 74 functions to try. Entries of this list are triples containing the 75 function to apply, a check when to apply and a theorem about how 76 to rewrite in case the check succeeds. For FST the entries would 77 look like: (``FST``, pairSyntax.is_pair, pairTheory.FST). *) 78 val sgsfwc_eq_fun : (term * (term -> bool) * thm) list -> (* ?z. _ = _ *) 79 simple_guess_search_fun_with_callback 80 81 (* List of eq_funs for pairs, lists, options and sum types. *) 82 val default_eq_funs : (term * (term -> bool) * thm) list 83 84 val default_sgsfwcs : simple_guess_search_fun_with_callback list 85 86 (* Generalised conversions that allow specifying which search functions to use *) 87 val SIMPLE_EXISTS_INSTANTIATE_CONV_GEN : simple_guess_search_fun_with_callback list -> conv 88 val SIMPLE_FORALL_INSTANTIATE_CONV_GEN : simple_guess_search_fun_with_callback list -> conv 89 val SIMPLE_UEXISTS_INSTANTIATE_CONV_GEN : simple_guess_search_fun_with_callback list -> conv 90 val SIMPLE_SOME_INSTANTIATE_CONV_GEN : simple_guess_search_fun_with_callback list -> conv 91 val SIMPLE_SELECT_INSTANTIATE_CONV_GEN : simple_guess_search_fun_with_callback list -> conv 92 93 val SIMPLE_QUANT_INSTANTIATE_CONV_GEN : simple_guess_search_fun_with_callback list -> conv 94 val SIMPLE_QUANT_INST_GEN_ss : simple_guess_search_fun_with_callback list -> simpLib.ssfrag 95 96end 97