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.

翻译：在Isabelle/HOL中，以Isar语言编写的声明式证明因其可读性和鲁棒性而广受认可。然而，部分用户可能更倾向于编写过程式"apply风格"的证明脚本，因为这种方式便于快速探索搜索空间。为兼得两者优势，我们提出了Apply2Isar——一个用于Isabelle/HOL的工具，它能自动将apply风格的脚本转换为声明式Isar。这使得用户可以编写复杂（可能脆弱）的apply风格脚本，随后自动将其转换为更易读且鲁棒的声明式Isar证明。为证明Apply2Isar在实际应用中的有效性，我们使用来自Isabelle正式证明档案库的大规模基准测试集对其进行了评估，该测试集包含apply风格的证明。