The case-analysis evaluation corpus consists of 87 theorems about functions defined using conditional statements over natural numbers, lists and binary trees. IsaPlanner's rippling technique can automatically prove 47 of these theorems, only using the function definitions and not supplied with any extra lemmas. A simpler technique, applying induction followed by Isabelle's simplifier proves 37 theorems. We also experimented with a modification to our original case-analysis technique for rippling, allowing it to conjecture non-rippling goals after case-splitting as lemmas. This technique was able to prove 49 theorems, but would often not terminate on theorems it could not solve, which does not happen for the standard version.
The Isabelle theory files used in the experiments are below:
Webpage maintained by
Moa Johansson
