A Meta-Model for the Isabelle API

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 “datatype ” 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[1] project where it is used to con-struct a package for object-oriented data-type theories generated from UML class di