Gergely Buday (Mar 17 2025 at 09:57): Gergely Buday (Mar 17 2025 at 09:57):Developing an Isabelle theory is an art. I have my experience in this but I would like to ask for advice.
What I see is that writing good definitions and picking good lemmas are important.
Good definitions: they need not only be correct but they should ease proving lemmas about them. One should be aware what proof support the ingredients have: fold combinators, definitional mechanisms.
Picking lemmas: there are two basic schools on this: bottom-up and top-down. In bottom-up, you have your basic definitions, and first you prove properties of individual definitions as lemmas, and then "obvious" lemmas on combinations of function definitions.
In top-down, you strive for the theorem you really need, and trying to use some automation on the goal you end up with some proof state where you can identify a needed lemma to advance the proof. When you try to prove that lemma you might identify new more low-level lemmas in turn, some of them are already proved in the Isabelle code base. You can do higher-order proving in top-down: you can say sorry for low-level, "trivial" lemmas and focus on the really interesting theorems to see whether your main ideas work.
Unfolding: you need to unfold only one or two levels where you have relevant lemmas to use.
Generalisation: if you need a lemma, try to state it in its most general form: it will be easier to prove, and it will be easier to use in later proofs.
Is there any written wisdom on this? I would love to read your remarks on the above, especially what constitutes a good definition and how shall one write it. And, if you can extend it in any way.
Last updated: Apr 26 2025 at 12:36 UTC