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