*To*: Isabelle List <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Isabelle Proof in Papers*From*: Norbert Schirmer <schirmer at in.tum.de>*Date*: Thu, 21 Jan 2010 11:23:18 +0100*In-reply-to*: <4B56E948.20808@uibk.ac.at>*References*: <4B56E948.20808@uibk.ac.at>

Hi Christian, one way to achieve what you want is basically the same approach as you have done for your Paper.thy, just applied within an Isar-proof. You basically hide all the real Isar commands with (*<*) ... (*>*) and then afterwards write one txt with antiquotations e.g. to the 'haves' inside. For example ... (*<*) from X Y have p1: "..." by auto (*>*) txt {* From @{thm[source] X} and @{thm[source] Y} we trivially obtain @{thm p1}. *} ... With this approach you get your syntax tricks from Setup.thy applied and still can safely quote formal stuff. Cheers, Norbert On 20.01.2010, at 12:30, 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] Isabelle Proof in Papers
- Previous by Thread: Re: [isabelle] Isabelle Proof in Papers
- Next by Thread: Re: [isabelle] Isabelle Proof in Papers
- 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