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

Sage Binder; Hanna Lachnitt; Katherine Kosaian

doi:10.48550/arxiv.2603.07771

Back

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

Preprint

Open access

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

Sage Binder, Hanna Lachnitt and Katherine Kosaian

ArXiv.org

Cornell University

03/08/2026

DOI: 10.48550/arxiv.2603.07771

Files and links (1)

url

https://doi.org/10.48550/arxiv.2603.07771View

Preprint (Author's original)This preprint has not been evaluated by subject experts through peer review. Preprints may undergo extensive changes and/or become peer-reviewed journal articles. Open Access

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" proof scripts 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 scripts to declarative Isar. This allows users to write complex, possibly fragile apply-style scripts, 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.

Computer Science - Logic in Computer Science

Details

Title: Subtitle: Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar
Creators: Sage Binder
Hanna Lachnitt
Katherine Kosaian
Resource Type: Preprint
Publication Details: ArXiv.org
DOI: 10.48550/arxiv.2603.07771
ISSN: 2331-8422
Publisher: Cornell University; Ithaca, New York
Language: English
Date posted: 03/08/2026
Academic Unit: Computer Science
Record Identifier: 9985143126702771

Metrics

1 Record Views