Faster Smarter Induction in Isabelle/HOL

We present semantic_induct, an automatic tool to recommend how to apply proof by induction in Isabelle/HOL. Given an inductive problem, semantic_induct produces candidate arguments to the induct tactic and selects promising ones using heuristics. Our evaluation based on 1,095 inductive problems from 22 theory files shows that semantic_induct achieves a 90.0\% increase of the coincidence rate for the most promising candidate within 5.0 seconds of timeout compared to an existing tool, smart_induct, while achieving a 62.0\% decrease of the median value of execution time.