Re: [isabelle] Isabelle Proof in Papers

Greetings Chris

I'm currently writing my thesis and trying out the Isabelle-tex capabilities. I am also completely new to this, but I've found a way to display the proofs in a way that I like.

My problem was that I wanted the Isabelle-Isar code in my papers, but I also wanted the nicely generated tex-syntax for my object logic, as I don't want the readers to have to parse weird ascii-xsymbol syntax when reading the proofs.

Anyway, I don't know what your Setup.thy theory looks like, but if it's anything like mine then you have a bunch of abbreviations from your Isabelle expressions to tex-code..... with these \<^raw:..> constructs spliced in to get the proper look that you want.

What you can then do is to write these latex commands in stead of your object logic. The abbreviations will translate it back to the corresponding logic that Isabelle understands, and your scripts will still be fully verified, although completely unreadable at a source code level. They will look nice in print though.

For example, you can have:

from A B C have "tex code" by (rule D)
moreover from ...

You can then comment out the (rule D) part and replace it with txt {* Lemma \ref{mylatexreference} *} if you want, or just add as a comment which lemma you mean by (rule D).

This is not exactly pretty, but it works. What would be nice is if all object logic formulae could be passed through the tex-code generator, but I have been told that this is technically very difficult.

Best of luck


On Jan 20, 2010, at 12:30 PM, Christian Sternagel wrote:

> Hi there,
> currently I'm the first time using Isabelle/HOL for writing a paper. Thanks to Alexander Krauss, most of my initial questions were resolved.
> Initially I wrote my paper as an Isabelle theory Paper.thy, depending on my actual Isabelle/HOL developments. At first, I just stated my lemmas and filled the gaps with some "glue text" to explain everything. Additionally I set up a theory Setup.thy just for introducing notations I wanted to use in the paper. At this stage everything worked fine.
> However, I also wanted to give a textual sketch of every proof that was used for my lemmas. My Idea was to redo every proof that I wanted to describe inside Paper.thy. Then I wanted to hide all Isar commands (using (*<*) and (*>*)), replace them by "glue text" and refer to intermediate formulas, e.g., instead of
>  have "A" by (auto simp: very powerful lemmas)
>  hence "B" by (auto simp: even more powerful lemmas)
> I would like to have
> ... we obtain A by using Lemmas x--y. From
> this we conclude B using ...
> What I tried to do was
>  txt {* ... we obtain *}
>  (*<*)have(*>*) "A" by %invisible (auto ...)
>  txt {* by using Lemmas x--y. From this we conclude *}
>  (*<*)hence(*>*) "B" by %invisible (auto ...)
>  txt {* using ... *}
> The result looks horrible :) and furthermore, no notations from Setup.thy are used. Hence my question: Is there a (preferably easy and nice) way to do what I want? What do others do in such situations?
> Maybe I should also give at least one reason, why I want to do what I showed above. Of course, I would like to rely on Isabelle to check all my displayed formulas in the background. Additionally, I do not want the reader (and especially the reviewer) to see any difference to a paper, just typeset with LaTeX without using Isabelle. My fear is, that reviewers wouldn't like to have to read Isabelle proofs (this surely depends on where you send your paper).
> cheers
> chris

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