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?


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.