I am currently working on solving the problem of correctness of model transformations. I read a lot of articles and found Isabelle theorem prover is a good choice to solve the problem. Now I want to use the Isabelle theorem prover for analysis and verification. But I do not know how to formalize my modeling language (including source model, target model, transformation itself) with Isabelle ’s own language standard. In other words, I want to quickly learn Isabelle's formal language to describe my modeling language. I downloaded many documentation on the official website, but I can not determined how to get started quickly. I hope that researchers in the field can give some suggestions to the beginners, thank you very much.
I would recommend the concrete semantics book:
http://concrete-semantics.org/
It teaches you how to model a small programming language in Isabelle and how to specify its semantics.
I guess the approach will be similar for a modeling language.
1.Describe the abstract syntax of source and target language using algebraic data types. 2. Define the semantics for both. 3. Define transformations as functions.