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


Send me sources, please. As I mention below, it's hard to get excited about an offer when there's still work required by me, but I should at least look at what you got if you offer it to me, plus I might as well have it to be able to open up the THY to see the actual code. There's always something to be learned by looking at the actual code, rather than just the PDF.

On 10/30/2012 3:31 AM, Christian Sternagel wrote:
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.

It becomes a matter of personal preference. I'm trying to figure out a way to format things so that I can read a THY like I read a PDF.

My willingness to get verbose in my THYs, rather than cryptic/clean, is for me. I need to explain concepts to myself, and explain in plain language to myself the steps of my proofs, especially so I can go back months later and know what it is that I'm doing in a proof.

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.)

So partly, we're talking past each other, or talking about different things.

Partly, it's that to get someone really excited about what you offer them, it has to work by magic, and sometimes it helps if you're in their office, and they show you what they're talking about.

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
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.

I completely agree, but I'm pretty much through asking for anything related to the interface. We talk. Makarius listens sometimes. He already has lots of ideas. We might give him some new ideas.

What do we really want? I don't know. Like Mathematica? I don't think so. Like Sounds nice, but that would be a very different road. Using something like that in practice might be terrible, even though I've messed around with it.

Change is risky.

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).

Again, I guess we've talking about different things. I'm not trying to depart radically from the current end result. I think the best way to present theories to people, whether experts or beginners, is the current way. You give them a THY that they can load or import, and for reading if they want, and you give them a PDF to provide them a more polished document that's meant to be read like a book.

I'm just trying to make my working THYs so that they're also meant for reading, even when they're loaded up with a ton of verbosity.

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

Giving you what I attach is premature, but I do it. If it could be months before my next question, that would be good, and maybe I'll have my scripts going by that time.

Like I said, I think the end result as it is now is good. For a theory, people get a THY and a PDF. That I'm doing something non-standard to produce the THY and the PDF is just a result of things evolving into something different for me. If there are any good ideas in it, that's good, but I'm not trying to change anything outside of what I'm doing.

I was taking notes on a tutorial, and the attached pimGreI.pdf was my experimenting at the time.

I was working through prog-tut.pdf, and the attached i12prI2_D.pdf was getting produced at the time.

You don't want to take either too seriously, but the content and layout is a consequence of certain key ideas of mine. Even then, a key idea of mine was that some people, like you, would want things uncluttered and free of the clutter that I put in for myself.


Attachment: i12prI2_D.pdf
Description: Adobe PDF document

Attachment: pimGreI.pdf
Description: Adobe PDF document

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