Re: [isabelle] Isabelle Proof in Papers



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
> 






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