Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar
Fuente:
arXiv
Salvato in:
| Autori principali: | , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2026
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866914618693124096 |
|---|---|
| author | Binder, Sage Lachnitt, Hanna Kosaian, Katherine |
| author_facet | Binder, Sage Lachnitt, Hanna Kosaian, Katherine |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2603_07771 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar Binder, Sage Lachnitt, Hanna Kosaian, Katherine Logic in Computer Science F.4.1 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. |
| title | Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar |
| topic | Logic in Computer Science F.4.1 |
| url | https://arxiv.org/abs/2603.07771 |