[isabelle] Isabelle Proof in Papers



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.