Abstract

We show how to automate termination proofs for recursive functions in (a
first-order subset of) Isabelle/HOL by encoding them as term rewrite
systems and invoking an external termination prover. Our link to the
external prover includes full proof reconstruction, where all necessary
properties are derived inside Isabelle/HOL without oracles. Apart from the
certification of the imported proof, the main challenge is the formal
reduction of the proof obligation produced by Isabelle/HOL to the
termination of the corresponding term rewrite system. We automate this
reduction via suitable tactics which we added to the IsaFoR library.

BibTeX

@inproceedings{AKCSRTCFJG-ITP11,
  author      = "Alexander Krauss and Christian Sternagel and Ren{\'e}
                 Thiemann and Carsten Fuhs and J{\"u}rgen Giesl",
  title       = "Termination of {Isabelle} Functions via Termination of
                 Rewriting",
  booktitle   = "Proceedings of the 2nd International Conference on
                 Interactive Theorem Proving",
  series      = "Lecture Notes in Computer Science",
  volume      = 6898,
  pages       = "152--167",
  publisher   = "Springer-Verlag",
  year        = 2011
}