1signature quantHeuristicsLibBase = 2sig 3 include Abbrev 4 5 6(*some general conversions, that might be useful 7 in other context as well *) 8 val TOP_ONCE_REWRITE_CONV : thm list -> conv; 9 val NEG_NEG_INTRO_CONV : conv; 10 val NEG_NEG_ELIM_CONV : conv; 11 val NOT_FORALL_LIST_CONV : conv; 12 val NOT_EXISTS_LIST_CONV : conv; 13 val STRIP_NUM_QUANT_CONV : int -> conv -> conv; 14 val BOUNDED_NOT_EXISTS_LIST_CONV : int -> conv; 15 val BOUNDED_REPEATC : int -> conv -> conv; 16 17 val EXISTS_NOT_LIST_CONV : conv; 18 val FORALL_NOT_LIST_CONV : conv; 19 val QUANT_SIMP_CONV : conv; 20 21 val NOT_OR_CONV : conv; 22 val NOT_AND_CONV : conv; 23 val AND_NOT_CONV : conv; 24 val OR_NOT_CONV : conv; 25 26 val VARIANT_TAC : term list -> tactic 27 val VARIANT_CONV : term list -> conv 28 29 30 datatype guess_type = 31 gty_exists | gty_exists_gap | gty_exists_point 32 | gty_forall | gty_forall_gap | gty_forall_point 33 34 datatype guess = 35 guess_general of term * term list 36 | guess_term of guess_type * term * term list * term 37 | guess_thm of guess_type * term * term list * thm 38 39 val is_guess_general : guess -> bool 40 val is_guess_thm : guess_type -> guess -> bool 41 val is_guess_term : guess_type -> guess -> bool 42 val is_guess : guess_type -> guess -> bool 43 val guess_has_thm : guess -> bool 44 val guess_has_no_free_vars : guess -> bool 45 val guess_has_thm_no_free_vars : guess -> bool 46 47 val guess_type2string : guess_type -> string 48 val guess_type2term : guess_type -> term 49 val guess_term2type : term -> guess_type 50 val make_guess_thm_term : guess_type -> term -> term -> term -> term list -> term 51 val guess_remove_thm : term -> term -> guess -> guess 52 val make_set_guess_thm : guess -> (term -> thm) -> guess 53 val mk_guess : guess_type -> term -> term -> term -> term list -> guess 54 val mk_guess_opt : guess_type option -> term -> term -> term -> term list -> guess 55 56 val make_guess___dummy : guess_type -> term -> term -> term -> term list -> guess 57 val make_guess___assume : guess_type -> term -> term -> term -> term list -> guess 58 val make_guess___simple : guess_type -> term -> term -> term -> term list -> guess 59 60 val make_set_guess_thm___dummy : guess -> guess 61 val make_set_guess_thm___simple : guess -> guess 62 val make_set_guess_thm___assume : guess -> guess 63 64 val guess_extract : guess -> term * term list 65 val guess_extract_thm : guess -> guess_type * term * term list * thm * bool 66 val guess2term : guess -> term option 67 val guess2thm : guess -> bool * thm 68 val guess2thm_opt : guess -> thm option 69 val guess_extract_type : guess -> guess_type option 70 71 72 val guess_thm_to_guess : bool -> (term * term list) option -> thm -> guess 73 val dest_guess_tm : term -> guess_type * term * term * term 74 val is_guess_tm : term -> bool 75 76 val guess_to_string : bool -> guess -> string 77 78 79 (*guesses are organised in collections. They are used to 80 store the different types of guesses separately. Moreover, 81 rewrite theorems, that might come in handy, are there as well.*) 82 type guess_collection = 83 {rewrites : thm list, 84 general : guess list, 85 exists_point : guess list, 86 forall_point : guess list, 87 forall : guess list, 88 exists : guess list, 89 forall_gap : guess list, 90 exists_gap : guess list} 91 92 val guess_collection_guess_type : guess_type -> guess_collection -> guess list 93 94 val empty_guess_collection : guess_collection; 95 val is_empty_guess_collection : guess_collection -> bool; 96 val guess_collection_append : guess_collection -> guess_collection -> guess_collection; 97 val guess_collection_flatten : guess_collection option list -> guess_collection; 98 val guess_list2collection : thm list * guess list -> guess_collection; 99 val guess_collection2list : guess_collection -> thm list * guess list; 100 val guess_collection___get_exists_weaken : guess_collection -> guess list; 101 val guess_collection___get_forall_weaken : guess_collection -> guess list; 102 103 104 105 val guess_weaken : guess -> guess 106 val check_guess : term -> term -> guess -> bool 107 val correct_guess : term -> term -> guess -> guess option 108 val correct_guess_list : term -> term -> guess list -> guess list; 109 val correct_guess_collection : 110 term -> term -> guess_collection -> guess_collection 111 112 113 type inference_collection = 114 {exists_point : thm list, 115 forall_point : thm list, 116 exists : thm list, 117 forall : thm list, 118 exists_gap : thm list, 119 forall_gap : thm list}; 120 121 val GUESS_THM_list2collection : thm list -> inference_collection; 122 123 124 exception QUANT_INSTANTIATE_HEURISTIC___no_guess_exp; 125 126(*Basic types*) 127 type quant_heuristic_base = term -> term -> guess_collection; 128 type quant_heuristic = quant_heuristic_base -> quant_heuristic_base; 129 type quant_heuristic_cache; 130 131 val mk_quant_heuristic_cache : unit -> quant_heuristic_cache; 132 133 134(* Quantifier Heuristics Parameters are the main way to configure the behaviour. They 135 are a record of theorems, conversion and full heuristics used during proof search. *) 136 137 type quant_param; 138 139(* constructing quantifier heuristics parameters*) 140 141 val distinct_qp : thm list -> quant_param 142 val cases_qp : thm list -> quant_param 143 val rewrite_qp : thm list -> quant_param 144 val inst_filter_qp : (term -> term -> term -> term list -> bool) list -> quant_param 145 val instantiation_qp : thm list -> quant_param 146 val imp_qp : thm list -> quant_param 147 val fixed_context_qp : thm list -> quant_param 148 val inference_qp : thm list -> quant_param 149 val convs_qp : conv list -> quant_param 150 val filter_qp : (term -> term -> bool) list -> quant_param 151 val top_heuristics_qp: quant_heuristic list -> quant_param 152 val context_heuristics_qp : (thm list -> quant_heuristic) list -> quant_param 153 val context_top_heuristics_qp : (thm list -> quant_heuristic) list -> quant_param 154 val heuristics_qp : quant_heuristic list -> quant_param 155 val oracle_qp : (term -> term -> (term * term list) option) -> quant_param (* creates heuristic that produces oracle guesses *) 156 val context_oracle_qp: (thm list -> term -> term -> (term * term list) option) -> quant_param (* creates heuristic that produces oracle guesses *) 157 val final_rewrite_qp : thm list -> quant_param 158 159 (* a stateful version and combining several*) 160 val clear_stateful_qp : unit -> unit 161 val stateful_qp___add_combine_arguments : 162 quant_param list -> unit; 163 164 val empty_qp : quant_param; 165 val basic_qp : quant_param; (* the basic things that should always be turned on *) 166 val direct_context_qp : quant_param; (* use the context, but don't recurse *) 167 val context_qp : quant_param; (* use the context *) 168 val stateful_qp : unit -> quant_param; 169 val pure_stateful_qp : unit -> quant_param; 170 val TypeBase_qp : quant_param; 171 val get_qp___for_types : hol_type list -> quant_param 172 173 val combine_qp : 174 quant_param -> quant_param -> 175 quant_param; 176 177 val combine_qps : 178 quant_param list -> quant_param; 179 180 181 val COMBINE_HEURISTIC_FUNS : (unit -> guess_collection) list -> guess_collection; 182 183(*Heuristics that might be useful to write own ones*) 184 val QUANT_INSTANTIATE_HEURISTIC___CONV : conv -> quant_heuristic; 185 val QUANT_INSTANTIATE_HEURISTIC___EQUATION_distinct : thm list -> quant_heuristic; 186 val QUANT_INSTANTIATE_HEURISTIC___EQUATION_two_cases : thm -> quant_heuristic; 187 val QUANT_INSTANTIATE_HEURISTIC___one_case : thm -> quant_heuristic; 188 val QUANT_INSTANTIATE_HEURISTIC___cases : thm -> quant_heuristic; 189 val QUANT_INSTANTIATE_HEURISTIC___GIVEN_INSTANTIATION : bool -> thm list -> quant_heuristic; 190 val QUANT_INSTANTIATE_HEURISTIC___STRENGTHEN_WEAKEN : thm list -> quant_heuristic; 191 val QUANT_INSTANTIATE_HEURISTIC___QUANT : bool -> quant_heuristic; 192 193 val QUANT_INSTANTIATE_HEURISTIC___max_rec_depth : int ref 194 195 (*use this to create sys for debugging own heuristics*) 196 val qp_to_heuristic : quant_param -> quant_heuristic_cache ref option -> thm list -> term -> term -> guess_collection 197 val debug_sys : term -> term -> guess_collection 198 199 (*The most important functions *) 200 val EXTENSIBLE_QUANT_INSTANTIATE_CONV : quant_heuristic_cache ref option -> 201 bool -> bool -> bool -> thm list -> quant_param -> quant_param list -> conv; 202 val QUANT_INSTANTIATE_TAC : quant_param list -> tactic; 203 val ASM_QUANT_INSTANTIATE_TAC : quant_param list -> tactic; 204 val QUANT_INSTANTIATE_CONV : quant_param list -> conv; 205 val FAST_QUANT_INSTANTIATE_CONV : quant_param list -> conv; 206 val FAST_QUANT_INSTANTIATE_TAC : quant_param list -> tactic; 207 val FAST_ASM_QUANT_INSTANTIATE_TAC : quant_param list -> tactic; 208 val EXPAND_QUANT_INSTANTIATE_CONV : quant_param list -> conv; 209 val FAST_EXPAND_QUANT_INSTANTIATE_CONV: quant_param list -> conv; 210 211 val NORE_QUANT_INSTANTIATE_CONV : quant_param list -> conv; 212 val NORE_EXPAND_QUANT_INSTANTIATE_CONV : quant_param list -> conv; 213 214 215 val EXTENSIBLE_QUANT_INSTANTIATE_CONSEQ_CONV : 216 quant_heuristic_cache ref option -> bool -> bool -> quant_param -> quant_param list -> ConseqConv.directed_conseq_conv; 217 val EXTENSIBLE_QUANT_INSTANTIATE_STEP_CONSEQ_CONV : 218 quant_heuristic_cache ref option -> bool -> quant_param -> quant_param list -> ConseqConv.directed_conseq_conv; 219 val QUANT_INSTANTIATE_CONSEQ_CONV : 220 quant_param list -> ConseqConv.directed_conseq_conv; 221 val QUANT_INSTANTIATE_CONSEQ_TAC : quant_param list -> tactic; 222 val NORE_QUANT_INSTANTIATE_CONSEQ_CONV : 223 quant_param list -> ConseqConv.directed_conseq_conv; 224 val FAST_QUANT_INSTANTIATE_CONSEQ_CONV : 225 quant_param list -> ConseqConv.directed_conseq_conv; 226 227 228 val INST_QUANT_CONV : (string * Parse.term Lib.frag list * Parse.term Parse.frag list list) list 229 -> conv; 230 val QUANT_TAC : (string * Parse.term Lib.frag list * Parse.term Parse.frag list list) list 231 -> tactic; 232 233(* Predefined filters to use with filter_qp *) 234val subterm_filter : term list -> term -> term -> bool 235val subterm_match_filter : term list -> term -> term -> bool 236val type_filter : hol_type list -> term -> term -> bool 237val type_match_filter : hol_type list -> term -> term -> bool 238val neg_filter : (term -> term -> bool) -> term -> term -> bool 239 240(*combination with simplifier*) 241 val QUANT_INST_ss : quant_param list -> simpLib.ssfrag; 242 val EXPAND_QUANT_INST_ss : quant_param list -> simpLib.ssfrag; 243 val FAST_QUANT_INST_ss : quant_param list -> simpLib.ssfrag; 244 245(* Traces *) 246(* "QUANT_INST_DEBUG" can be used to get debug information on 247 how guesses are obtained 248 249 "QUANT_INST___print_term_length" used for printing debug concisely 250 251 252 "QUANT_INST___REC_DEPTH" can set the maximal recursion depth, default is 250. 253 If the search is aborted, because the depth is not big enough, a warning 254 is printed. Decrease for speed and increase if the warning appears and you want to search deeper. 255*) 256 257 258 259end 260