Email Gateway (Aug 22 2022 at 11:19): Email Gateway (Aug 22 2022 at 11:19):From: Tobias Nipkow <nipkow@in.tum.de>
A Meta-Model for the Isabelle API
Frédéric Tuong and Burkhart Wolff
http://afp.sourceforge.net/entries/Isabelle_Meta_Model.shtml
We represent a theory of (a fragment of) Isabelle/HOL in Isabelle/HOL. The
purpose of this exercise is to write packages for domain-specific specifications
such as class models, B-machines, ..., and generally any languages that can be
described with a sequence of datatypes in HOL itself; the Isabelle
code-generator can then be used to generate tactic code.
Consequently the package is geared towards parsing, printing and code-generation
to the Isabelle API. It is at the moment not sufficiently rich for doing meta
theory on Isabelle itself. Extensions in this direction are possible though.
Moreover, the chosen fragment is fairly rudimentary. However it should be easily
adapted to one's needs if a package is written on top of it. The supported API
contains types, terms, transformation of global context like definitions and
data-type declarations as well as infrastructure for Isar-setups.
This theory is drawn from the Featherweight OCL project where it is used to
construct a package for object-oriented data-type theories generated from UML
class diagrams. The Featherweight OCL, for example, allows for both the direct
execution of compiled tactic code by the Isabelle API as well as the generation
of ".thy"-files for debugging purposes.
Gained experience from this project shows that the compiled code is sufficiently
efficient for practical purposes while being based on a formal "model" on which
properties of the package can be proven such as termination of certain
transformations, correctness, etc.
Enjoy!
smime.p7s
Last updated: Apr 26 2024 at 04:17 UTC