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

Dear Gottfried,

My point here is that you are investing a lot of time to reinvent the wheel (moreover a somewhat square wheel that people won't put on their own cars; sorry for that ;)).

My suggestion (just my personal opinion): Keep the actual THY-file as clean and simple as possible.

For a proper presentation of theories there is already Isabelle's document preparation system which works very well for LaTeX. No need to cook up your own variant. (What people often do when they want to publish some Isabelle formalization is to start another theory that imports the actual formalization and write their paper/article in this new theory, referencing facts from the previous formalization. Of course it depends on the audience, what the best solution is. E.g., for mathematicians I would mostly hide Isabelle related stuff and instead of presenting the sourcecode of the actual formalization, just reference facts - using Isabelle's antiquotations - and give textual overviews of the formalized proofs which convey the main ideas.)

Concerning your markups in order to process THY files with scripts. In your example THY file I do not see what additional possibility your markups give, since they always accompany existing commands like "section", "subsection", "definition", ... which could as easily be recognized my scripts.

The most important question: What is your actual application anyway?

Maybe there is already existing infrastructure which could achieve the same goal more easily.



On 10/28/2012 05:46 PM, Gottfried Barrow wrote:

Now on to your complaint about my creating noise and clutter in my THY.

Working on trying to better reduce noise and clutter is half of what I
got out of sending off this email. The other half is learning about the
usefulness of locales to do some preliminary proofs without globally
injecting all the overhead into the THY.

Back to noise and clutter, the challenge is to find a way to mark up
THYs in a way that is reasonably readable, and which can also be
processed with scripts to generate other THY and TEX files to give
people options on how they want to absorb the information.

For mathematical writing, I think there are four main components,

1) Section headings
2) Text/discussion
3) Statement of theorems, definitions, axioms, etc.
4) Proofs

A big part of LaTeX is the newtheorem environment:

I'm trying to duplicate a decent imitation of the newtheorem environment
in the THY file, without creating too much clutter and noise, and not
fall prey to the "gaudy web page syndrome".

It's not obvious how to use a limited set of tools to get something
better than the traditional way of doing things.

Sometimes you don't get something better. There was Xerox. And there was
Apple. It's the story of Apple taking new ideas and refining the new
ideas in significant ways, and doing it with hardware limitations.

I attach my newest attempt to edit my THY so that I can convert my cheap
newtheorem imitations into the real thing with a script, among other
processing. The source code of a marked up language isn't meant for
public consumption, but if the public can consume the source code,
that's a good thing, because then it means you can probably read your
own source code.

Christian, thanks for the help.


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