src/quantHeuristics/quantHeuristicsLibBase.sig

34   datatype guess =
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
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
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
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
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
72   val guess_thm_to_guess  : bool -> (term * term list) option -> thm -> guess
76   val guess_to_string : bool -> guess -> string
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}
92   val guess_collection_guess_type : guess_type -> guess_collection -> guess list
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;
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;