Re: [isabelle] Free variable dead horse beat; getting two equiv formulas after either one is axiomatized
On 10/28/2012 11:58 PM, Christian Sternagel wrote:
The most important question: What is your actual application anyway?
This was your second to the last question. You say it's the most
important, so I move it up here, since I get wordy below.
The application is implementing certain mathematical textbooks in
Isabelle, until I get to a level to where I use Isabelle to implement
The style is educational, textbook writing. Discussion, example,
theorem, proof, exercise, repeat. The original research part will be the
hardest part to achieve, especially because it will be so time consuming
to build up to that level. I at least try to end up having made an
"Hypothetical application" would be a better phrase to use. Applications
require work, and I don't get paid for this. Financial incentive is one
of the best motivators for working, where there would be two halves to
"financial incentive", the reward of income for producing, and the fear
of the loss of income for not producing. I have neither to motivate me.
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 ;)).
The wheel has largely been invented, but the wheel has been optimized
for those who invented the wheel, and for those who have made
significant technical contributions towards getting the wheel rolling.
Let us call this group of people Professional Software Developers (PGD).
Given limited resources, we can say that the choices made so far by the
PGD in optimizing the wheel have been the best choices made, seeing that
the PGD are currently the primary users.
Myself, I'm not a PGD, so the wheel is not completely optimized for my
needs. As to users, at times, I prioritize myself as the most important
My suggestion (just my personal opinion): Keep the actual THY-file as
clean and simple as possible.
Well, it's not possible to tap into the power of LaTeX, or something
similar, and have a primary source code file that's super clean.
You can achieve clean, but then there's cryptic, where, in my opinion,
"cryptic" would currently describe almost all of the Isabelle/HOL
distribution source, and the source on the http://afp.sourceforge.net/.
I'm not complaining here. I'm just talking.
However, as I said, I'm out to cater to the market. For you, in the
future I will easily be able to give you a THY which is nothing but
theorem code, proof code, theorem code, proof code, with some of my
comments in the proofs. Will it turn out that you're annoyed by my
comments? Not a problem. I'll strip them out and give it to you as
cryptic as you want, or someone like you.
It's best not to annoy people who help me out.
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.)
Last year I worked for a month on trying to switch over to Isabelle
document processing. It didn't work out. I didn't figure out a way to
put all THY Isar code in a verbatim environment. I don't explain why
here why I want to do that.
It's my intent to make mathematicians my primary audience, but on your
point of hiding things, my conclusion is the opposite of yours here.
(With all this, opinion heavily comes into play, and my opinions are
subject change, so feel to disregard anything I say here.)
Actually, what I say here is based on my own preferences, where I've
been greatly influenced by the culture of mathematicians.
Proofs are everything, and as a symbol of rigor, a certain amount of
detailed proofs are expected, and they're expected to be written in such
a way that they can be read, where "be read" will vary with the
audience, such as from 1st year university level to Ph.D.
If I'm hiding the details of all the proofs, then why am I even
presenting the math by means of Isabelle? Why not just do things the
traditional way? You may say, "Because if you prove something in
Isabelle, it shows them it's legitimate for sure." But no. It'll prove
nothing to them. What is not presented to mathematicians as literature
with proofs that they can read, they will not be interested in.
Paul Erdos, https://en.wikipedia.org/wiki/Paul_Erd%C5%91s, had no
interest in the proof of the Four Color
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.
When scrolling through a long document, for the major textual items, I
want to answer 4 questions fast: What is it? What's it going to tell me?
Where does it start? Where does it end?
With the Latex theorem environment, you can create your "Definition",
"Theorem", "Postulate", etc, and the environment formatting helps
separate things. Unlike with a Latex theorem environment, In the midst
of lots of other Isar keywords, a Isar keyword like "theorem" doesn't
stand out that well, and it doesn't always describe how it's being used.
(Yes, "theorem" could be used for a theorem, but where are keywords like
"example", "exercise", "remark", "postulate". And you wouldn't want all
those keywords in Isar. I made a very weak attempt to ask Makarius to
allow us to define our own outer-syntax keywords in Isar. I decided that
would be a bad idea. It's the limited number of keywords that
standardize the language.)
Consider my COUNTERX. My COUNTERX is a conjecture for which I've found a
counterexample. The keyword "theorem" doesn't accurately describe how
I'm using "theorem". So suppose I say, "Okay, I have that counterexample
above, and I need to scroll up and look at it again." Also suppose I
have 8 theorems up above. Well, the keyword "theorem" does nothing to
help me quickly locate my counterexample.
Suppose I have 4 counterexamples. The Isar keywords alone don't help me
distinguish between them. Even a named theorem doesn't always tell me
quickly what a theorem does. With the following, I get 4 pieces of
information in the first two lines:
COUNTERX (Shows P is false with input z and y.)
"a big long hard to read formula that would take me a long time to
know what it's about"
--"Nitpick counterexamples that make it false"
The capital bold COUNTERX helps me skip a whole lot of other stuff fast,
like definitions, axioms, theorems, lemmas, etc.
The short description gives me a quick summary of what to expect.
Descriptive theorem names are desirable, but not if they're 10 words
long, so I don't want:
That's hard to read and would be even worse to reference in some other
All this is personal. If you work different, then you'll consider my
tweaking a waste of time.
Maybe there is already existing infrastructure which could achieve the
same goal more easily.
Sometimes, though, I just do what I've been doing, after making some
initial attempt to make a change that didn't work out.
I know that there's a lot of power in Isabelle's document processing,
but I consider it to be less risky to continue down my own non-standard
Thanks again for that proof, and documenting the low-level
quantification that's occurring.
On 10/28/2012 05:46 PM, Gottfried Barrow wrote:
*NOISE AND CLUTTER*
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
3) Statement of theorems, definitions, axioms, etc.
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