Re: [isabelle] Free variable dead horse beat; getting two equiv formulas after either one is axiomatized



Dear Gottfried,

On 10/30/2012 01:21 PM, Gottfried Barrow wrote:
Okay, this ends up being a perfect example to tie into things I said, or
could have said, and the essence of your complaint about noise and clutter.

You give me a document that you spent a lot of time on to make it a
professional grade document, and you offer to give me the TEX source (or
THY with a lot of LaTeX in it).
I see your point ;) ... but still: a difference to your approach is that I have clean THY files for my main formalization separate from my presentation THY files and only reference those in my presentation THY as needed.

I open the PDF, and I think something that I don't plan on saying at the
time, like, "Well, TEX files and TEX content are a dime a dozen on the
web, and I've already made many of my LaTeX design decisions. Your blue
text boxes look good, but I ruled out using colored boxes some time ago,
though seeing how you do it might get me to think about it again."
I did not want to advertise my design (such choices are just too subjective and maybe I do not even like my design anymore ;)). I was rather talking about the way of presenting formalized Isabelle/HOL theories safely (as in everything is still checked by Isabelle) as a readable PDF in principle. (The design can be arbitrarily chosen afterwards via your usual LaTeX setup.)

However, it was a huge overhead over the actual formalization to
present it this way ;). (And I found it necessary to explain at least
a bit about Isabelle in the beginning.)

This brings up how we work with THY and TEX files. We read the PDF for
the discussion of concepts, and we read the THY (if we have to, or to
edit it) for the non-text{*...*} code.
Concerning my thesis, you do not have to do that, as it directly includes Isabelle proofs (only somewhat pepped up to look more familiar to non-Isabelle users) in the PDF. My goal was to have a PDF that includes all the content but was readable for non-Isabelle users (and Isar does help greatly here). So it should not be necessary to have a look at the THY files (but maybe someone who knows Isabelle, would prefer it and still can, without the THY file being cluttered by my presentation, since - as mentioned above - I use a separate THY file containing all the LaTeX stuff and so on).

Of course, I'm not saying that this is the best solution (or even a good one, I was more or less experimenting) ... just one that I found useful some time ago. And sure, it would be nice to do something similar but with much less effort for the author.

You talked about me reinventing the wheel. This huge overhead you talk
about is something I want to do once, and then benefit from easily and
repeatedly.
I agree. I also think such an effort could (and maybe should) be integrated into Isabelle itself where we have much more control than with external scripts.

Currently Isabelle document preparation "just" supports PDF (and to some extend HTML?) but I don't think that it is in principle restricted to it.

I'm sure that many people, especially on this list, have thoughts about how to properly present a formalization to non-experts. It would be nice to hear those ideas (also if its just a vision for the future).

If you (or anyone else) are interested I can send you the sources later.

TEX sources? A dime a dozen. Pertinent, good instructional content on
Isabelle that's generated from LaTeX, like your Chapter 2? A very, very
small percentage of the content that is generated from the millions of
lines of LaTeX in the world.
I was not so much talking about TeX sources, but rather the theory file that in the end generates the TeX sources and then the PDF file (there is still another wrapper of TeX around the generated TeX sources, but that is just for the usual LaTeX setup you would do anyway when writing a paper).

But thanks to our discussion I see that the subject is (as usual) more intricate than expected.

cheers

chris

@all: Having had a look at my thesis sources again after a long while, I noticed that most (if not all) of my "huge overhead" could have been avoided when syntax that was introduced with the notation command (or similarly) would also apply to the PDF representation of proofs themselves. The same issue has already been talked about here


https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2010-January/msg00037.html

Maybe in the meanwhile there are more thoughts about it?





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