Conference proceeding
Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar
17th International Conference on Interactive Theorem Proving, ITP 2026, Vol.382, 18
07/16/2026
DOI: 10.4230/LIPIcs.ITP.2026.18
Abstract
In Isabelle/HOL, declarative proofs written in the Isar language are widely appreciated for their readability and robustness. However, some users may prefer writing procedural "apply-style" proofs since they enable rapid exploration of the search space. To get the best of both worlds, we introduce Apply2Isar, a tool for Isabelle/HOL that automatically converts apply-style proofs to declarative Isar. This allows users to write complex, possibly fragile apply-style proofs, and then automatically convert them to more readable and robust declarative Isar proofs. To demonstrate the efficacy of Apply2Isar in practice, we evaluate it on a large benchmark set consisting of apply-style proofs from the Isabelle Archive of Formal Proofs.
Details
- Title: Subtitle
- Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar
- Creators
- Sage Binder - University of IowaHanna Lachnitt - Stanford UniversityKatherine Kosaian - University of Iowa
- Resource Type
- Conference proceeding
- Publication Details
- 17th International Conference on Interactive Theorem Proving, ITP 2026, Vol.382, 18
- DOI
- 10.4230/LIPIcs.ITP.2026.18
- ISSN
- 1868-8969
- Grant note
- FA8750-24-2-1001 / Defense Advanced Research Projects Agency (100000185) FA8750-24-2-1001 / Defense Advanced Research Projects Agency (http://data.elsevier.com/vocabulary/SciValFunders/100000185)
- Language
- English
- Date published
- 07/16/2026
- Academic Unit
- Computer Science
- Record Identifier
- 9985217816302771
Metrics
1 Record Views