Anzeige
Erschienen in:
2013 | OriginalPaper | Buchkapitel
Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
verfasst von : Brian Huffman, Ondřej Kunčar
Erschienen in: Certified Programs and Proofs
Verlag: Springer International Publishing
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Quotients, subtypes, and other forms of type abstraction are ubiquitous in formal reasoning with higher-order logic. Typically, users want to build a library of operations and theorems about an abstract type, but they want to write definitions and proofs in terms of a more concrete representation type, or “raw” type. Earlier work on the Isabelle Quotient package has yielded great progress in automation, but it still has many technical limitations.
We present an improved, modular design centered around two new packages: the
Transfer
package for proving theorems, and the
Lifting
package for defining constants. Our new design is simpler, applicable in more situations, and has more user-friendly automation.