HOL Import
Theory translation from HOL Light to Isabelle/HOL
|
|
 |
Publications:
Abstract:
All existing translations between proof assistants have been
notoriously sluggy, resource-demanding, and do not scale to large
developments, which has lead to the general perception that the whole
approach is probably not practical. We aim to show that the observed
inefficiencies are not inherent, but merely a deficiency of the
existing implementations. We do so by providing a new implementation
of a theory import from HOLLight to Isabelle/HOL, which achieves
decent performance and scalability mostly by avoiding the mistakes of
the past.
After some preprocessing, our tool can import large HOLLight
developments faster than HOLLight processes them. Our main target and
motivation is the Flyspeck development, which can be imported in a few
hours on commodity hardware. We also provide mappings for most basic
types present in the developments including lists, integers and real
numbers.
This papers outlines some design considerations and presents a few of our
extensive measurements, which reveal interesting insights in the low-level
structure of larger proof developments.
Source Code
- Download source code: holimport.tgz.
- Unpack in your HOL Light directory and follow the instructions in the included README file.
Documentation