Structure metisTools
(* ========================================================================= *)
(* A HOL INTERFACE TO THE METIS FIRST-ORDER PROVER. *)
(* Created by Joe Hurd, October 2001 *)
(* ========================================================================= *)
signature metisTools =
sig
(* "Metis" trace levels:
0: No output
1: The equivalent of Meson dots
2: Timing information
3: More detailed prover information: slice by slice
4: Log of each step in proof translation
5: Log of each inference during proof search *)
type 'a stream = 'a mlibStream.stream
type limit = mlibMeter.limit
type term = Term.term
type thm = Thm.thm
type tactic = Abbrev.tactic
type Query = folTools.Query
type Result = folTools.Result
(* Parameters *)
type Fparm = folTools.parameters
type Mparm = mlibMetis.parameters
type parameters = {interface : Fparm, solver : Mparm, limit : limit}
val defaults : parameters
val update_interface : (Fparm -> Fparm) -> parameters -> parameters
val update_solver : (Mparm -> Mparm) -> parameters -> parameters
val update_limit : (limit -> limit) -> parameters -> parameters
(* Prolog solver *)
val PROLOG_SOLVE : thm list -> Query -> Result stream
(* Metis solver *)
val GEN_METIS_SOLVE : parameters -> thm list -> Query -> Result stream
(* Tactic interface to the metis prover *)
val GEN_METIS_TAC : parameters -> thm list -> tactic
(* All the following use this limit *)
val limit : limit ref
(* Canned parameters for common situations *)
val FO_METIS_TAC : thm list -> tactic (* First-order *)
val FOT_METIS_TAC : thm list -> tactic (* + types *)
val HO_METIS_TAC : thm list -> tactic (* Higher-order *)
val HOT_METIS_TAC : thm list -> tactic (* + types *)
val FULL_METIS_TAC : thm list -> tactic (* + combinators & booleans *)
(* Simple user interface to the metis prover *)
val FO_METIS_PROVE : thm list -> term -> thm (* First-order *)
val FOT_METIS_PROVE : thm list -> term -> thm (* + types *)
val HO_METIS_PROVE : thm list -> term -> thm (* Higher-order *)
val HOT_METIS_PROVE : thm list -> term -> thm (* + types *)
val FULL_METIS_PROVE : thm list -> term -> thm (* + combinators & booleans *)
(* Uses heuristics to apply one of {FO|FOT}, {HO|HOT} or FULL. *)
val METIS_TAC : thm list -> tactic
val METIS_PROVE : thm list -> term -> thm
end
HOL 4, Kananaskis-13