Email Gateway (Aug 18 2022 at 14:30): Email Gateway (Aug 18 2022 at 14:30):From: Christian Sternagel <christian.sternagel@uibk.ac.at>
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
Email Gateway (Aug 18 2022 at 14:31):From: Lawrence Paulson <lp15@cam.ac.uk>
I prefer to keep my papers and my proofs quite separate. Sometimes I use Isabelle to generate laTeX material, which I process in various ways and insert into documents.
This approach allows you to use integrated TeX environments and have full control over the appearance.
Larry Paulson
Email Gateway (Aug 18 2022 at 14:31):From: Norbert Schirmer <schirmer@in.tum.de>
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
Email Gateway (Aug 18 2022 at 14:31):From: Jesper Bengtson <jesperb@it.uu.se>
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
Last updated: Apr 26 2024 at 12:28 UTC