Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Sage Binder, Hanna Lachnitt, Katherine Kosaian

TL;DR

This work introduces Apply2Isar, a tool for Isabelle/HOL that automatically converts apply-style scripts to declarative Isar, and evaluates it on a large benchmark set consisting of apply-style proofs from the Isabelle Archive of Formal Proofs.

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.

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

TL;DR

This work introduces Apply2Isar, a tool for Isabelle/HOL that automatically converts apply-style scripts to declarative Isar, and evaluates it on a large benchmark set consisting of apply-style proofs from the Isabelle Archive of Formal Proofs.

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.
Paper Structure (15 sections, 1 figure, 2 tables)

This paper contains 15 sections, 1 figure, 2 tables.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Motivating Example and Overview
  4. Implementation Challenges
  5. Operations on Multiple Goals
  6. Operations that Complicate Proof Flow
  7. Interactions Between Commands
  8. Shadowing
  9. Schematic Variables in Goals
  10. Types
  11. Proof Exploration and Partial Proofs
  12. Evaluation
  13. Future and Related Work
  14. Conclusion
  15. Acknowledgements

Figures (1)

  • Figure 1: A visualization of our evaluation data. The green (leftmost) segment of each bar indicates the portion of successes; the hatched orange (middle) segment indicates the portion of partial translations; and the red (rightmost) segment indicates the portion of failures.