Hey there! Let’s dive into your questions about using Isabelle/HOL for formalizing model transformation correctness—this is a common workflow when dealing with formal verification of meta-models and transformations, so I’ll break it down clearly:

1. Is the Isabelle proof process split into a "programming mode" for coding and a "proof mode" for verification? #

Not exactly in a strict, separate mode way. Isabelle works in an interactive, unified environment: you write your formalizations (like data types, functions, definitions) and your proof scripts in the same context, usually within a .thy theory file. As you write, Isabelle’s IDE (most commonly Isabelle/jEdit) will continuously check and validate both your definitions (to ensure they’re well-formed) and your proof steps (to confirm each logical step is sound). You don’t switch between distinct modes; instead, you build up your formalization and proofs incrementally in one flow.

2. Do I need to manually write .thy theory files in a "programming mode" first, then run them in a "proof mode" to get correctness proofs? #

Yes, .thy files are the core of any Isabelle project—they hold all your formal content, including definitions, lemmas, theorems, and proof scripts. But there’s no separate "programming" vs "proof" mode to switch between. You’ll write everything directly in the .thy file: start by defining your source/target meta-models, then the transformation function, then state your correctness properties as lemmas/theorems, and write the proof steps right alongside them. When you load the .thy file in Isabelle’s IDE, it will automatically process the definitions and validate each proof step in real time. You don’t have to "run" it separately; the verification happens as you build out the file.

3. Do I need to write all Isabelle modules (datatypes, constants, functions, definitions, lemmas, theorems) separately to complete a model transformation correctness proof? #

Absolutely—these components are all essential, interconnected parts of building a rigorous formal proof for model transformation correctness. Here’s how they fit together for your use case:

• Datatypes: Use datatype to formally model the structure of your source and target meta-models (e.g., defining the entities, relationships, and attributes of each model).
• Functions/Definitions: Use fun or definition to encode the model transformation logic itself—this is the formalized version of how you map elements from the source meta-model to the target.
• Lemmas: State intermediate properties of your transformation (e.g., "every source element maps to exactly one target element") and prove them first—these act as building blocks for your final theorem.
• Theorems: State your core correctness claim (e.g., "the transformation preserves the semantic properties X and Y of the source model") and use the lemmas you’ve proven to validate this final result.

Each component builds on the previous one, so you’ll typically write them in that order within your .thy file, incrementally verifying each part as you go.

内容的提问来源于stack exchange，提问作者Junjie Chen