  Proof assistants offer tactics to apply proof by induction, but these tactics
rely on inputs given by human engineers. To automate this laborious process, we
developed SeLFiE, a boolean query language to represent experienced users'
knowledge on how to apply the induct tactic in Isabelle/HOL: when we apply an
induction heuristic written in SeLFiE to an inductive problem and arguments to
the induct tactic, the SeLFiE interpreter judges whether the arguments are
plausible for that problem according to the heuristic by examining both the
syntactic structure of the problem and definitions of the relevant constants.
To examine the intricate interaction between syntactic analysis and analysis of
constant definitions, we introduce definitional quantifiers. For evaluation we
build an automatic induction prover using SeLFiE. Our evaluation based on 347
inductive problems shows that our new prover achieves 1.4 x 10^3% improvement
over the corresponding baseline prover for 1.0 second of timeout and the median
value of speedup is 4.48x.
