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

I put an archive of the sources here:

Note the sources were created for Isabelle2009-2 (see also COMPATIBILITY).



On 10/31/2012 01:34 PM, Gottfried Barrow wrote:

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

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.


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