Automated Discovery of Conditional Lemmas in Hipster

Abstract

Hipster is a tool for theory exploration and automation of inductive proofs for the proof assistant Isabelle/HOL. The purpose of theory exploration is to automate the discovery (and proof) of new lemmas of interest within a theory development, enriching the background theory and providing necessary missing lemmas that might be required for other automated tactics to succeed. Hipster has so far succeeded in incorporating automated discovery of equational conjectures and lemmas. This work presents an extension of Hipster adding support for conditional lemmas, required, for example, when reasoning about sorting algorithms and treating different branches of a proof along with their specific conditions. The main focus is the implementation of a tactic for automated inductive proving via recursion induction, accompanied by an evaluation of the tool’s capabilities. Recursion induction succeeds at automatically proving many of the discovered conditional conjectures, whereas a previously existing tactic was unable to. Additionally, recursion induction manages to set up inductive steps in a proof to render more immediately realisable subgoals by following computation order. Results show proving capabilities are increased not only with respect to conditional lemmas but also for more general equational lemmas.