Email Gateway (Aug 19 2022 at 08:52): Email Gateway (Aug 19 2022 at 08:52):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Christian,
I'm now ready to remain skeptical even though I'm safely assuming that
you're right when you say that free variables are quantified with the
"!!" operator. And somehow, my skepticism here is not the same thing as
cognitive dissonance.
If you can tell me the ML file (or ML file folder) where "!!" is used to
quantify the free variables, that would definitively put all this to
rest, I think.
So, you would be at least the third person who has told me that free
variables are implicitly quantified. I'm happy to take lessons in basic
logic, but I think part of what's been leading me astray here is that
with the examples I've been looking at, I logically get the same results
by assuming that free variables aren't implicitly quantified. At the
very least here, I could just switch all this to a question, "Do I get
the same results if I assume free variables aren't quantified?" It might
be a trivial question, with a trivial result. I don't know.
Here, I give two lemmas, one conjecture, and two axioms, which I think
are representative of what I'm doing in my THY, and which ties into your
reply.
Lemma1: (!q. P q) --> (P q)
Lemma2: (P q) --> (!q. P q)
Conjecture1: (!q. P q) <-> (P q)
Axiom1: (!q. P q)
Axiom2: (P q)
Essentially, I can get similar results as you describe below without
assuming that free variables get quantified by "!!".
Prior to Axiom1 and Axiom2 being given, Lemma1 is trivially true, and
Lemma2 is obviously false, so Conjecture 1 is obviously false.
(In this case, if I explicitly quantify Lemma1 and Lemma2 using (!q.
(!q. P q) --> (P q)) and (!q. (P q) --> (!q. P q)), I get the same
results, so it doesn't tell me I'm misguided.)
This result would be similar to my counterexample in my THY. I didn't
actually substitute the values that Nitpick gave me into my formula. If
I did the brainwork, it might show me that it would have to be the case
that "!!" is quantifying the free variables.
Assume Axiom1. Lemma1 doesn't need Axiom1 to be true. For Lemma2,
because of Axiom1, the right-hand side of Lemma2 is always true, thus
Lemma2 is true. This result represents the result of using my first locale.
Assume Axiom2. Again, Lemma1 doesn't need it. For Lemma2, we would have
the equivalent formula (True --> (!q. True)), which is true. This result
represents my result of using my second locale.
Okay, I could be saying the most stupidest of things here. Once I miss
formally learning certain basics, it's hard to find time to go back and
learn what I don't have to know.
It makes sense that free variables would be quantified by the software.
On the other hand, when no one will point me to a formal document
telling me that, I keep open the option that something different could
be going on. "Makes sense" doesn't serve me well sometimes.
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
2) Text/discussion
3) Statement of theorems, definitions, axioms, etc.
4) Proofs
A big part of LaTeX is the newtheorem environment:
ftp://ftp.ams.org/pub/tex/doc/amscls/amsthdoc.pdf
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.
http://www.folklore.org/index.py
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.
Regards,
GB
a_sTs01_121027.thy
Email Gateway (Aug 19 2022 at 08:53):From: Christian Sternagel <c-sterna@jaist.ac.jp>
Dear Gottfried,
I wrote too much in my last email and thereby missed to convey my main
point. Consider the following:
definition P :: "'a => bool" where
"P x == undefined" -- "the exact definition of P doesn't matter"
axiomatization where
Axiom2: "P x" and
Axiom2': "!!x::'a. P x"
thm Axiom2 Axiom2' -- "this shows that for Isabelle both axioms are
the same"
I.e., the resulting theorem that is stored in the theorem database of
Isabelle is exactly the same for Axiom2 and Axiom2', i.e., "P ?x" (where
a schematic variable, the one with the question mark in front, is used
to represent all-quantification, in the sense that we may substitute any
term having the correct type for ?x).
By that reasoning, your Axiom2 is the same as my Axiom2'. Then in order
to get a correct counterexample you would have to disprove
-- "here is a proof that your Axiom1 is equivalent to your Axiom2"
lemma Conjecture: "Trueprop (ALL x::'a. P x) == (!!x::'a. P x)"
proof
fix x::'a assume "ALL x::'a. P x" then show "P x" ..
next
assume "!!x::'a. P x" then show "ALL x::'a. P x" ..
qed
thm Conjecture
But that is not possible, since it is a theorem. Moreover consider
lemma Conjecture1: "(ALL x::'a. P x) <-> P x" sorry
lemma Conjecture1': "!! x. (ALL x::'a. P x) <-> P x" sorry
thm Conjecture1 Conjecture1'
which are two equivalent statements of your Conjecture1. This states
something different from my Conjecture (just have a look at the result
of the thm command).
So, everything else I said aside, your counterexample does not show what
you think it does. That's my main point. Also you do not have to look
into any ML code, just observe the results of the thm command ;)
cheers
chris
Email Gateway (Aug 19 2022 at 08:53):From: Christian Sternagel <c-sterna@jaist.ac.jp>
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.
cheers
chris
Email Gateway (Aug 19 2022 at 08:54):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Christian,
You say, "I wrote too much in my last email and thereby missed to convey
my main point".
I've understood the point all along about implicit quantification, which
Larry called "universal closure", and I knew that if that it was true,
that I couldn't explicitly state certain formulas like I was trying to
do. But you're the first one who explicitly told me that "!!" is where
the quantification is occurring.
It is true that I forgot about the implicit quantification... Actually,
it's becoming too much work to remember what it is I understood or
didn't understand, or forgot once I went off on a tangent by treating
things as unquantified propositions.
Fortunately, you thought I missed your point and went the extra step of
giving me enough details to take everything from the abstract to the
concrete.
You showed things several ways, but this is a very straightforward
demonstration of the quantification that's occurring:
lemma Conjecture1: "(ALL x::'a. P x) <-> P x" sorry
lemma Conjecture1': "!! x. (ALL x::'a. P x) <-> P x" sorry
It seems to me that the documentation should point this out. A person
can say that standard logic principles cover this, but it doesn't,
because Isabelle/HOL is not standard logic.
Magical software is mysterious. Unless told otherwise (and
substantiated), a person might be assuming the truth of "(ALL x::'a. P
x) <-> P x" is being determined with a huge truth table retrieved from
Google, which would allow the formula to be used in other formulas
without quantification being forced on it like it is now.
This implicit quantification is all tied into schematic variables, so it
appears it's not an easy subject to broach:
http://article.gmane.org/gmane.science.mathematics.logic.isabelle.user/5396
At the top is where Lars told me about the implicit quantification, and
then Makarius says:
But when you state lemma "!!x y. A x ==> B y" your result is schematic "A ?x ==> B ?y".
Your proof, using "==", shows you (probably) have to resort to
meta-logic to be able to prove the equivalency without first assuming
either Axiom1 or Axiom2.
Will I do that? No. For my current application, I'll stay away from the
explicit use of meta-logic, if I can. Why? I don't explain that. All
that would do is make this email longer.
Christian, thanks for the proof and documenting what's going on.
Regards,
GB
Email Gateway (Aug 19 2022 at 08:54):From: Gottfried Barrow <gottfried.barrow@gmx.com>
On 10/28/2012 11:58 PM, Christian Sternagel wrote:
Christian,
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
original research.
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
educational contribution.
"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
user.
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
Theorem:https://en.wikipedia.org/wiki/Four_color_theorem
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.)
theorem false_p:
"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"
oops
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:
theorem shows_P_is_false_with_input_z_and_y.
That's hard to read and would be even worse to reference in some other
command.
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
route.
Thanks again for that proof, and documenting the low-level
quantification that's occurring.
Regards,
GB
cheers
chris
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
2) Text/discussion
3) Statement of theorems, definitions, axioms, etc.
4) ProofsA big part of LaTeX is the newtheorem environment:
ftp://ftp.ams.org/pub/tex/doc/amscls/amsthdoc.pdf
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.http://www.folklore.org/index.py
I attach my newest attempt to edit my THY so that I can convert my cheap
newtheorem imitations into the real thing with a s
[message truncated]
Email Gateway (Aug 19 2022 at 08:54):From: Christian Sternagel <c-sterna@jaist.ac.jp>
I tried to achieve something very similar in my PhD-thesis (the content
is not really textbook-like, but the presentation was intended for
people that do not know Isabelle/HOL). Just ignoring the content you
could have a look whether this way of presentation could be used in your
case.
http://www.jaist.ac.jp/~c-sterna/publications/PhD-thesis.pdf
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.)
If you (or anyone else) are interested I can send you the sources later.
cheers
chris
Email Gateway (Aug 19 2022 at 08:54):From: Gottfried Barrow <gottfried.barrow@gmx.com>
On 10/29/2012 8:21 PM, Christian Sternagel wrote:
On 10/30/2012 03:51 AM, Gottfried Barrow wrote:
...I at least try to end up having made an educational contribution.
I tried to achieve something very similar in my PhD-thesis (the
content is not really textbook-like, but the presentation was intended
for people that do not know Isabelle/HOL). Just ignoring the content
you could have a look whether this way of presentation could be used
in your case.http://www.jaist.ac.jp/~c-sterna/publications/PhD-thesis.pdf
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 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."
You tell me to ignore the content, but then when I get to your Chapter
2, I say, "Alright, another one of these PhD theses which provides a
short tutorial on Isabelle. I need to read this Chapter 2."
In fact, your PhD thesis has been setting on my hard drive with
documents from 13 other people, most of who I found on the TUM web site,
and all of whose articles I ripped off of their sites. Those along with
most if not all documents off of Wenzel's, Nipkow's, and Paulson's web
pages.
As it turns out, I'm not interested in your source, I'm interested in
your content. I gave you a THY, and you weren't interested in my
involved system, you just wanted to see the pertinent content, which was
obscured.
I think this describes most of us. We want to know what a person has to
say, or what their code says. We're not normally interested in people's
low-level methods of creating source code.
And now that my attention is brought to your tree in the forest, I see
that on page 13 and 19, you say that implicit quantification is
happening at the meta-logic level. Without the examples you gave me, it
wouldn't have the same meaning that it does now.
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.
I'm trying to get away from this two-document editing process. It's a
pain. Edit, then compile to be able to read it and make sure it
compiles. Do that again forever, hitting the compile button multiple
times on many loops because of a LaTeX error.
REMARK: The continuous prover mode of jEdit makes errors immediate,
which helps to get away from a "compile to make sure it compiles" type
process of editing code. Thanks Makarius.
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.
First, I do a lot of work to set up a THY document style that can be
processed by a script, and I write a bunch of jEdit macros for text entry.
After that, I'm in "cheap imitation WYSIWYG word processor mode". I
compile to PDF, not to see if it compiles (unless I had to resort to
LaTeX), and not to read what I wrote, but to create a professional
looking document to give to other people. The script also creates a
bare-bones THY to give to other people like you who don't want any
verbosity, or help from me to know what the code means. And the code
that's in the bare-bones THY? It's also in a verbatim environment in the
TEX file that gets compiled. (Any of this is subject to change.)
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.
Thanks for bringing attention to your thesis.
Regards,
GB
Email Gateway (Aug 19 2022 at 08:54):From: Christian Sternagel <c-sterna@jaist.ac.jp>
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?
Email Gateway (Aug 19 2022 at 08:55):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Christian,
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
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.
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 http://lyx.org? 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.
Regards,
GB
i12prI2_D.pdf
pimGreI.pdf
Email Gateway (Aug 19 2022 at 08:55):From: Christian Sternagel <c-sterna@jaist.ac.jp>
I put an archive of the sources here:
http://www.jaist.ac.jp/~c-sterna/phdthesis.zip
Note the sources were created for Isabelle2009-2 (see also COMPATIBILITY).
cheers
chris
Email Gateway (Aug 19 2022 at 08:55):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Christian,
Alright. Thanks for putting it up. This will come in useful.
Regards,
GB
Email Gateway (Aug 19 2022 at 09:05):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Hi,
There may not be much to say about this. I'm looking for subtleties that
I may not understand, about what the prover engine is doing with the
free variables when I axiomatize a formula that contains free variables.
I attach the THY and a PDF printout of the THY. The PDF is about 1 and a
1/2 pages long.
I have two formulas:
!q1.!q2.(!x. x ∈ q1 ⟷ x ∈q2) ⟷ (q1 = q2), and
(!x. x ∈ q1 ⟷ x ∈q2) ⟷ (q1 = q2).
First, I show they're not equivalent with a counter example.
Using locales, I then show that if I axiomatize either one of them, then
they're equivalent.
I then axiomatize both of them, and I explain why with my last sentence.
If anyone cares to comment, please do.
Thanks,
GB
a_sTs01_121027.pdf
a_sTs01_121027.thy
Email Gateway (Aug 19 2022 at 09:05):From: Christian Sternagel <c-sterna@jaist.ac.jp>
Dear Gottfried,
first of all, the way you are using symbols in comments is rather
non-conventional and makes the THY file a bit cluttered with unnecessary
noise. Since typical Isabelle users might prefer to consult the THY file
over the generated PDF file that is unfortunate.
Concerning the counterexample: The theorem for which nitpick found a
counterexample does not state equivalence of the two formulas.
To see why, you have to know how Isabelle treats free variables: they
are implicitly all-quantified (using the all-quantifier of Pure, which
is !!). Let "P(q1,q2)" stand for the formula "(!x. x : q1 <-> x : q2)
<-> (q1 = q2)", then your first axiomatization is
!q1. !q2. P(q1,q2)
which stays as it is, since there are no free variables. The second one is
P(q1,q2)
and should be read as
!!q1 q1. P(q1,q2)
Now, if you write
(!q1. !q2. P(q1, q2)) <-> P(q1,q2)
the implicit Pure all-quantification is at the outermost position, i.e.,
!!q1 q2. (!q1. !q2. P(q1, q2)) <-> P(q1, q2)
For this formula nitpick found a counterexample. The think is, this
formula does not state equivalence between your two axioms (since the
quantifiers are at the "wrong" place).
Now for your locales. Since for any Q, "!x. Q x" is logically equivalent
to "!!x. Q x" (in HOL) the locales are equivalent (and thus more or less
identical for automated tools like blast, auto, metis).
Moreover the proofs are both trivial. If we have "!q1 q2. P(q1, q2)" we
can of course specialize this to arbitrary q1 and q2, i.e., "P(q1, q2)".
The other direction of the biimplication, where we have "P(q1, q2)" for
some arbitrary but fixed q1 and q2 and have to show "!q1 q2. P(q1, q2)"
just does not have to use the assumption at all, since the only axiom of
the local is already what we have to prove.
In short: both axioms are indeed equivalent and the counterexample does
not apply since it was generated for a different statement.
Take away: free variables in theorems are implicitly all-quantified.
hope that helps
chris
Last updated: Apr 20 2024 at 04:19 UTC