  The logic of hereditary Harrop formulas (HH) has proven useful for specifying
a wide range of formal systems. This logic includes a form of hypothetical
judgment that leads to dynamically changing sets of assumptions and that is key
to encoding side conditions and contexts that occur frequently in structural
operational semantics (SOS) style presentations. Specifications are often
useful in reasoning about the systems they describe. The Abella theorem prover
supports such reasoning by explicitly embedding the specification logic within
a rich reasoning logic; specifications are then reasoned about through this
embedding. However, realizing an induction principle in the face of dynamically
changing assumption sets is nontrivial and the original Abella system uses only
a subset of the HH specification logic for this reason. We develop a method
here for supporting inductive reasoning over all of HH. Our approach takes
advantage of a focusing property of HH to isolate the use of an assumption and
the ability to finitely characterize the structure of any such assumption in
the reasoning logic. We demonstrate the effectiveness of these ideas via
several specification and meta-theoretic reasoning examples that have been
implemented in an extended version of Abella.
