hh : tactic
STRUCTURE
holyHammer
SYNOPSIS
General purpose tactic relying on a automatic selection of theorems in the library. It returns a automatically generated call to METIS_TAC that solves the goal. A good practice is to replace the call of holyhammer.hh by the generated tactic.
DESCRIPTION
Select relevant theorems for proving a goal using the k-nearest neighbor premise selection algorithm, translate the theorems together with the goal from higher-order to first-order, call external provers (ATP) and reconstruct the final proof inside HOL4 by calling METIS_TAC with the theorems appearing in the proof of the prover.
FAILURE
Fails if the supplied goal does not contain boolean terms only. Or if no ATP is installed. Or if no proof is found by the installed ATPs in less than a 15 seconds (default). This timeout can be modifed by holyHammer.set_timeout. Or if METIS_TAC cannot reconstruct the proof from the selected theorems in less than one second.
EXAMPLE
- load "holyHammer"; open holyHammer;
(* output omitted *)
> val it = () : unit

- hh ([],``1+1=2``);
Loading 3091 theorems 
proof found by eprover:
  metisTools.METIS_TAC [arithmeticTheory.ALT_ZERO , arithmeticTheory.SUC_ONE_ADD , arithmeticTheory.TWO , numeralTheory.numeral_distrib , numeralTheory.numeral_suc]
minimized proof:  
  METIS_TAC [arithmeticTheory.SUC_ONE_ADD, numeralTheory.numeral_distrib, numeralTheory.numeral_suc]
(* output omitted *)
> val it = ([], fn): goal list * validation
COMMENTS
See src/holyhammer/README for more information on how to install the provers. See more examples in src/holyhammer/examples.
SEEALSO
holyhammer, ttt, matchp
HOL  Trindemossen-1