*To*: Christian Sternagel <christian.sternagel at uibk.ac.at>*Subject*: Re: [isabelle] Isabelle Proof in Papers*From*: Jesper Bengtson <jesperb at it.uu.se>*Date*: Thu, 21 Jan 2010 11:23:37 +0100*Cc*: Isabelle List <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <4B56E948.20808@uibk.ac.at>*References*: <4B56E948.20808@uibk.ac.at>

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 /Jesper 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 > >

**References**:**[isabelle] Isabelle Proof in Papers***From:*Christian Sternagel

- Previous by Date: Re: [isabelle] Isabelle Proof in Papers
- Next by Date: Re: [isabelle] Problems with Real addition
- Previous by Thread: Re: [isabelle] Isabelle Proof in Papers
- Next by Thread: [isabelle] Problems with Real addition
- Cl-isabelle-users January 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list