Edinburgh Research Explorer

Case-Analysis for Rippling and Inductive Proof

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Related Edinburgh Organisations

Open Access permissions


Original languageEnglish
Title of host publicationInteractive Theorem Proving, Series
Subtitle of host publicationFirst International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings
EditorsM. Kaufmann, L. C. Paulson
PublisherSpringer-Verlag GmbH
Number of pages16
ISBN (Electronic)978-3-642-14052-5
ISBN (Print)978-3-642-14051-8
Publication statusPublished - 2010

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
ISSN (Print)0302-9743


Rippling is a heuristic used to guide rewriting and is typically used for inductive theorem proving. We introduce a method to support case-analysis within rippling. Like earlier work, this allows goals containing if-statements to be proved automatically. The new contribution is that our method also supports case-analysis on datatypes. By locating the case-analysis as a step within rippling we also maintain the termination. The work has been implemented in IsaPlanner and used to extend the existing inductive proof method. We evaluate this extended prover on a large set of examples from Isabelle’s theory library and from the inductive theorem proving literature. We find that this leads to a significant improvement in the coverage of inductive theorem proving. The main limitations of the extended prover are identified, highlight the need for advances in the treatment of assumptions during rippling and when conjecturing lemmas.

    Research areas

  • Computer Science, Rippling, Interactive Theorem Proving

Download statistics

No data available

ID: 142468