Document Open Access Logo

Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar

Authors Sage Binder , Hanna Lachnitt , Katherine Kosaian

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2026.18.pdf
  • Filesize: 0.8 MB
  • 20 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Proof Assistants
  • Isabelle/HOL
  • Isabelle/ML
  • Isabelle/Isar
  • Proof Refactoring

Metrics

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.

Cite As Get BibTex

Sage Binder, Hanna Lachnitt, and Katherine Kosaian. Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 18:1-18:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.ITP.2026.18

Author Details

Sage Binder
  • University of Iowa, Iowa City, IA, USA
Hanna Lachnitt
  • Stanford University, Stanford, CA, USA
Katherine Kosaian
  • University of Iowa, Iowa City, IA, USA

Funding

This work was supported in part by the Defense Advanced Research Projects Agency (DARPA) under contract FA8750-24-2-1001. Any opinions, findings, and conclusions or recommendations expressed here are those of the authors and do not necessarily reflect the views of DARPA.

Acknowledgements

Many thanks to Fabian Huch for his valuable feedback on the paper and his Isabelle/ML guidance. We also thank Andrew Marmaduke, Kartik Sabharwal, Shweta Rajiv, and Apoorv Ingle for useful discussions and helpful feedback on the paper. For help with specific technical questions via the Isabelle Zulip channel, we thank Jonathan Julián Huerta y Munive, Kevin Kappelmann, and Lukas Bartl. Finally, we thank the anonymous ITP reviewers for their valuable feedback and comments.

Supplementary Materials

References

  1. Archive of formal proofs. URL: https://www.isa-afp.org/.
  2. Mark Adams. Refactoring proofs with Tactician. In Domenico Bianculli, Radu Calinescu, and Bernhard Rumpe, editors, Software Engineering and Formal Methods - SEFM 2015 Collocated Workshops: ATSE, HOFM, MoKMaSD, and VERY*SCART, York, UK, September 7-8, 2015, Revised Selected Papers, volume 9509 of Lecture Notes in Computer Science, pages 53-67. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-49224-6_6.
  3. Gertrud Bauer and Tobias Nipkow. Flyspeck I: Tame graphs. Archive of Formal Proofs, May 2006. Formal proof development. URL: https://isa-afp.org/entries/Flyspeck-Tame.html.
  4. Hanno Becker, Nathan Chong, Robert Dockins, Jim Grundy, Jason Z. S. Hu, Ike Mulder, Dominic P. Mulligan, Paul Mure, Lawrence C. Paulson, and Konrad Slind. AutoCorrode software verification framework for Isabelle/HOL. https://github.com/awslabs/autocorrode, 2025.
  5. Stefan Berghofer and Tobias Nipkow. Proof terms for simply typed higher order logic. In Mark Aagaard and John Harrison, editors, Theorem Proving in Higher Order Logics, pages 38-52, Berlin, Heidelberg, 2000. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/3-540-44659-1_3.
  6. Sage Binder, Hanna Lachnitt, and Katherine Kosaian. Apply2Isar. Software, (visited on 2026-07-13). URL: https://github.com/sagebinder/apply2isar
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.27121
  7. Jasmin Blanchette, Martin Desharnais, Lawrence C. Paulson, and Lukas Bartl. Hammering Away: A User’s Guide to Sledgehammer for Isabelle/HOL, January 2026. User’s Guide. URL: https://isabelle.in.tum.de/doc/sledgehammer.pdf.
  8. Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel. Operations on bounded natural functors. Archive of Formal Proofs, December 2017. Formal proof development. URL: https://isa-afp.org/entries/BNF_Operations.html.
  9. Matthew Brecknell, David Greenaway, Johannes Hölzl, Fabian Immler, Gerwin Klein, Rafal Kolanski, Japheth Lim, Michael Norrish, Norbert Schirmer, Salomon Sickert, Thomas Sewell, Harvey Tuch, and Simon Wimmer. AutoCorres2. Archive of Formal Proofs, April 2024. Formal proof development. URL: https://isa-afp.org/entries/AutoCorres2.html.
  10. Florian Haftmann. Sketch_and_Explore. Isabelle Distribution. URL: https://isabelle.in.tum.de/library/HOL/HOL-ex/Sketch_and_Explore.html.
  11. John Harrison. HOL Light: An overview. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors, Theorem Proving in Higher Order Logics, pages 60-66, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-03359-9_4.
  12. Kevin Kappelmann. Zippy - generic white-box proof search with zippers, 2025. URL: https://doi.org/10.48550/arXiv.2503.20413.
  13. Kevin Kappelmann. Zippy - generic white-box proof search with zippers. Archive of Formal Proofs, November 2025. Formal proof development. URL: https://isa-afp.org/entries/Zippy.html.
  14. Hidetsune Kobayashi. Fundamental properties of valuation theory and Hensel’s lemma. Archive of Formal Proofs, August 2007. Formal proof development. URL: https://isa-afp.org/entries/Valuation.html.
  15. Hidetsune Kobayashi, L. Chen, and H. Murao. Groups, rings and modules. Archive of Formal Proofs, May 2004. Formal proof development. URL: https://isa-afp.org/entries/Group-Ring-Module.html.
  16. Peter Lammich. The imperative refinement framework. Archive of Formal Proofs, August 2016. Formal proof development. URL: https://isa-afp.org/entries/Refine_Imperative_HOL.html.
  17. Peter Lammich. Refinement to imperative HOL. Journal of Automated Reasoning, 62(4):481-503, April 2019. URL: https://doi.org/10.1007/s10817-017-9437-1.
  18. Nicolas Magaud. Towards automatic transformations of Coq proof scripts. Electronic Proceedings in Theoretical Computer Science, 398:4-10, January 2024. URL: https://doi.org/10.4204/EPTCS.398.4.
  19. Yecine Megdiche, Fabian Huch, and Lukas Stevens. A linter for Isabelle: Implementation and evaluation. CoRR, abs/2207.10424, 2022. URL: https://doi.org/10.48550/arXiv.2207.10424.
  20. Adam Naumowicz and Artur Korniłowicz. A brief overview of mizar. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors, Theorem Proving in Higher Order Logics, pages 67-72, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg. Google Scholar
  21. Tobias Nipkow, Lawrence C. Paulson, and Makarius Wenzel. A Proof Assistant for Higher Order Logic. Isabelle/HOL Tutorial. URL: https://isabelle.in.tum.de/doc/tutorial.pdf.
  22. Lawrence C. Paulson. Isabelle: The next seven hundred theorem provers. In Ewing Lusk and Ross Overbeek, editors, 9th International Conference on Automated Deduction, pages 772-773, Berlin, Heidelberg, 1988. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/BFB0012891.
  23. Jessica Shi, Cassia Torczon, Harrison Goldstein, Andrew Head, and Benjamin C. Pierce. Designing Proof Deautomation for Rocq. In 15th PLATEAU Workshop on Programming Languages and Human-Computer Interaction, July 2025. URL: https://doi.org/10.1184/R1/29087003.v1.
  24. Chengsong Tan, Alastair F. Donaldson, Jonathan Julián Huerta y Munive, and John Wickerson. The burden of proof: Automated tooling for rapid iteration on large mechanised proofs. In 13th IEEE/ACM International Conference on Formal Methods in Software Engineering, FormaliSE@ICSE 2025, Ottawa, ON, Canada, April 27-28, 2025, pages 34-45. IEEE, 2025. URL: https://doi.org/10.1109/FORMALISE66629.2025.00010.
  25. Makarius Wenzel. The Isabelle/Isar Implementation. Isabelle/Isar Implementation Manual. URL: https://isabelle.in.tum.de/dist/Isabelle2025-2/doc/implementation.pdf.
  26. Makarius Wenzel. The Isabelle/Isar Reference Manual. Isabelle/Isar Reference Manual. URL: https://isabelle.in.tum.de/doc/isar-ref.pdf.
  27. Makarius Wenzel. Interaction with formal mathematical documents in isabelle/pide. In Cezary Kaliszyk, Edwin C. Brady, Andrea Kohlhase, and Claudio Sacerdoti Coen, editors, Intelligent Computer Mathematics - 12th International Conference, CICM 2019, Prague, Czech Republic, July 8-12, 2019, Proceedings, Lecture Notes in Computer Science, pages 1-15. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-23250-4_1.
  28. Markus Wenzel. Isar - A generic interpretative approach to readable formal proof documents. In Yves Bertot, Gilles Dowek, Laurent Théry, André Hirschowitz, and Christine Paulin, editors, Theorem Proving in Higher Order Logics, pages 167-183, Berlin, Heidelberg, 1999. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/3-540-48256-3_12.
  29. Freek Wiedijk. A synthesis of the procedural and declarative styles of interactive theorem proving. Log. Methods Comput. Sci., 8(1), 2012. URL: https://doi.org/10.2168/LMCS-8(1:30)2012.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact