I'm patching up Isabelle/Mizar to work with Isabelle2023, and I am wondering what are the best practices for implementing an object logic in Isabelle? (Usually there is great documentation for Isabelle, but this is the one department where it is lacking.)
Some random selection of the questions which come to mind:
- Is there an idiomatic way to implement "unit tests" to double check, e.g., the syntactic constructions are working as intended? (I know that we can prove results concerning the implementation, but just "quick example usage" type tests are helpful.)
- Are there expected metatheorems to prove various properties of the object logic?
- Are there idiomatic judgments to implement? Is there some expected "skeleton" which object logics should resemble?
