[isabelle] Looking for the GOOD way to use Isabelle and Latex together when writing a thesis

Hello everybody,

I am currently writing a master's thesis which includes a lot of Isabelle formalizations and proofs. So of course, I would like to write sections in which I show for example some "highlights" of the formalization or of the proofs, but not entire Isabelle theories (this being saved for the appendix).

I have already written a few "bigger" documents where I also used Isabelle's Latex generation, so I know the basics of how to generate Latex documents and how to use antiquotations etc. But as "solution" to the above scenario, I have always simply copied the parts of the .tex code generated from my theory files and inserted them in my tex source files where I wanted them. But obviously, this can be a lot of work, and if you change just a minor thing like a variable name in your theory files, you have to do this all over again and it is very likely you forget something and in the end, your Latex document is not consistent with your Isabelle theories. Also, I guess the Isabelle latex support is not really meant to be used like this ;).

So basically, I am looking for a good way to combine Isabelle and Latex such that
- I do not need to invest a lot of work to make my tex code consistent with my Isabelle theories whenever I change something in the Isabelle theories
- I do not need to create very obfuscated versions of my Isabelle theories, writing all the explanatory text in between definitions and proof commands, blocking out unwanted parts using %invisible (This would obviously be one answer to ensure only my first condition, but I would like to keep and to work on "clean" versions of my theories, and also to include these "clean" versions in my appendix. However, if there is a way of managing a "clean" version of an Isabelle theory file next to a "heavily commented and annotated" version such that all the definitions inside both versions are consistent, I would also be interested in that.)
- (optionally, if you know anything about it) I can use this way together with latexmk such that the Isabelle .tex representation I need is updated every time I change the .thy files. For this to work, one needs to provide a perl method that tells latexmk how to generate a tex/pdf file from a .thy file. But for example with isabelle make, you usually produce .tex output for a bunch of Isabelle theory files, so if you used this, it would regenerate the .tex output of all Isabelle theory files even though you only changed one .thy file (which can then take quite long if you have a lot of .thy files that belong together...).

How do you deal with such problems when you create large documents and want to show parts of your Isabelle theories inside the text?

Thanks in advance,
Sylvia Grewe

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.